stencilMomentTensor_ne_zero
plain-language theorem explainer
The (0,0) entry of the Freudenthal stencil moment tensor A₀ is nonzero. Continuum-limit and ellipticity arguments for the frozen Regge Hessian on the canonical periodic Freudenthal family cite this as the first nondegeneracy check on A₀. The proof is a one-line lift of diagonal positivity via ne_of_gt.
Claim. The stencil moment tensor $A_0=\sum_{d\in D} c_d\, d d^{\mathsf T}$ of the seven Freudenthal displacement classes satisfies $(A_0)_{00}\neq 0$.
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 at every side length $N>2$. The quadratic form of the canonical Regge Hessian is identified with a seven-class nearest-displacement stencil $\sum_x\sum_{d:F_7} c_d(u(x+d)-u(x))^2$, with dual weights $c_d=\sqrt{\ell_d^2}$ for the three axis, three face-diagonal, and one body-diagonal classes ($\ell^2\in{1,1,1,2,2,2,3}$).
The stencil moment tensor is the $3\times 3$ matrix $A_0=\sum_d c_d, d d^{\mathsf T}$. It is computed exactly as $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ ($J$ the all-ones matrix), so every diagonal entry equals $1+2\sqrt{2}+\sqrt{3}$ and every off-diagonal equals $\sqrt{2}+\sqrt{3}$.
Upstream, stencilMomentTensor_diag_pos already proves every diagonal entry is strictly positive by rewriting through that closed form and using nonnegativity of $\sqrt{2}$ and $\sqrt{3}$.
proof idea
One-line term proof. Apply ne_of_gt to the instance stencilMomentTensor_diag_pos 0, which supplies $0 < (A_0){00}$. Strict positivity immediately yields $(A_0){00}\neq 0$. No further algebraic work.
why it matters
Nondegeneracy of $A_0$ is the first algebraic gate before continuum ellipticity of the anisotropic stencil operator. The module already has the exact closed form $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ and diagonal positivity; this theorem packages the $(0,0)$ entry as an explicit nonzero witness usable in later invertibility or coercivity arguments.
It sits inside the tensor-first anisotropic action continuum limit (candidate C8, Phase 2b). The companion stage-2 module develops the energy limit; the pillar-2 path-sum flag remains red and is out of scope here. No downstream consumers are wired yet, so this is a preflight lemma waiting on the continuum-limit chain.
Framework context: discrete gravity on the Freudenthal family, not the T0–T8 forcing chain or the mass ladder. The result is pure stencil linear algebra supporting the Regge-to-continuum bridge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.