czChunk14_bridge
plain-language theorem explainer
Chunk 14 of the 4D Regge coupling table, written as structured Coupling records, equals the same data after flattening each record to a CZ integer tuple. Gravity analysts cite it when assembling the full coupling-to-CZ bridge for the midpoint m² TT kernel certificates. The proof is a single kernel `decide` on a finite list equality.
Claim. Converting every entry of coupling chunk 14 from the structured coupling form (numerator, denominator, and three $\mathbb{Z}^4$ multi-indices) into the flattened fourteen-integer CZ record, then reading the array as a list, yields exactly the precomputed CZ chunk-14 list.
background
This module holds machine-generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. Couplings are stored two ways: as Coupling records (rational weight plus three integer 4-vectors $\mathrm{De}$, $\mathrm{Dep}$, $\delta_2$) in the flat Hessian Bloch data module, and as flat CZ 14-tuples of integers in the certificate module.
The converter sends a coupling $c$ to $\langle c.\mathrm{num}, c.\mathrm{den}, c.\mathrm{De}i, c.\mathrm{Dep}i, c.\delta{2,i}\rangle{i=0..3}$. Chunk 14 is one of sixteen fixed blocks that concatenate to the full coupling table. The certificate side lists the same block already flattened, so a bridge lemma is needed before the global table identity can be stated.
proof idea
One-line kernel proof: decide. Both sides are closed finite lists of concrete integer records, so propositional equality is decidable in the kernel without native_decide or arithmetic lemmas. No rewrite of the converter definition is required; the checker compares the fully evaluated lists.
why it matters
Feeds couplingZList_bridge, which asserts that the full coupling table, concatenated from sixteen chunks and mapped through the CZ converter, equals the global CZ list. That parent rewrites with List.map_append and then chains czChunk0_bridge through czChunk15_bridge; this declaration is the chunk-14 step of that chain.
In the Recognition gravity stack these certificates underwrite the exact midpoint $m^2$ TT kernel identity on the 4D Regge lattice (generated by the 20260721 script, scale-32 integer tables). They sit in the discrete-gravity analysis layer rather than the T0–T8 forcing chain, but they are the computational backbone for claiming the TT mass-squared identity holds exactly on the certified kernel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.