A source-compatible finite-certificate framework for the Collatz conjecture via compact L = 7 certification and global primitive

This article develops a finite-certificate framework for the Collatz problem based on asource-compatible decomposition of the odd dynamics. The argument separates three layers.First, an anti-9 reduction sends every odd integer not divisible by 3 to an odd predecessorsource divisible by 3. Second, a compact L = 7 frontier certificate organizes the residualsource dynamics into a finite family of admissible first-exit classes. Third, a primitive re-entrymechanism gives a strict descent of the primitive parameter outside the finite base rangeξ ≤ 6561.The proof is reduced to two explicitly identified components: an analytic descent argumenton primitive source families, and a finite certificate layer checking the frontier, first-exit,positivity, and compatibility conditions used by the descent. The submitted package containsdeterministic replay scripts and SHA-256 manifests for the finite layer. It is now accompaniedby two Lean 4 archives. The certificate-master archive checks the finite certificate bundlethrough RederoCollatz.FinalCheck. The global-shell archive checks the anti-9 table, firstexit positivity, preservation under removal of powers of two, the primitive descent inequality,strong induction on the primitive parameter, and the reduction from positive odd integers toall positive integers, with no project-level axiom declarations in the RederoCollatz sources.The remaining global interface is explicitly identified as the source-layer certificate hypothesisSourceLayerConvergence, which the certificate-master archive is designed to audit at thefinite-data level.