stencilWeight_values
plain-language theorem explainer
The seven Freudenthal displacement-class stencil weights evaluate exactly to 1, 1, 1, √2, √2, √2, √3. Anyone citing the canonical Regge Hessian as a nearest-neighbor stencil on the periodic Freudenthal torus needs these closed forms. The proof is a seven-way refine that unfolds the definition and runs norm_num on the squared lengths and √1.
Claim. For the seven displacement classes on the canonical periodic Freudenthal triangulation, the stencil weights (square roots of the class squared edge lengths) are $w_0 = w_1 = w_2 = 1$, $w_3 = w_4 = w_5 = \sqrt{2}$, and $w_6 = \sqrt{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 Freudenthal family, for 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:0\ldots 6} c_d,(u(x+d)-u(x))^2$.
The squared edge lengths by positive displacement class are the definitional table periodicDispSqEdge: three axis classes with $\ell^2=1$, three face-diagonal classes with $\ell^2=2$, and one body-diagonal class with $\ell^2=3$. The stencil weight of class $d$ is defined as $c_d = \sqrt{\ell^2_d}$. That choice is not postulated: on the canonical periodic triangulation the Hessian dual weight sums $\sqrt{\mathrm{globalSqEdge},e}$ over incident edges, and those squared lengths reduce exactly to the displacement-class table.
The present lemma simply records the seven numerical values of those square roots.
proof idea
Term-mode proof by a single refine that splits the seven-way conjunction, then a shared norm_num tactic on each goal. Unfolding stencilWeight and periodicDispSqEdge reduces each goal to evaluating $\sqrt{1}$, $\sqrt{2}$, or $\sqrt{3}$; Real.sqrt_one discharges the three axis cases. No intermediate lemmas are required beyond the two definitions.
why it matters
These explicit weights are the $c_d$ that appear in the panel-locked stencil identity $\rho(N),Q_N(u)=h^3\sum_x\sum_d c_d\bigl((u(x+d)-u(x))/h\bigr)^2$ with $h=1/N$ and $\rho(N)=1/N$, and in the exact moment tensor $A_0=\sum_d c_d,dd^\top=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$. Downstream continuum-limit and anisotropy analysis in this module and its stage-2 companion (FreudenthalEnergyLimit) treat the seven coefficients as known constants rather than symbolic placeholders.
In the broader Recognition gravity stack this is preflight arithmetic for the tensor-first anisotropic action continuum limit (candidate C8), not a forcing-chain step. The pillar-2 path-sum flag remains red; this lemma does not touch measure-weighted sums over triangulation classes. No used_by edges are recorded yet, so its immediate consumers are sibling identities in the same preflight file (nonnegativity, energy reindexing, moment tensor).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.