stencilWeight
plain-language theorem explainer
Defines the seven displacement-class stencil weights as square roots of the Freudenthal periodic squared edge lengths: three axis edges weight 1, three face diagonals √2, one body diagonal √3. Anyone writing the continuum limit of the frozen Regge Hessian on the canonical periodic triangulation cites this. The body is a one-line definitional square root of periodicDispSqEdge.
Claim. For each displacement class $d \in \{0,\ldots,6\}$, the stencil weight is $c_d := \sqrt{\ell_d^2}$, where $\ell_d^2$ is the squared edge length of that class on the canonical periodic Freudenthal triangulation ($\ell_d^2 \in \{1,1,1,2,2,2,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 target identity equates the canonical Regge-Hessian quadratic form to a seven-class nearest-displacement stencil $\sum_x \sum_d c_d,(u(x+d)-u(x))^2$.
The seven classes are the positive displacements on the 3-torus lattice: three axis steps (squared length 1), three face diagonals (squared length 2), and one body diagonal (squared length 3). Upstream, periodicDispSqEdge records exactly those squared lengths as a function of the class index. On the canonical periodic triangulation the global squared edge length of any edge is that of its displacement class, so the Hessian dual-weight length factor collapses to $\sqrt{\ell_d^2}$.
The weights are not free parameters. They are read off the incidence dual weights of the canonical Hessian; the continuum moment tensor $A_0=\sum_d c_d,dd^T$ is then computed exactly from them.
proof idea
Pure definition: $c_d$ is Real.sqrt applied to periodicDispSqEdge d. No tactics, no lemmas. Downstream equalities such as stencilWeight_eq_sqrt_globalSqEdge are rfl by definitional transparency once the edge is identified with its displacement class.
why it matters
This is the coefficient table for the entire Stage-1 stencil calculus. The seven-class energy freudenthalStencilEnergy multiplies each squared forward difference by these weights; the panel-locked identity freudenthal_stencil_identity normalizes that energy against the canonical Regge Hessian for all $N>2$; and stencilMomentTensor_eq evaluates $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ from the same $c_d$.
Downstream energy-limit witnesses (stencil_inner_sum_witness, freudenthalStencilEnergy_witness) evaluate the stencil on sinusoidal test fields by summing only the four classes that step in a given coordinate, with weights $1,\sqrt{2},\sqrt{2},\sqrt{3}$. Without this definition the continuum limit of the frozen quadratic form has no concrete anisotropic coefficients.
Scope remains partial: the pillar-2 path-sum flag stays red; flipping it needs the refinement-indexed measure-weighted sum over inequivalent triangulation classes. This definition only supplies the frozen-stencil weights on the canonical Freudenthal family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.