stencilMomentTensor_quadratic_eq
plain-language theorem explainer
The quadratic form of the Freudenthal stencil moment tensor equals a weighted sum of squared directional projections: vᵀ A₀ v = Σ_d c_d ⟨d,v⟩² over the seven displacement classes. Continuum-limit and discrete-gravity analysts cite it as the algebraic PSD witness for A₀. The proof unfolds the tensor definition and closes by ring arithmetic on the finite sums.
Claim. For every vector $v \in \mathbb{R}^3$, the quadratic form of the stencil moment tensor satisfies $$\sum_{i,j=1}^{3} (A_0)_{ij} v_i v_j = \sum_{d=1}^{7} c_d \, \langle d, v \rangle^2,$$ where $A_0 = \sum_d c_d \, d d^{\mathsf{T}}$, the weights $c_d$ are the square roots of the squared edge lengths of the seven Freudenthal displacement classes, and $d$ runs over the axis, face-diagonal, and body-diagonal displacements with real coordinates in $\{0,1\}^3$.
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign: the action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal triangulation, for every side length $N>2$. The Hessian of the canonical Regge action reduces exactly to a seven-class nearest-displacement stencil $\sum_x \sum_d c_d (u(x+d)-u(x))^2$, with weights $c_d=\sqrt{\ell_d^2}$ read off the incidence dual weights ($\ell^2 \in {1,1,1,2,2,2,3}$ for three axis, three face-diagonal, and one body-diagonal classes).
The stencil moment tensor is the $3\times 3$ matrix $A_0=\sum_d c_d, d d^{\mathsf{T}}$, built from stencilWeight (square root of the periodic squared edge length of class $d$) and dispReal (the explicit $0/1$ coordinate table of the seven displacements). Its closed form is $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ with $J$ the all-ones matrix. The quadratic form identity proved here is the kernel-level sum-of-squares decomposition that makes positive-semidefiniteness immediate.
proof idea
Term-mode proof. Unfold stencilMomentTensor (the double sum defining $A_0$), expand the finite sums over Fin 3 and Fin 7, and substitute the coordinate table dispReal. The resulting polynomial identity in the components of $v$ and the seven weights is discharged by ring. No external lemmas beyond definitional unfolding are required.
why it matters
This identity is the algebraic engine behind stencilMomentTensor_psd, which concludes $v^{\mathsf{T}} A_0 v \ge 0$ by rewriting via the sum-of-squares form and using nonnegativity of each stencil weight. Together they certify that the continuum symbol of the Freudenthal stencil is elliptic (up to the constant kernel), a necessary Stage-1 ingredient for the tensor-first anisotropic action continuum limit (candidate C8, Test G).
In the broader Recognition gravity stack, the module sits under the Regge-action concrete geometry and the periodic Freudenthal torus; the pillar-2 path-sum flag remains red, so this result does not yet flip the refinement-indexed measure-weighted triangulation sum. It does close the kernel PSD witness for the moment tensor that feeds the normalized stencil identity $\rho(N) Q_N(u)=h^3\sum c_d((u(x+d)-u(x))/h)^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.