rateConstant_nonneg
plain-language theorem explainer
The explicit continuum-limit rate constant C = A₀[0,0]·(2π)⁴/24 is nonnegative. Anyone invoking the stage-2 Freudenthal energy rate bound needs this sign gate. The proof unfolds the definition and multiplies three nonnegative factors: the positive diagonal moment-tensor entry, a positive power of 2π, and the reciprocal of 24.
Claim. Let $A_0$ be the stencil moment tensor of the canonical Freudenthal displacement classes. The rate constant $C := A_0[0,0]\cdot(2\pi)^4/24$ satisfies $C \ge 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 the fixed nonconstant witness $f(x,y,z)=\sin(2\pi x)$.
The stencil moment tensor $A_0=\sum_d c_d,dd^T$ is assembled in the stage-1 preflight; every diagonal entry equals $1+2\sqrt{2}+\sqrt{3}>0$ (stencilMomentTensor_diag_pos). Independently of the lattice, the continuum target is $\int_{[0,1]^3}\langle\nabla f,A_0\nabla f\rangle=A_0[0,0]\cdot 2\pi^2$.
The rate constant is the $N$-independent prefactor $C=A_0[0,0]\cdot(2\pi)^4/24$ that multiplies $1/N$ (in fact the closed form yields the sharper $1/N^2$) in the panel-locked stage-2 observable.
proof idea
Unfold rateConstant to $A_0[0,0]\cdot(2\pi)^4/24$. Obtain $A_0[0,0]\ge 0$ from le_of_lt on stencilMomentTensor_diag_pos 0. The power $(2\pi)^4$ is nonnegative by positivity. Conclude with div_nonneg on the product over the positive constant 24 (norm_num).
why it matters
Feeds directly into scaledCanonicalEnergy_witness_rate, the panel-locked stage-2 bound
$|E_N(\mathrm{sample},f)-\mathrm{continuumTarget}|\le C/N$
with this explicit $C$. Without nonnegativity the absolute-value comparison is ill-typed as a rate. The module is axiom-clean THEOREM status for candidate C8 (tensor-first anisotropic action continuum limit); the pillar-2 path-sum flag remains red and is out of scope here. Landmark contact is the discrete-to-continuum energy limit on the Freudenthal family, not the T0–T8 forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.