couplingWeightCrossIdx
plain-language theorem explainer
Indexes the bilinear cross-weight of two 4×4 strain matrices against the i-th row of the fixed 1208-entry coupling table. Anyone assembling the directional first variation of the closed midpoint Bloch symbol cites this. The body is a one-line lookup wrapper around the unindexed cross-weight.
Claim. For $4\times 4$ matrices $H,K$ and coupling index $i\in\{0,\ldots,1207\}$, the indexed cross coupling weight is the unindexed cross-weight of $H$ and $K$ evaluated on the $i$-th row of the generated coupling table.
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+K$ and $H-K$ plus polarization.
Mat4 is the $4\times 4$ real matrix type used for continuum Regge strains. CouplingIdx is Fin of the size of the generated coupling table (1208 rows), the discrete edge-pair catalogue of the exact flat Hessian Bloch symbol. The unindexed sibling cross-weight takes two matrices and one coupling record and returns the bilinear edge-strain cross factor; this definition merely selects that record by index.
Upstream, the coupling table is the concatenated chunk array of all admissible couplings for the 4D Bloch data. The cost-algebra $H$ and bridge ratio $K$ appear in the broader gravity stack but are not free parameters of this wrapper.
proof idea
Pure definitional wrapper: evaluate the unindexed cross-weight on couplingTable[i]. No tactics, no lemmas. The subsequent opaque crossWeightFn freezes the same map for Fin-1208 hygiene so downstream sums do not unfold the table lookup.
why it matters
Feeds two local parents. The line identity expands the indexed coupling weight along $H+tK$ as a quadratic polynomial whose linear coefficient is exactly this cross-weight. The directional first variation of the midpoint Bloch symbol is the finite sum over all coupling indices of this cross-weight times the cosine of the corresponding Bloch phase.
That first variation is the concrete cross-term the module then polarizes and passes through the closed 4D RS-converges-to-EH continuum face. Per the module honesty clause, the result lives only in the Euclidean weak-field TT sector: it is not a source equation, not Ricci or null focusing, and not GAP1 closure. The missing future object remains a Recognition-derived Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.