Linear-budget completeness of the generated Syracuse descent certificate

Let $n$ be a positive odd natural number with $n < 2^L$ (so $L$ bits suffice to describe $n$), and suppose the Syracuse map descends at time $t$: $\mathrm{syracuseStep}^{[t]}(n) < n$ (iterating the accelerated map $\mathrm{syracuseStep}(n) = \mathrm{ordCompl}_2(3n+1)$ $t$ times drops below $n$). This theorem shows that the executable generator candidateCertificate of Def_collatzFrontierCertificate — which guesses each division's exponent by bounded trial division, capped by an explicit fuel parameter — already succeeds at the uniform, linear budget $\mathrm{fuel} = \text{modulus exponent} = L + 2t$:

In words: both the amount of trial division the generator needs, and the size of the certified residue class, scale only linearly in the input's bit-width $L$ and the number of descent steps $t$ — not merely as some unspecified (adaptively large) budget.

Role and reuse. This is the key uniform-budget estimate behind the explicit failure-rate bound (automatic_certificate_failure_bound), which calls it directly on every input it certifies as a bounded descent. Its proof reduces to the checker-completeness platform theorem CollatzFrontier.chainCertificate_accepts, plus an explicit estimate (syracuse_total_valuation_budget) on how large the cumulative 2-adic valuation of a Syracuse orbit's $3x+1$ numerators can be relative to the orbit's own linear growth bound.

Formalization Note. Transcribed verbatim from CollatzFrontier.bounded_descent_generated in lean/CollatzFrontier/ExplicitCertificate.lean. All four hypotheses (hn, hodd, hsize, hdesc) are used in the proof; none were dropped. No reference to the unproved joint-law proposition SyracuseJointGeometricBound ("M46") occurs anywhere in the statement or proof.