couplingWeightIdx_line
plain-language theorem explainer
Along the affine line H + t K in 4×4 matrices, the indexed coupling weight expands exactly as a quadratic polynomial: base weight plus t times the cross weight plus t² times the weight of K. Cited by anyone assembling the directional first variation of the closed midpoint Bloch symbol in the Euclidean weak-field TT sector. Proof unfolds the indexed wrappers and applies the unindexed line identity on the table entry at i.
Claim. For $4\times 4$ matrices $H,K$, coupling-table index $i$, and scalar $t\in\mathbb{R}$, the indexed coupling weight satisfies $w_i(H+tK)=w_i(H)+t\,w_i^{\mathrm{cross}}(H,K)+t^2 w_i(K)$, where $w_i$ is the weight of the $i$-th table coupling and $w_i^{\mathrm{cross}}$ is the corresponding bilinear cross weight.
background
The ambient module derives the genuine cross-term (directional first variation) of the closed 4D midpoint Bloch symbol in the Euclidean weak-field transverse-traceless sector, then transports the torus-normalized continuum face via the banked RS-to-Einstein–Hilbert convergence on $H\pm K$ plus polarization.
Mat4 is the $4\times 4$ real matrix type used for continuum Regge preflight data. CouplingIdx is a finite index into the generated coupling table (size 1208) that enumerates the discrete edge/face couplings of the exact flat Hessian Bloch symbol. The indexed weight $w_i(M)$ evaluates the $i$-th table coupling on matrix $M$; the cross weight is the mixed bilinear form that appears as the coefficient of $t$ in the expansion along a line.
Upstream, the unindexed identity couplingWeight_line already gives the same quadratic expansion for a single coupling record. The table itself is the concatenated chunk array from the Regge exact flat Hessian Bloch data module.
proof idea
Term-mode one-liner after unfolding. Unfold the definitions of the indexed weight and the indexed cross weight so both sides become the unindexed weight/cross weight applied to couplingTable[i]. Then apply the already-proved unindexed line identity couplingWeight_line at matrices $H,K$, that table entry, and scalar $t$. No further algebra is needed.
why it matters
This is the indexed bridge that lets the first-variation pipeline work over the full coupling table rather than a single coupling record. Its sole direct consumer is weightFn_line, which rewrites the same quadratic expansion for the weight-function layer used by the midpoint Bloch first variation.
In the Recognition gravity stack it sits inside the Euclidean weak-field TT analysis of the closed midpoint Bloch continuum face (module honesty block). It is deliberately not a source equation, not Ricci/null focusing, and not GAP1 closure; those require a future Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, followed by Lorentzian null-dyad transport. The result is pure algebraic bookkeeping that keeps the directional derivative of the Bloch symbol exact before continuum limits are taken.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.