czChunk5_bridge
plain-language theorem explainer
Chunk-5 bridge: converting the fifth block of the 4D Regge coupling table into flattened CZ integer tuples recovers the precomputed CZ list for that block. Gravity analysts cite it when assembling the full coupling-to-CZ table equality. The proof is a single kernel `decide` on finite list equality.
Claim. Mapping each entry of coupling chunk 5 through the flattening map (numerator, denominator, and the twelve integer components of the three lattice vectors $D_e$, $D_e'$, $\Delta_2$) yields exactly the precomputed CZ chunk-5 list.
background
This module holds machine-generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Couplings are stored as records with a rational weight (num/den) and three $\mathbb{Z}^4$ lattice vectors ($D_e$, $D_e'$, $\Delta_2$). The CZ form flattens those vectors into twelve bare integers so the whole table becomes a pure integer list amenable to decide.
Chunk 5 is one of sixteen blocks of the flat Hessian Bloch coupling table. The source block lives in the Bloch data module; the CZ image is a hand-emitted constant list in this cert module. The conversion toCZ is componentwise unpacking, not a physical map.
The local convention is Int List.foldl with scale-32 tables and kernel decide only (no native_decide), matching the generator script named in the module doc.
proof idea
One-line wrapper: decide. Both sides are closed concrete terms (a mapped finite array versus a literal List CZ), so propositional equality is decidable and the kernel discharges it with no lemmas or rewriting.
why it matters
Feeds couplingZList_bridge, which concatenates the sixteen chunk bridges and rewrites the full couplingTable.toList.map toCZ = couplingZList identity via List.map_append and the per-chunk equalities. Without chunk 5, the global table certificate does not close.
In the Recognition gravity stack these certs underwrite the exact midpoint $m^2$ TT kernel identity on the 4D Regge lattice (flat Hessian Bloch data). They are bookkeeping, not a new dynamical law, but they make the discrete curvature/coupling algebra checkable inside Lean rather than trusted from external numerics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.