one_add_probeNormSum_pos
plain-language theorem explainer
One plus the sum of probe norms on a canonical periodic six-tet volume quadrature slice is strictly positive. Gravity authors cite this to keep the first branch of the per-slice damping factor well-defined and positive. The proof is a one-line linear-arithmetic step from nonnegativity of that sum.
Claim. For any canonical periodic six-tetrahedron volume quadrature slice $S$ on a filter, $0 < 1 + \sum_{\tau} \|\xi_{\tau}\|$, where the sum is the slice's total probe-norm aggregate.
background
The D2 damped-schedule module closes residual vanishing for product-filter Regge-to-continuum convergence without a supplied analytic residual field. Each cardinality slice already carries a Track 1.B local correspondence: a cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)| \le C|\xi|^3$ inside a local radius $r$. Damping rescales within-slice probes by a factor built from that radius, the cubic constant, probe norms, and limiting cell volume.
The probe-norm sum is the aggregate $\sum_\tau |\xi_\tau|$ over the slice's tetrahedra; it is already known to be nonnegative. The damping factor's first branch is $r_S/(1+\sum_\tau|\xi_\tau|)$, so the denominator must be strictly positive. That is exactly the content of this lemma. The second branch uses a residual coefficient $K_S$ built from cube-sum probes; both branches feed the min that defines the damping factor.
proof idea
Invoke the sibling nonnegativity theorem for the probe-norm sum, then close with linarith: if $0 \le s$ then $0 < 1+s$. No filter or slice structure is unpacked.
why it matters
This is a tiny positivity gate on the path that discharges D2 open item 2 (uniform residual vanishing) from the primitive curvature bound alone. Downstream, dampingFactor_pos unfolds the damping factor as a min of two positive terms and needs this lemma for the first arm; dampedSlice_residual_abs_le then bounds the full nonlinear Regge-minus-quadrature residual by $|\sigma t|$ once probes are scaled by that positive factor. Together they underwrite dampedFamily_uniformResidual and the master product-filter convergence for the damped family, so the residual target is derived rather than hypothesized. No Recognition forcing-chain landmark (T5–T8, RCL, phi) is touched; the result is pure real analysis inside the gravity D2 closure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.