weightFn_line
plain-language theorem explainer
Along any affine line H + tK of 4×4 matrices, each coupling-channel weight expands as a quadratic polynomial in t: value at H, plus t times the cross weight of (H,K), plus t² times the weight of K. Used when assembling the line expansion of the closed midpoint Bloch symbol. Proof unfolds the weight definitions and applies the coupling-index line identity.
Claim. For $4\times 4$ matrices $H,K$, scalar $t\in\mathbb{R}$, and coupling index $i$, the channel weight satisfies $\mathrm{weight}(H+tK,i)=\mathrm{weight}(H,i)+t\,\mathrm{crossWeight}(H,K,i)+t^{2}\,\mathrm{weight}(K,i)$.
background
The module derives the directional first variation of the closed 4D midpoint Bloch symbol in the Euclidean weak-field transverse-traceless (TT) sector, then transports the torus-normalized continuum face via the banked SRS-to-Einstein–Hilbert convergence on $H\pm K$ plus polarization.
Here Mat4 is the $4\times 4$ continuum matrix type from the Regge preflight layer, and CouplingIdx indexes the finite coupling table of the exact flat Hessian Bloch symbol. The weight function assigns a scalar cost contribution to each coupling channel of a matrix strain; the cross weight is the mixed bilinear term between two strains on the same channel.
The algebraic engine underneath is the coupling-index line expansion already proved for the raw coupling weights; this declaration merely packages that identity in the named weight / cross-weight interface used by the Bloch-symbol calculus.
proof idea
One-line wrapper. Rewrite the goal with the three weight definitions and the cross-weight definition, then close by the already-proved coupling-index line identity couplingWeightIdx_line H K i t, which supplies the same quadratic expansion at the raw coupling-weight level.
why it matters
Feeds the parent theorem exactMidpointBlochSymbol_line, whose doc-comment states the target expansion $Q(H+tK)=Q(H)+t\cdot\mathrm{FV}(H,K)+t^{2}\cdot Q(K)$. That line identity is the algebraic step that isolates the genuine cross-term / directional first variation of the closed midpoint Bloch symbol before continuum transport.
In the Recognition gravity stack this sits inside the Euclidean weak-field TT analysis that prepares a Recognition-derived first variation; it is explicitly not a source equation, not Ricci/null focusing, and not GAP1 closure. The missing future object named in the module honesty block is a Freudenthal exact-$J$ metric refinement identifying the sourced response with this midpoint variation, followed by Lorentzian null-dyad transport.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.