Pith. sign in
theorem

stencilWeight_nonneg

proved
show as:
module
IndisputableMonolith.Gravity.Analysis.FreudenthalStencilPreflight
domain
Gravity
line
103 · github
papers citing
none yet

plain-language theorem explainer

The seven Freudenthal nearest-displacement stencil weights are nonnegative. Anyone building the moment tensor A₀ = Σ c_d d dᵀ or the continuum quadratic form cites this for the positivity half of the PSD argument. The proof is a one-line appeal to nonnegativity of the real square root.

Claim. For every displacement class $d \in \{0,\ldots,6\}$, the stencil weight $c_d$ satisfies $0 \le c_d$.

background

This module is Stage 1 of panel-locked Test G (QG full-theory campaign, Phase 2b, candidate C8): the action-level continuum limit of the frozen quadratic energy on the canonical periodic Freudenthal triangulation, for every side length $N > 2$. The quadratic form of the canonical Regge Hessian is identified with the seven-class nearest-displacement stencil $\sum_x \sum_{d} c_d ,(u(x+d)-u(x))^2$, with weights $c_d = \sqrt{\ell_d^2}$ read from the Hessian incidence dual weights ($\ell^2 \in {1,1,1,2,2,2,3}$ for the three axis, three face-diagonal, and one body-diagonal classes).

Vertices live on the periodic cubic torus $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$. A positive-displacement periodic edge is a pair (base, class) with class in $\mathrm{Fin},7$; shifting the base by that class is the map that matches the edge endpoints. The stencil weight is the coefficient $c_d$ attached to each of those seven classes; by construction it is a real square root of a squared edge length.

proof idea

One-line term proof. The weight is definitionally a real square root of a nonnegative squared length, so Real.sqrt_nonneg discharges $0 \le c_d$ for every class $d$. No case split on the seven classes is required.

why it matters

Direct input to stencilMomentTensor_psd, which proves the moment tensor $A_0 = \sum_d c_d, d d^\top$ is positive semidefinite: after rewriting the quadratic form as a sum over classes, each term is a product of $c_d$ and a square, and nonnegativity of $c_d$ supplies the first factor. That PSD fact sits inside the tensor-first anisotropic continuum limit (Test G stage 1): the exact identity $A_0 = (1+\sqrt{2})I + (\sqrt{2}+\sqrt{3})J$ and the normalized stencil energy both need nonnegative weights before any $N\to\infty$ analysis. The module is axiom-clean and proved; the separate 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.