stencilWeight_eq_sqrt_globalSqEdge
plain-language theorem explainer
On the canonical periodic Freudenthal triangulation of side N, the stencil weight of an edge's displacement class equals the square root of that edge's Hessian dual-weight (global squared length). Continuum-limit and Regge-Hessian analysts cite it to identify the seven-class nearest-neighbor weights with incidence data. The proof is pure definitional equality (rfl).
Claim. For every edge $e$ of the canonical periodic Freudenthal triangulation of side length $N$, $\sqrt{\ell^2_{\mathrm{glob}}(e)} = w(\mathrm{disp}(e))$, where $\ell^2_{\mathrm{glob}}(e)$ is the Hessian dual-weight (global squared edge length) and $w$ is the stencil weight of the edge's displacement class.
background
This module is Stage 1 of panel-locked Test G in the QG full-theory campaign (Phase 2b, candidate C8): the action-level continuum limit of the frozen quadratic energy on the canonical Freudenthal family, for every side $N>2$. The quadratic form of the canonical Regge Hessian is identified with a seven-class nearest-displacement stencil $\sum_x \sum_{d\in\mathrm{Fin},7} c_d,(u(x+d)-u(x))^2$, with weights $c_d=\sqrt{\ell^2_d}$ read from incidence dual weights ($\ell^2\in{1,1,1,2,2,2,3}$ for three axis, three face-diagonal, and one body-diagonal classes).
stencilWeight assigns to each displacement class the corresponding dual-weight length factor. globalSqEdge is the Hessian incidence dual weight on a concrete edge of the canonical periodic triangulation. The edge-to-(base, displacement) equivalence edgeFinEquiv extracts the displacement class of any edge index. The identity here is the bridge that makes those two presentations of the same length factor definitionally equal.
proof idea
Term-mode proof by rfl. Once stencilWeight is defined as the square root of the dual weight on the displacement class, and the canonical incidence data expose globalSqEdge as that same dual weight, the two sides are definitionally identical after transporting the edge through edgeFinEquiv to its displacement. No lemmas are applied; transparency of the definitions closes the goal.
why it matters
The equality is the definitional hinge between incidence geometry and the seven-class stencil that Stage 1 needs before any continuum or moment-tensor work. Module goals that sit on top of it include the exact stencil identity hessianQuadratic_canonical_eq_freudenthalStencil (Regge Hessian quadratic form equals the weighted nearest-displacement sum) and the a-priori normalized identity freudenthal_stencil_identity with $\rho(N)=1/N$ and $h=1/N$. Sibling facts then list the seven explicit values $\sqrt{1},\sqrt{1},\sqrt{1},\sqrt{2},\sqrt{2},\sqrt{2},\sqrt{3}$ and nonnegativity, and compute the moment tensor $A_0=\sum_d c_d,dd^T=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$.
No used-by edges are recorded yet; the declaration is infrastructure inside the preflight panel rather than a leaf citation. Scope remains partial: the pillar-2 path-sum flag stays red until a refinement-indexed measure-weighted sum over inequivalent triangulation classes is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.