probeNormSum
plain-language theorem explainer
Sum of Euclidean norms of the tetrahedron probes on a canonical periodic six-tet volume quadrature slice. Gravity analysts cite it when assembling the per-slice damping factor that keeps scaled probes inside the local-correspondence ball. The body is a finite sum over Freudenthal tetrahedra via the periodic torus index equivalence.
Claim. For a canonical periodic six-tet volume quadrature slice $S$ along a filter, the probe-norm sum is $\sum_{\tau} \|\xi_{\tau}\|$, where the sum runs over all periodic Freudenthal tetrahedra of $S$ and $\xi_{\tau}$ is the probe vector on tetrahedron $\tau$.
background
The module discharges D2 residual-vanishing from the Track 1.B local correspondence alone: each cardinality slice already carries a cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$. No separate analytic residual field is supplied.
Periodic Freudenthal tetrahedra are the six tets inside each cubic cell of the periodic torus; they are indexed by a finite type via the canonical equivalence tetFinEquiv. Each tet carries a probe vector (edge-length or metric deviation). The sum of those norms is the first aggregate that enters the damping schedule.
Concretely the per-slice damping factor is $\min\bigl(r_S/(1+\sum_\tau|\xi_\tau|),,1/(1+K_S)\bigr)$ with $K_S$ built from the cubed-norm sum and the limiting cell volume. The linear-norm sum keeps every scaled probe inside the local radius $r_S$.
proof idea
Definition, not a proof. After installing the three NeZero instances for the slice cardinalities, it is the finite sum over Fin (card (PeriodicTet Nx Ny Nz)) of the Euclidean norm of tetProbe at the tetrahedron recovered by tetFinEquiv. No lemmas are applied.
why it matters
This aggregate is the denominator ingredient of the damping factor: dampingFactor S = min (localRadius S / (1 + probeNormSum S)) (1 / (1 + residualCoefficient S)). Downstream, one_add_probeNormSum_pos and probeNormSum_nonneg guarantee the quotient is well-defined and positive, and dampingFactor_le_radius_quotient records the first min-branch.
That damping is what forces dampedSlice_residual_abs_le: the full nonlinear Regge aggregate minus the quadrature proxy is bounded by $|\sigma t|$ uniformly in the slice. Closing the residual this way discharges D2 open item 2 of the scoping audit (uniform residual vanishing) without a supplied analytic field, so the product-filter continuum limit for the damped family needs only the quadrature target.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.