scaledCanonicalEnergy
plain-language theorem explainer
Defines the ρ(N)-normalized canonical quadratic energy of a scalar field on the side-N periodic Freudenthal triangulation of the unit 3-torus. Gravity continuum-limit arguments sample continuum fields into this quantity and compare it to ∫⟨∇f, A₀∇f⟩. The body is a one-line product of the a-priori factor 1/N with the Regge Hessian quadratic form on the potential lift of u.
Claim. For $N \ge 1$ and a real field $u$ on the $N^3$ periodic cubic vertices, the scaled canonical energy is $\rho(N)\, Q_N(u)$, where $\rho(N)=1/N$ and $Q_N(u)$ is the quadratic form of the canonical Regge Hessian of the side-$N$ periodic Freudenthal triangulation, evaluated on the potential lift of $u$.
background
This module is Stage 1 of panel-locked Test G (QG full-theory campaign, Phase 2b): the action-level continuum limit of the frozen quadratic energy on the canonical Freudenthal family, for every side length $N>2$. Vertices are the periodic cubic lattice $\mathrm{Fin},N\times\mathrm{Fin},N\times\mathrm{Fin},N$. The triangulation skeleton is the concrete finite periodic Freudenthal complex; incidence consistency is the packaged wraparound certificate.
The canonical Regge Hessian is the graph-Laplacian matrix induced by incidence dual weights: diagonal row-sums of dual weights, off-diagonal minus the dual weight. Its quadratic form is $\sum_{i,j} H_{ij}\xi_i\xi_j$. The a-priori normalization $\rho(N)=1/N$ is dimensional, not fitted: each Hessian summand carries one hinge-measure length $\sqrt{\ell_d^2}$ at spacing $h=1/N$, so the physical density $h^3\sum c_d((\Delta u)/h)^2$ differs from the raw quadratic form by exactly one power of $h$.
Stage 1 proves that this quadratic form equals the seven-class nearest-displacement stencil $\sum_x\sum_{d\in\mathrm{Fin},7} c_d(u(x+d)-u(x))^2$ with $c_d=\sqrt{\ell_d^2}$ for axis, face-diagonal, and body-diagonal classes ($\ell^2\in{1,1,1,2,2,2,3}$).
proof idea
Pure definitional composition, no tactics. Multiply stencilNormalization N ($=1/N$) by hessianQuadratic of canonicalReggeHessian on canonicalPeriodicTriangulation N N N under canonicalPeriodicIncidenceConsistent, evaluated at toPotential N u (the Fin-indexed potential lift of the vertex field $u$). Downstream identities rewrite this product as the $\rho(N)$-scaled seven-class stencil energy.
why it matters
This is the Stage-2 sampling target for the Freudenthal energy continuum limit. Downstream, scaledCanonicalEnergy_eq_scaled_stencil equates it to the normalized stencil sum; scaledCanonicalEnergy_witness_closed_form gives the exact closed form $A_0[0,0]\cdot 2N^2\sin^2(\pi/N)$ on the sine witness; scaledCanonicalEnergy_witness_rate and freudenthal_witness_energy_limit prove the panel-locked rate $|E_N-\int\langle\nabla f,A_0\nabla f\rangle|\le C/N$ for $N\ge 3$.
It sits inside the tensor-first anisotropic action continuum limit (candidate C8), not the path-sum pillar (still red: refinement-indexed measure-weighted sums over inequivalent triangulation classes remain open). The moment tensor $A_0=(1+\sqrt{2})I+(\sqrt{2}+\sqrt{3})J$ computed in this module is the continuum anisotropy that the scaled energy is designed to recover.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.