Explicit failure-rate bound for the executable automatic Syracuse descent-certificate checker

Fix an accuracy parameter $m \ge 2$ and a sample size $R$ with $2^{24m} \le R$. Recall automaticCertificateFailureCount R m (from Def_collatzFrontierCoverage): among the first $R$ positive odd integers, the number rejected by one fully specified, finite call to the actual executable checker (boundedCertificateTest, at $4m$ descent steps and an automatically computed ambient bit-width). This theorem gives an explicit, fully rational upper bound on the resulting failure fraction:

For each fixed $m$ this bounds the failure fraction of the accuracy-$m$ test; the bound is about $0.943$ at $m=2$ (valid once $R \ge 2^{48}$) and tends to $0$ as $m \to \infty$, each $m$ being a different finite test. The decay is slow (middle rate $\approx 0.971^{m}$). The result is unconditional: it does not assume the joint-law proposition SyracuseJointGeometricBound ("M46") used by an earlier conditional version.

Role and reuse. This is the headline quantitative coverage/completeness result for the actual executable checker: it is an unconditional, fully explicit accuracy/sample-size trade-off for a genuinely finite, machine-checkable test, as opposed to an existential membership predicate. Its proof reduces the checker-acceptance step to the imported platform theorem CollatzFrontier.bounded_descent_generated.

Formalization Note. Transcribed verbatim from CollatzFrontier.automatic_certificate_failure_bound in lean/CollatzFrontier/ExecutableCertificateCoverage.lean. Both hypotheses (hm, hlarge) are used in the proof; none were dropped.