meshSize
plain-language theorem explainer
Lattice spacing $h=1/N$ for the side-$N$ canonical periodic Freudenthal family on the unit 3-torus. Anyone citing the stage-1 stencil identity or continuum limit of the Regge-Hessian quadratic form uses this as the mesh parameter. It is a one-line definitional abbreviation, not a derived claim.
Claim. For each natural number $N$, the mesh size of the side-$N$ lattice is $h = 1/N$.
background
The module develops stage 1 of panel-locked Test G in the QG full-theory campaign: the exact general-$N$ stencil identity for the frozen quadratic energy on the canonical Freudenthal triangulation of the unit 3-torus. Spatial dimension is the forced $D=3$ of the Recognition chain (T8).
Vertices of the side-$N$ periodic family sit on a cubic lattice of spacing $h=1/N$ inside the unit cube with periodic identification. Discrete differences $u(x+d)-u(x)$ become continuum gradients only after division by this $h$; the volume element scales as $h^3$. The companion normalization $\rho(N)=1/N$ is declared a priori with the same dimensional content.
Upstream geometry supplies the canonical periodic triangulation and the Regge-Hessian quadratic form; this definition simply names the lattice spacing those constructions already imply.
proof idea
Pure definition: cast $N$ to a real and invert. No lemmas, no tactics.
why it matters
Feeds the panel-locked stage-1 identity freudenthal_stencil_identity, which equates the normalized canonical Regge-Hessian quadratic form to the seven-class Freudenthal stencil
$\rho(N),Q_N(u)=h^3\sum_x\sum_d c_d\bigl((u(x+d)-u(x))/h\bigr)^2$
with $h=\mathrm{meshSize},N$. Without a named mesh size the continuum scaling $h^3$ and the difference quotients cannot be written cleanly.
That identity is the exact finite-$N$ input to the stage-2 continuum limit (FreudenthalEnergyLimit) and to the moment-tensor computation $A_0=\sum_d c_d,dd^T$. It sits inside the tensor-first anisotropic action path of candidate C8; the pillar-2 path-sum flag remains red and is out of scope here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.