couplingZList
plain-language theorem explainer
The full integer-encoded 4D Regge coupling table as a flat list of CZ records, formed by concatenating sixteen generated chunks. Kernel certificates fold over this list to clear denominators and prove vanishing of midpoint m² TT and Bloch-symbol quartic numerators. The body is pure list append of the precomputed chunks.
Claim. Let $\mathrm{CZ}$ be the integer record $(n,d;\Delta e_0,\ldots;\Delta e'_0,\ldots)$ packing one coupling coefficient. Define the master coupling list as the concatenation of the sixteen generated chunks $C_0\mathbin{+\!+}\cdots\mathbin{+\!+}C_{15}$, each a finite list of such records.
background
This module holds machine-generated kernel certificates for the midpoint $m^2$ transverse-traceless identity in 4D Regge calculus. The script emits Int List.foldl tables scaled by 32; proofs use only decide (no native_decide).
Each coupling is packed as a CZ structure: integer numerator and natural denominator, plus integer edge and dual-edge multi-indices that enter the cleared-denominator contribution. The sixteen czChunk* definitions are the raw generated slices of that table.
Downstream folds (m2Num, qNum) sum integer contributions over the full list after clearing denominators against the fixed scale 16, so the list is the single source of truth for every kernel vanishing certificate in this family.
proof idea
Definition only: the value is the successive list-append of czChunk0 through czChunk15. No proof obligations; the mathematical content lives in the chunk data and in the bridge theorem that identifies this concatenation with couplingTable.toList.map toCZ.
why it matters
Every kernel certificate in the midpoint $m^2$ TT and flat-Hessian Bloch-symbol pipelines folds over this list. Immediate consumers include m2Num (cleared $m^2$ numerator), qNum (cleared quartic numerator), couplingZ_den_dvd_16 (every denominator divides 16), and the glue lemmas that relate rational coupling terms to integer contributions divided by 32.
The companion couplingZList_bridge proves the list equals the mapped live coupling table, so decide-based vanishing on the Int encoding transfers back to the geometric coupling data. In the Recognition gravity stack this is scaffolding for exact 4D Regge Hessian identities that underwrite continuum TT mode structure, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.