couplingChunk14
plain-language theorem explainer
Fourteenth data chunk of the exact midpoint Bloch coupling table for the 4D Regge flat Hessian. It stores one block of unit-cell edge-pair couplings: each entry is a rational Hessian weight with two edge displacements in {0,1}^4 and a doubled midpoint offset. Gravity analysts cite it when assembling the full table or discharging the chunk-14 CZ bridge. The body is pure generated literal data, not a proof.
Claim. The fourteenth chunk of the generated 4D Regge flat-Hessian midpoint Bloch coupling table: a finite array of unit-cell edge-pair couplings. Each entry is a rational weight $s=p/q$ together with edge displacements $D_e,D_{e'}\in\{0,1\}^4$ and doubled midpoint offset $\delta_2=2(\mathrm{mid}_e-\mathrm{mid}_{e'})$.
background
This module holds the exact flat Hessian midpoint Bloch coupling table for 4D Regge calculus. It is auto-generated (do not hand-edit) and split into chunks so Lean stays under maxRecDepth. The continuum symbol reconstructed from the table is
[(1/2)\sum s,(D_e^\top H D_e)(D_{e'}^\top H D_{e'})\cos(k\cdot\Delta),]
with $\Delta=\delta_2/2$.
A single coupling record packages the rational Hessian weight $s=\mathrm{num}/\mathrm{den}$, the two edge displacements $D_e,D_{e'}$ as maps $\mathrm{Fin},4\to\mathbb{Z}$, and the doubled midpoint offset $\delta_2=2(\mathrm{mid}e-\mathrm{mid}{e'})$. Chunks are siblings of the same shape; this is chunk 14 of that sequence.
proof idea
No proof. The declaration is a def whose right-hand side is a literal Array of structure values, emitted by the generator script. Each row is written as a five-field constructor (numerator, denominator, $D_e$, $D_{e'}$, $\delta_2$). Elaboration cost is the only reason the table is split; the chunk itself performs no algebraic reduction.
why it matters
The full generated table is the concatenation of chunks 0 through 15 (1208 rows). This chunk is one summand of that assembly, so every consumer of the complete Bloch coupling data depends on it indirectly.
Directly, the kernel certificate czChunk14_bridge asserts that mapping this chunk through toCZ recovers the corresponding CZ chunk, proved by decide. That bridge is part of the exact midpoint $M_2$ TT-identity certification for the 4D flat Hessian. In the broader Recognition gravity stack, the table supplies the discrete quadratic form whose continuum limit is the Bloch symbol used in Regge/Hessian analysis; it does not itself invoke the forcing chain (T5–T8) or the J-cost RCL, but it is infrastructure those continuum comparisons rest on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.