stencilMomentTensor_offDiag_pos
plain-language theorem explainer
Off-diagonal entries of the Freudenthal stencil moment tensor A₀ equal √2+√3 and are therefore strictly positive. Continuum-limit and anisotropy arguments for the frozen Regge Hessian on the periodic Freudenthal family cite this fact. The proof is a two-step rewrite through the closed form of A₀ plus positivity of √2+√3.
Claim. For all distinct spatial indices $i,j\in\{0,1,2\}$, the off-diagonal entry of the stencil moment tensor satisfies $0<(A_0)_{ij}$. Explicitly, $(A_0)_{ij}=\sqrt{2}+\sqrt{3}$ whenever $i\neq j$.
background
This module is Stage 1 of panel-locked Test G (QG full-theory campaign, Phase 2b): 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 whose weights $c_d=\sqrt{\ell_d^2}$ are $1,1,1,2,2,2,3$ for the 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}$. Its closed form is $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ with $J$ the all-ones matrix, so diagonals are $1+\sqrt{2}$ and off-diagonals are $\sqrt{2}+\sqrt{3}$. The companion positivity fact $\sqrt{2}+\sqrt{3}>0$ is already proved in-module.
proof idea
Term-mode, two steps. Rewrite the goal with the closed-form identity for the moment tensor; the $i\neq j$ hypothesis selects the off-diagonal branch, which is exactly $\sqrt{2}+\sqrt{3}$. Discharge the resulting inequality by the in-module lemma that $\sqrt{2}+\sqrt{3}>0$ (via simpa). No case analysis on the seven displacement classes is repeated here; that work lives in the closed-form identity.
why it matters
This is the quantitative positivity half of the FINDING that $A_0$ is anisotropic. The sole downstream consumer is stencilMomentTensor_not_isotropic, which shows $A_0\neq c\cdot I$ for every scalar $c$ by comparing the off-diagonal entry against zero. That anisotropy is intentional: Stage 1 of Test G is the tensor-first anisotropic action continuum limit on the Freudenthal family, not an isotropic Laplacian claim.
In the broader Recognition gravity stack this sits under the Regge-action concrete path (canonical Hessian equals graph Dirichlet energy, then edge-stencil reindexing). It does not touch the still-red pillar-2 path-sum flag; that requires a refinement-indexed measure-weighted sum over inequivalent triangulation classes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.