probeNormSum_nonneg
plain-language theorem explainer
The sum of probe norms over the tetrahedra of a canonical periodic six-tet volume quadrature slice is nonnegative. Gravity and ILG analysts cite it when building the damped within-slice schedule that keeps every scaled probe inside the local-correspondence ball. The proof is a one-line application of Finset.sum_nonneg to the nonnegativity of the Euclidean norm.
Claim. For any filter $l$ on a type $\alpha$ and any canonical periodic six-tet volume quadrature slice $S$ along $l$, the sum of the Euclidean norms of the slice probes satisfies $0 \le \sum_\tau \|\xi_\tau\|$.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual-vanishing target for the full nonlinear Regge-minus-quadrature difference. Rather than supply that target as a hypothesis field, the module builds a damped family whose within-slice spacing is scaled by a factor
$d_S = \min\bigl(r_S/(1+\sum_\tau|\xi_\tau|),, 1/(1+K_S)\bigr)$
computed from the slice's own local-correspondence witnesses $(r_S,C_S)$, its probe norms, and its limiting cell volume. The cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$ then forces the residual below a slice-independent envelope $|\sigma(t)|$.
The quantity $\mathrm{probeNormSum},S$ is exactly the sum of probe norms $\sum_\tau|\xi_\tau|$ appearing in the first factor of $d_S$. Nonnegativity of that sum is the elementary positivity fact needed before one can form the reciprocal $1/(1+\sum|\xi_\tau|)$ and keep every scaled probe inside the local ball.
proof idea
Install the three NeZero instances for the slice cardinalities $N_x,N_y,N_z$ so the finite index set of tetrahedra is well-formed. Then apply Finset.sum_nonneg with the pointwise witness norm_nonneg on each probe. No further algebraic identity is required.
why it matters
Feeds the immediate parent one_add_probeNormSum_pos, which upgrades nonnegativity to the strict inequality $1+\sum|\xi_\tau|>0$ used in the denominator of the damping factor $d_S$. That factor is the device by which the module discharges D2 residual vanishing from the Track 1.B local correspondence alone, with no supplied analytic residual field. Downstream, the damped family inherits the same quadrature proxies while the product-filter residual tends to zero, so full nonlinear Regge-to-continuum convergence reduces to the quadrature limit. In the broader Recognition gravity stack this is bookkeeping that keeps the ILG discrete-to-continuum bridge free of extra axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.