continuumTarget_pos
plain-language theorem explainer
The continuum energy target A₀[0,0]·2π² is strictly positive. Anyone citing the Freudenthal witness energy limit needs this gate so the lattice-to-continuum comparison is not a vacuous 0=0 identity. The proof unfolds the constant and multiplies two strictly positive factors: the (0,0) stencil moment and 2π².
Claim. Let $A_0$ be the stage-1 stencil moment tensor and set the continuum target $E_\infty := A_0[0,0]\cdot 2\pi^2$. Then $E_\infty > 0$.
background
This module runs 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^2$ witness $f(x,y,z)=\sin(2\pi x)$. Stage 1 supplies the moment tensor $A_0$ with diagonal entries $1+2\sqrt{2}+\sqrt{3}$.
The continuum target is defined independently of any lattice sum as the cube integral $\int_{[0,1]^3}\langle\nabla f,A_0\nabla f\rangle$. Because the integrand depends only on the first coordinate, it collapses to $A_0[0,0]\cdot 2\pi^2$. Upstream, stencilMomentTensor_diag_pos already proves every diagonal entry of $A_0$ is strictly positive.
Gate (vi) exists to rule out a degenerate witness whose continuum energy vanishes, which would make the rate bound hold trivially.
proof idea
Term-mode after a one-line unfold of the continuum target into $A_0[0,0]\cdot(2\pi^2)$. Apply real multiplication-positivity to the product of two factors: the diagonal positivity lemma at index $0$ (so $A_0[0,0]>0$), and a positivity subproof for $2\pi^2$ (using $\pi>0$). No integral work is needed here; the integral identity is certified elsewhere.
why it matters
Panel-locked Test G stage 2 requires a nonzero continuum limit so the observable $|E_N-E_\infty|\le C/N$ is a genuine convergence statement rather than $0=0$. The status record EnergyLimitStatus records this gate alongside the closed-form lattice evaluation and the explicit rate constant $C=A_0[0,0]\cdot(2\pi)^4/24$.
Together with the independent definition of the continuum target and the exact lattice closed form $A_0[0,0]\cdot 2N^2\sin^2(\pi/N)$, this positivity finishes the nondegeneracy half of the tensor-first anisotropic action continuum limit on the Freudenthal family. Scope remains partial: the pillar-2 path-sum flag stays red until a refinement-indexed measure-weighted sum over triangulation classes is available.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.