quadraticForm
plain-language theorem explainer
Defines the 4D bilinear quadratic form Q[k;H] = Σᵢⱼ kᵢ Hᵢⱼ kⱼ on a real 4×4 matrix and a 4-vector wave mode. Gravity analysts cite it when assembling the closed midpoint m² TT expression and when relating Dirichlet energy to the Hessian symbol. The body is the plain double sum; no proof content.
Claim. For a real $4\times 4$ matrix $H$ and a real 4-vector $k$, set $Q[k;H] := \sum_{i=0}^{3}\sum_{j=0}^{3} k_i\, H_{ij}\, k_j$.
background
The module closes the exact midpoint Bloch $m^2$ TT identity in 4D Regge calculus (script-backed kernel certificates and numerical assembly). Local types are fixed: Mat4 is a real $4\times 4$ matrix and Wave4 is a real function on Fin 4, i.e. a 4-component mode.
The same bilinear pattern already appears in the weak-field conformal Regge layer as $Q[\xi;M]=\sum_{i,j} M_{ij}\xi_i\xi_j$. There it is the algebraic partner of the Dirichlet form: for symmetric zero-row-sum $M$, $Q=-D$. Here the 4D specialization feeds the closed-form combination of Frobenius, load, and trace terms that encodes the midpoint TT mass coefficient.
Upstream cost algebra defines the shifted cost $H(x)=J(x)+1=\tfrac12(x+x^{-1})$ turning the Recognition Composition Law into d'Alembert form; that $H$ is unrelated notation. The matrix argument of this quadratic form is a Hessian/Bloch symbol, not the cost functional.
proof idea
Definitional one-liner: expand the standard matrix quadratic form as a double finite sum over Fin 4. No lemmas, no tactics, no hypotheses. Downstream proofs simply unfold quadraticForm and simplify the resulting sums (often with Fin.sum_univ_four and ring).
why it matters
This is the bilinear building block inside closedForm, the explicit midpoint TT expression
$(-1/8)|H|_F^2|k|^2+(1/4)\mathrm{load}(H,k)+(1/8)\mathrm{tr}(H)(\mathrm{tr}(H)|k|^2-2Q[k;H])$.
The identity biquad_closedCoeff_eq_closedForm shows every closed-coefficient bi-quadratic collapses to that form, and closedForm_gaugePart_eq_zero uses the same expansion to prove pure gauge pairs contribute zero.
In the weak-field conformal stack it reappears as the object equated (up to sign) with the Dirichlet form under symmetry and zero row sums, which is the algebraic core of the weak-field conformal reduction and the edge-area identities. Within Recognition gravity analysis it therefore links the 4D Regge Hessian symbol to both the exact $m^2$ TT midpoint certificate and the continuum-style energy identities used downstream.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.