continuumTarget
plain-language theorem explainer
The continuum energy target for the fixed witness field f=sin(2πx) on the unit cube is the exact constant A₀[0,0]·2π², with A₀ the Freudenthal stencil moment tensor. Anyone comparing lattice Regge-Hessian energy to its continuum limit cites this as the independent continuum side. The definition is a one-line product of the (0,0) moment entry with 2π², not a lattice-derived quantity.
Claim. Define the continuum target as the real constant $A_0[0,0]\cdot 2\pi^2$, where $A_0$ is the stencil moment tensor of the canonical Freudenthal family. This equals the cube integral $\int_{[0,1]^3}\langle\nabla f,A_0\nabla f\rangle$ for the witness $f(x,y,z)=\sin(2\pi x)$, reduced by hand to an interval integral because the integrand depends only on the first coordinate.
background
Module scope is Phase 2b of the QG full-theory campaign: the action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal family, for one fixed nonconstant C² witness. The pillar-2 path-sum flag stays red; this module only treats the sampled quadratic energy.
The stencil moment tensor $A_0=\sum_d c_d,dd^T$ is built in the stage-1 preflight from the seven Freudenthal displacement classes and their Hessian dual weights. Exact closed form: every diagonal entry is $1+2\sqrt{2}+\sqrt{3}$, every off-diagonal is $\sqrt{2}+\sqrt{3}$. The witness field is $f=\sin(2\pi x)$; its gradient is nonzero only in the first slot, so $\langle\nabla f,A_0\nabla f\rangle=A_0[0,0](2\pi\cos(2\pi x))^2$.
The continuum target is defined independently of any lattice sum, as the by-hand evaluation of that cube integral. Downstream Lean then certifies the matching interval integral via a closed-form antiderivative.
proof idea
Pure definition: multiply the $(0,0)$ entry of the stencil moment tensor by $2\pi^2$. No tactics, no lemmas in the body. The equality of this constant to the cube (equivalently interval) integral of the anisotropic energy density is proved separately in integral_witness_energy_density, using the antiderivative identity for $\cos^2(2\pi t)$ and the section derivative of the witness.
why it matters
This constant is the continuum side of the panel-locked stage-2 observable. The rate theorem freudenthal_witness_energy_limit asserts that the $\rho(N)$-normalized canonical energy of the sampled witness converges to this target at explicit rate $C/N$ with $C=A_0[0,0]\cdot(2\pi)^4/24$. Positivity (continuumTarget_pos) rules out the trivial $0=0$ trap. Status record EnergyLimitStatus flags that the target is defined independently and the integral is Lean-checked. Together with the exact lattice closed form $A_0[0,0]\cdot 2N^2\sin^2(\pi/N)$, it closes the action-level continuum limit for this witness on the Freudenthal family (scoped partial: path-sum over triangulation classes remains open).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.