CouplingIdx
plain-language theorem explainer
Finite index type for entries of the unit-cell coupling table that builds the exact midpoint Bloch symbol in 4D. Anyone writing coupling weights, phases, or the first-variation cross term cites it as the domain of those sums. The body is a pure alias of the same index type from the Regge flat-Hessian Bloch-symbol module.
Claim. Let $N$ be the cardinality of the fixed unit-cell coupling table underlying the exact midpoint Bloch symbol. Then $\mathrm{CouplingIdx}$ is the finite index type $\mathrm{Fin}\,N$, used to label table rows when forming coupling weights, phases, and the trig-polynomial symbol.
background
The ambient module studies the Euclidean weak-field TT directional first variation of the closed 4D midpoint Bloch continuum face, then transports that face via the banked continuum limit $S_{\mathrm{RS}}\to\mathrm{EH}$ on $H\pm K$ plus polarization. It is explicitly not a sourced field equation and not GAP1 closure.
The coupling table is the finite list of lattice couplings that define the model trig-polynomial symbol. Upstream, the same index is introduced as Fin couplingTable.size in the Regge exact flat-Hessian Bloch-symbol development. Sibling objects in this file (4×4 matrices, 4-wavevectors, Frobenius pairing, edge-strain linearity) all consume that index when they sum over table rows.
Related Gap-2 language treats an edge as a two-vertex complex and strain as the per-letter charge; here those ideas appear only as the discrete couplings being indexed, not as a new lattice construction.
proof idea
Definitional abbreviation only: it re-exports the upstream index type ReggeExactFlatHessianBlochSymbol4D.CouplingIdx, itself Fin couplingTable.size. No proof obligations.
why it matters
This alias is the shared domain for every coupling-indexed object in the first-variation pipeline. Downstream it feeds coupling weight and phase maps, their scalar-homogeneity and zero lemmas, the cosine two-jet mass coefficient of the centered symbol, and the exact midpoint Bloch symbol (and its zero-momentum value). Without a single finite index type, the unit-cell sums that define the TT first variation cannot even be stated.
In the broader Recognition gravity stack this sits inside the Euclidean weak-field TT analysis that prepares continuum transport of the midpoint Bloch face. Module honesty forbids reading it as Ricci focusing, null transport, or a Recognition-derived Freudenthal exact-$J$ metric refinement; those remain the stated missing objects after this variation is in hand.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.