czChunk7_bridge
plain-language theorem explainer
Chunk 7 of the 4D Regge coupling table, after flattening each Coupling into a CZ record, equals the precomputed integer list czChunk7. Gravity analysts cite it when assembling the full couplingZList bridge for the midpoint m² TT kernel certificate. The proof is a pure kernel decide on finite integer data.
Claim. Converting every entry of coupling chunk 7 (an array of signed rational couplings with three $\mathbb{Z}^4$ multi-indices) via the componentwise flattening map to CZ records yields exactly the certified list for chunk 7.
background
This module holds generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Data are stored as scale-32 integer tables; equalities are discharged by decide only (no native evaluation).
A Coupling packages a rational weight (num, den) with three multi-indices De, Dep, delta2 in $\mathbb{Z}^4$. The map toCZ flattens those fields into a single 14-tuple CZ record (numerator, denominator, then twelve integer components). Coupling chunk 7 is one of sixteen fixed arrays that concatenate to the full coupling table; czChunk7 is the matching hand-certified list of CZ records.
Upstream, couplingChunk7 supplies the structured array; the bridge only asserts that its list view, after toCZ, coincides with czChunk7.
proof idea
One-line kernel proof: decide. Both sides are concrete finite lists of integer tuples, so propositional equality is decidable and closes without lemmas or rewriting.
why it matters
Parent theorem couplingZList_bridge rewrites the full table equality by concatenating the sixteen chunk bridges; this declaration is the chunk-7 step in that rw chain. Without it the midpoint $m^2$ TT kernel certificate cannot assemble the global coupling list used in the 4D Regge Hessian analysis. It is pure data integrity for the generated certificate script, not a dynamical claim, but it is required scaffolding for the gravity-side kernel identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.