closedForm
plain-language theorem explainer
Closed-form bi-quadratic for the exact midpoint Bloch mass-squared of a real 4×4 matrix H and wavevector k. Gravity analysts cite it when reducing the midpoint m² to TT polarization or checking pure-gauge vanishing. The body is a pure algebraic assembly of Frobenius, load, and trace-quadratic pieces with fixed rational coefficients.
Claim. For a real $4\times 4$ matrix $H$ and wavevector $k\in\mathbb{R}^4$, define $$C(H,k)=-\tfrac18\|H\|_F^2\|k\|^2+\tfrac14 N_{\mathrm{load}}(H,k)+\tfrac18\,\mathrm{tr}(H)\bigl(\mathrm{tr}(H)\|k\|^2-2\,q(H,k)\bigr),$$ where $\|H\|_F^2$ is the Frobenius squared norm, $\|k\|^2$ the Euclidean wave norm, $N_{\mathrm{load}}$ the load squared norm, and $q(H,k)$ the quadratic form $k\mapsto k^\top H k$.
background
The module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge analysis (script lineage regge_4d_m2_tt_identity). Matrices are Mat4 (real $4\times 4$), waves are Wave4 (maps $\mathrm{Fin},4\to\mathbb{R}$).
Building blocks: Frobenius squared norm $\sum_{i,j} H_{ij}^2$; Euclidean trace $\sum_i H_{ii}$; wave norm squared; load norm squared of the pair $(H,k)$; and the quadratic form associated to $H$ on $k$. Continuum TT polarization is algebraic TT plus Frobenius normalization; without that pin a fixed continuum coefficient is ill-posed.
The surrounding development compares discrete midpoint Bloch $m^2$ against a bi-quadratic with closed rational coefficients, then specializes to transverse-traceless and pure-gauge sectors.
proof idea
Definition only: no proof obligations. The right-hand side is the explicit linear combination
$(-1/8)|H|F^2|k|^2+(1/4)N{\mathrm{load}}(H,k)+(1/8),\mathrm{tr}(H)(\mathrm{tr}(H)|k|^2-2,q(H,k))$.
Downstream theorems unfold this expression and simplify with ring or simp after discharging TT or gauge hypotheses.
why it matters
Anchor expression for the closed midpoint $m^2$ identity. Downstream: exactMidpointBlochM2_eq_closedForm_of_symmetric equates the discrete midpoint Bloch $m^2$ to this form on symmetric $H$; biquad_closedCoeff_eq_closedForm shows the closed-coefficient bi-quadratic reproduces it for every $H$ (not only symmetric); closedForm_eq_neg_eighth_of_TT collapses it to $(-1/8)|H|_F^2|k|^2$ on TT pairs; closedForm_gaugePart_eq_zero proves pure-gauge pairs give identically zero.
That TT reduction is the analytic content of the exact midpoint $m^2$ TT identity the module is written to close. It sits in the gravity/Regge continuum-preflight stack that feeds Recognition Science continuum matching, not in the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.