couplingChunk12
plain-language theorem explainer
Chunk 12 of the auto-generated exact midpoint Bloch coupling table for the 4D flat Regge Hessian. Each row stores a rational coupling s = p/q, two edge displacements in {0,1}^4, and a doubled midpoint offset. Gravity analysts cite it when assembling the full 1208-row table or discharging the chunk-12 CZ bridge. The body is a pure data literal, not a derived proof.
Claim. An array of unit-cell edge-pair couplings for the exact midpoint Bloch symbol of the 4D flat Regge Hessian. Each entry is a quintuple $(p, q, D_e, D_{e'}, \delta_2)$ with rational weight $s = p/q$, edge displacements $D_e, D_{e'} \in \{0,1\}^4$, and doubled midpoint offset $\delta_2 = 2(\mathrm{mid}_e - \mathrm{mid}_{e'})$. This is chunk 12 of the partitioned table.
background
The module holds the exact flat Hessian midpoint Bloch coupling table for 4D Regge calculus, emitted by regge_4d_exact_m2_table_20260721.py and split into chunks so Lean stays under maxRecDepth. Do not hand-edit.
A coupling is one unit-cell edge-pair term: integer numerator and natural denominator for the rational Hessian weight $s = p/q$, integer 4-vectors $D_e$ and $D_{e'}$ for the two edges, and $\delta_2 = 2(\mathrm{mid}e - \mathrm{mid}{e'})$. The continuum Bloch symbol is $\frac12 \sum s , (D_e^\top H D_e)(D_{e'}^\top H D_{e'}) \cos(k \cdot \Delta)$ with $\Delta = \delta_2/2$.
Sibling chunks 0–11 (and later 13–15) have the same shape; this file only materializes partition 12.
proof idea
Definition only: a fixed Array literal of Coupling structures. No tactics, no lemmas. Values come from the external Python emitter; Lean records them as data so downstream decide and concatenation can treat the table as a closed term.
why it matters
Concatenated into the full generated coupling table (n = 1208) via couplingChunk0 ++ ... ++ couplingChunk15. That table is the discrete input for the exact midpoint $M_2$ Bloch analysis of the flat 4D Regge Hessian.
Also feeds czChunk12_bridge, which asserts that mapping this chunk through toCZ recovers czChunk12 by decide. Chunking keeps elaboration feasible while still giving a machine-checkable bridge from Hessian couplings to the CZ kernel certificate side.
In the broader RS gravity stack this is scaffolding data for continuum-limit and kernel-identity work on the discrete Hessian, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.