czChunk11
plain-language theorem explainer
Chunk 11 of the rational coupling table for the 4D Regge midpoint m² TT kernel certificate. Each entry is a signed fraction together with discrete edge and dual-edge multi-indices. Gravity analysts cite it when assembling the full coupling list or checking the generated bridge equality. The body is a literal list of structure values, produced by the kernel-cert script.
Claim. Define the eleventh block of the coupling table as an explicit finite list of records, each carrying a rational coefficient $n/d$ and integer multi-indices for the edge increments $(\Delta e_i)$ and dual-edge increments $(\Delta e'_j)$ that appear in the 4D Regge midpoint $m^2$ transverse-traceless kernel identity.
background
The module supplies machine-generated kernel certificates for the midpoint $m^2$ TT identity in 4D Regge calculus. Certificates are built from integer fold and scale-32 tables so that kernel goals close by decide alone, without native_decide.
Each table row is a CZ record: numerator and denominator of a rational coupling, plus integer coordinates for edge and dual-edge contributions. Sibling chunks czChunk0 through czChunk15 partition the full table so Lean can typecheck large literals in pieces.
Upstream, the structure type alone fixes the schema; no analytic lemma is required to introduce a chunk. The generating script is scripts/qg/regge_4d_m2_kernel_certs_20260721.py.
proof idea
There is no proof. The declaration is a pure data definition: a concrete List of CZ constructors with integer and natural literals. Downstream, czChunk11_bridge re-derives the same list from couplingChunk11 by decide, confirming the hand-inlined chunk matches the generated source.
why it matters
The full coupling table is the concatenation couplingZList = czChunk0 ++ ... ++ czChunk11 ++ ... ++ czChunk15. Without every chunk the kernel certificate for the midpoint $m^2$ TT identity cannot be assembled. The bridge theorem czChunk11_bridge pins this block to the generator output, so edits to the script or the literal are caught by decide.
In the broader Recognition gravity stack this sits inside exact 4D Regge Hessian and Bloch-data analysis (imported from ReggeExactFlatHessianBlochData4D). It is bookkeeping infrastructure for the discrete curvature kernel, not a forcing-chain step (T0–T8) or an RCL identity; it exists so the TT mass-squared identity can be certified by pure kernel decision procedures.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.