Coupling
plain-language theorem explainer
Packages one unit-cell edge-pair term in the exact flat 4D Regge midpoint Bloch Hessian: rational weight s = num/den, integer edge displacements De and Dep on Fin 4, and doubled midpoint offset delta2. Downstream continuum-symbol and mesh-coupling lemmas cite this row type. It is a plain data structure with derived rational and real projections, not a proved identity.
Claim. A unit-cell edge-pair coupling is a 5-tuple $(p,q,D_e,D_{e'},\delta_2)$ with $p\in\mathbb{Z}$, $q\in\mathbb{N}$, $D_e,D_{e'},\delta_2:\{0,1,2,3\}\to\mathbb{Z}$, encoding the rational Hessian weight $s=p/q$, the two edge displacement vectors in $\{0,1\}^4$, and the doubled midpoint offset $\delta_2=2(\mathrm{mid}_e-\mathrm{mid}_{e'})$. The derived fields are $s\in\mathbb{Q}$ and $\Delta=\delta_2/2\in\mathbb{R}^4$.
background
The module is an auto-generated table of exact flat Hessian midpoint Bloch couplings for 4D Regge calculus. Each row feeds the continuum symbol
$(1/2)\sum s,(D_e^T H D_e)(D_{e'}^T H D_{e'})\cos(k\cdot\Delta)$ with $\Delta=\delta_2/2$. Chunking keeps Lean elaboration under maxRecDepth.
Upstream, $D_e$ and $D_{e'}$ match the integer edge-displacement extractors used in the midpoint $M_2$ TT-identity kernel certificate. Plane-wave phase $k\cdot x$ (sum over four coordinates) is the continuum Fourier mode against which $\Delta$ is dotted. The Kronecker delta and eight-tick phase appear only as ambient RS infrastructure, not as fields of this structure.
The name collides with an unrelated FEP sparsity Coupling (a Prop on state classes). Here the meaning is purely geometric: one sparse Hessian edge-pair contribution on the flat 4-torus unit cell.
proof idea
No proof: a structure declaration plus two noncomputable projections. Coupling.s casts num/den to $\mathbb{Q}$. Coupling.delta maps each coordinate of delta2 to a real by dividing by 2, recovering the midpoint phase offset $\Delta$. Sibling couplingChunk0…couplingChunk10 are concrete table rows of this type.
why it matters
This is the row schema for the generated exact flat Hessian Bloch table that underwrites 4D Regge midpoint analysis. Local consumers include couplingChunk* and mesh_recognition_ratio_derived in the recognition-mesh dual-entry coupling development. Broader ledger and continuum bridges (bridge_chain_complete, edge-length-from-$\psi$ flatness, $J$-log error bounds) sit in the same gravity/ledger stack that needs a certified discrete-to-continuum Hessian symbol.
In the RS forcing picture the table supports the discrete side of the cubic bridge toward Einstein coupling at flat vacuum (T8, $D=3$ spatial plus time as Fin 4). It does not itself prove uniqueness of $J$, $\phi$, or the eight-tick octave; it supplies the numerical coupling data those continuum identities consume when specialized to exact midpoint Bloch modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.