czChunk0_bridge
plain-language theorem explainer
Finite certificate that coupling chunk 0, after flattening each Coupling into the CZ integer record, equals the precomputed czChunk0 table. Gravity analysts cite it when assembling the full midpoint m² TT kernel identity in 4D Regge calculus. The proof is a pure kernel decide on equality of finite integer lists.
Claim. Converting every entry of coupling chunk 0 via the flattening map (numerator, denominator, and the four components each of $D_e$, $D_e'$, $\Delta_2$) yields exactly the precomputed CZ chunk-0 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 structured records (rational weight plus three $\mathbb{Z}^4$ multi-indices $D_e$, $D_e'$, $\Delta_2$). The CZ type is the same data flattened to fourteen integer/nat fields so that list equality is decidable by the kernel alone.
Chunk 0 is the first block of the Bloch-style flat Hessian coupling table imported from the companion data module. The conversion map sends each Coupling to a CZ by reading off num, den, and the four components of each multi-index. The target list czChunk0 is the script-emitted table of those flattened rows.
The module convention is Int/List.foldl arithmetic with scale-32 tables and kernel decide only (no native_decide).
proof idea
One-line decidability proof. Both sides are concrete finite lists of integer tuples; Lean closes the equality by decide with no lemmas or rewriting.
why it matters
First of the sixteen chunk bridges that feed couplingZList_bridge. That parent theorem rewrites the full coupling table (concatenation of all chunks) under the flattening map to the global CZ list, which is the data backbone of the midpoint $m^2$ TT identity kernel certificate in 4D Regge gravity.
In the Recognition Science gravity stack these certificates lock the discrete Hessian/Bloch data used for the exact midpoint identity, so downstream continuum or continuum-limit arguments can treat the kernel as machine-checked rather than hand-tabulated. No open scaffold remains here: the claim is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.