exactMidpointBlochSymbol_line
plain-language theorem explainer
The exact midpoint Bloch symbol is exactly quadratic along affine lines in metric space: Q(H+tK)=Q(H)+t·FV(H,K)+t²·Q(K). Anyone deriving the TT first variation or continuum polarization of the closed 4D Regge symbol cites this. The proof rewrites to the irreducible weight/phase form, expands each coupling weight as a quadratic polynomial in t, then distributes the finite sum.
Claim. For $4\times 4$ metric matrices $H,K$, wavevector $k$, and real scalar $t$, the exact midpoint Bloch symbol satisfies $$Q(H+tK,k)=Q(H,k)+t\,\mathrm{FV}(H,K,k)+t^{2}\,Q(K,k),$$ where $Q$ is the finite cosine polynomial over the unit-cell coupling table and $\mathrm{FV}$ is its directional first-variation cross term.
background
This module works in the Euclidean weak-field transverse-traceless (TT) sector of the closed 4D midpoint Bloch continuum face. The exact midpoint Bloch symbol $Q(H,k)$ is the finite trig polynomial $\sum_i w_i(H)\cos(\theta_i(k))$ over the unit-cell coupling table: each term pairs a metric-dependent coupling weight with a wavevector-dependent phase cosine.
Matrices live in the $4$D continuum preflight type (Mat4); wavevectors are Wave4. The first-variation cross term $\mathrm{FV}(H,K,k)$ is the genuine bilinear cross weight summed against the same cosines. The module's honesty clause restricts all theorems here to that Euclidean TT sector: not a source equation, not Ricci/null focusing, and not GAP1 closure.
Upstream, $Q$ is defined in the Regge exact flat Hessian Bloch-symbol development as that coupling-table sum. The line identity is the algebraic engine that later yields both the $t=0$ directional derivative and the polarization formula for $\mathrm{FV}$.
proof idea
Rewrite $Q(H+tK)$, $Q(H)$, $Q(K)$, and $\mathrm{FV}(H,K)$ into the irreducible weight/phase form via the corresponding _eq_irred lemmas. For each coupling index, the weight along the affine line expands by weightFn_line as $$w_i(H+tK)=w_i(H)+t,w^{\times}_i(H,K)+t^{2},w_i(K);$$ multiply by $\cos(\theta_i(k))$ and rearrange with ring. Congruence of the finite sum, two applications of Finset.sum_add_distrib, then factor $t$ and $t^{2}$ out of the remaining sums with Finset.mul_sum, recovering the claimed quadratic identity.
why it matters
This is the exact finite-line expansion that makes the TT first variation of the closed midpoint Bloch symbol computable. Downstream it feeds hasDerivAt_exactMidpointBlochSymbol_line (directional derivative of $t\mapsto Q(H+tK)$ at $t=0$ equals $\mathrm{FV}$) and exactMidpointBlochFirstVariation_polarization (the polarization identity $\mathrm{FV}(H,K)=(Q(H+K)-Q(H-K))/2$).
Together those results transport the torus-normalized continuum face via the banked $S_{\mathrm{RS}}\to\mathrm{EH}$ Tendsto on $H\pm K$, which is the module's stated goal. Within Recognition Science gravity analysis this sits in the Euclidean weak-field TT sector only; the missing future object named in the module doc is a Recognition-derived Freudenthal exact-$J$ metric refinement that would identify the sourced response with this midpoint variation, then Lorentzian null-dyad Ricci/stress transport. It does not close GAP1 and must not be cited as a source equation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.