stencilMomentTensor_symm
plain-language theorem explainer
The stencil moment tensor A₀ = Σ_d c_d d dᵀ is symmetric in its two spatial indices. Continuum-limit and PSD analyses of the Freudenthal Regge stencil cite this before reading eigenvalues or writing vᵀ A₀ v. The proof unfolds the defining sum and applies ring to the product of displacement components.
Claim. For all $i,j \in \{0,1,2\}$, the stencil moment tensor satisfies $(A_0)_{ij} = (A_0)_{ji}$, where $A_0 = \sum_{d \in D} c_d\, d\, d^{\mathsf T}$ is the $3\times 3$ matrix built from the seven canonical Freudenthal displacement classes with Hessian dual weights $c_d = \sqrt{\ell_d^2}$.
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 exactly with 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}$ equal to $1,1,1,2,2,2,3$ on the three axis, three face-diagonal, and one body-diagonal classes.
The stencil moment tensor is the continuum second-moment matrix of those weighted displacements: $A_0=\sum_d c_d, d, d^{\mathsf T}$, coded as a sum over Fin 7 of stencilWeight d * dispReal d i * dispReal d j. Its exact closed form is $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ with $J$ the all-ones matrix; symmetry of $A_0$ is the elementary structural fact needed before that evaluation and before the sum-of-squares PSD witness $v^{\mathsf T}A_0 v=\sum_d c_d\langle d,v\rangle^2$.
proof idea
Unfold the definition of the moment tensor to a finite sum over the seven displacement classes. Apply Finset.sum_congr with a trivial set identity so it remains only to check the summand pointwise: $c_d, d_i, d_j = c_d, d_j, d_i$. That equality is pure commutative ring arithmetic on $\mathbb{R}$, discharged by ring. No geometric lemmas are required.
why it matters
Symmetry of $A_0$ is a prerequisite for the exact moment-tensor evaluation and for the kernel-level PSD witness that follows in the same module (the sum-of-squares decomposition of $v^{\mathsf T}A_0 v$). Those facts underwrite the continuum limit of the frozen Freudenthal stencil energy and the tensor-first anisotropic action path (candidate C8, Test G). The module is scoped partial: pillar-2 path-sum over inequivalent triangulation classes remains red. No downstream consumers are wired yet in the graph; the lemma is local infrastructure for the preflight panel.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.