couplingWeight_line
plain-language theorem explainer
Along any affine line of 4×4 metric perturbations, the midpoint-Bloch edge-pair coupling weight expands exactly as a quadratic polynomial in the line parameter: constant term, linear cross term, and quadratic self-term. First-variation work in the Euclidean weak-field TT sector cites this to isolate the directional derivative of the closed midpoint Bloch symbol. The proof unfolds the weight, applies additivity and scalar homogeneity of edge strain on both legs of the coupling, then finishes by ring.
Claim. For all $4\times 4$ real matrices $H,K$, every unit-cell edge-pair coupling $c$, and every real scalar $t$, the coupling weight along the affine line satisfies $\mathrm{weight}(H+tK,\,c)=\mathrm{weight}(H,\,c)+t\,\mathrm{cross}(H,K,\,c)+t^{2}\,\mathrm{weight}(K,\,c)$.
background
The ambient module derives the genuine cross-term (directional first variation) of the closed 4D midpoint Bloch symbol in the Euclidean weak-field TT sector, then transports its torus-normalized continuum face via the banked $S_{\mathrm{RS}}\to\mathrm{EH}$ Tendsto on $H\pm K$ plus polarization. Honesty bounds: theorem only in that sector; not a source equation, not Ricci/null focusing, and not GAP1 closure.
Matrices are Mat4 (the 4D continuum preflight matrix type). A Coupling packages one unit-cell edge-pair for the exact midpoint Bloch symbol: integer numerator/denominator and two lattice directions $D_e$, $D_{e'}$. Edge strain is the quadratic form $\sum_{i,j} H_{ij} D_i D_j$ on a direction. Coupling weight (and its polarized cross version) is built from the pair of edge strains on $D_e$ and $D_{e'}$; the present identity is the exact quadratic expansion of that weight along affine lines in matrix space.
Upstream strain lemmas supply additivity and scalar homogeneity of edge strain, which are the only structural inputs beyond unfolding.
proof idea
Tactic proof. Unfold coupling weight and the polarized cross weight. For each of the two coupling legs $D_e$ and $D_{e'}$, rewrite edge strain of $H+t\bullet K$ via the sibling identities edgeStrain_add and edgeStrain_smul, obtaining the affine expansion strain$(H)+t,\mathrm{strain}(K)$ on that leg. Substitute both expansions into the unfolded weight, then close the resulting polynomial identity by ring. No continuum or curvature input is used; the argument is pure bilinearity of the strain quadratic form.
why it matters
Feeds the indexed sibling couplingWeightIdx_line, which lifts the same quadratic line expansion from a single Coupling to a coupling index. That step is local scaffolding for the module's main object: the TT directional first variation of exactMidpointBlochSymbol and its continuum-face transport under S_RS_converges_EH_4d_closed.
In the Recognition gravity stack this is bookkeeping for the Euclidean weak-field TT sector of the closed midpoint Bloch face, not a claim about sourced response or Lorentzian null transport. The module doc is explicit that the missing future object is a Recognition-derived Freudenthal exact-$J$ metric refinement identifying sourced response with this midpoint variation, followed by Lorentzian null-dyad Ricci/stress transport. The identity itself is elementary but mandatory: without exact quadratic expansion of the coupling weight, the polarized first-variation cross term cannot be isolated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.