Completeness of the executable Syracuse descent checker on canonical dyadic chains

Fix two sequences $a, b : \mathbb{N} \to \mathbb{N}$ (exponents and representatives) and a dyadic modulus budget $K$. chainCertificate a b K k packages the length-$k$ prefix of this data into the executable DescentCertificate format of Def_collatzFrontierCertificate (the coefficient at step $i$ is the exact remaining budget $3^i \cdot 2^{K - \sum_{j<i} a_j}$). This theorem is the completeness (acceptance) bridge between an abstract Syracuse-step chain and the executable checker checkDescent:

whenever (i) the start representative $b_0$ is a positive odd number strictly below $2^K$ (so the family $b_0 + 2^K q$ is a canonical progression), (ii) every exponent $a_i$ for $i \le k$ is positive, (iii) the exact division identity $3 b_i + 1 = 2^{a_i} b_{i+1}$ holds through step $k$, (iv) every intermediate representative $b_{i+1}$ for $i < k$ is odd, (v) the cumulative exponent budget $\sum_{i \le k} a_i$ does not exceed $K$, and (vi) the representative strictly decreases ($b_{k+1} < b_0$).

Role and reuse. This is the single reusable checker-completeness engine behind both the linear-budget completeness theorem (bounded_descent_generated, which instantiates it with the factorization-derived exponent/representative sequence of an actual Syracuse orbit) and the adaptive-budget completeness equivalence (eventual_descent_iff_certificate, via the same instantiation). Packaging it as its own platform theorem removes the need to re-derive this ~60-line argument inside each of those two headline proofs.

Formalization Note. Transcribed verbatim from CollatzFrontier.chainCertificate_accepts in lean/CollatzFrontier/CertificateCompleteness.lean. All eight hypotheses are used in the proof; none were dropped.