probeCubeSum
plain-language theorem explainer
Finite sum of cubed probe norms over every periodic Freudenthal tetrahedron in a canonical six-tet volume quadrature slice. Gravity analysts cite it when building the per-slice residual coefficient that damps the within-slice schedule. The body is a plain Fin-indexed sum of Euclidean cubed norms, after installing the slice's NeZero cardinality instances.
Claim. For a canonical periodic six-tetrahedra volume quadrature slice $S$ along a filter, the probe cube sum is $\sum_{\tau} \|\xi_{\tau}\|^3$, where the sum runs over a finite index of the periodic Freudenthal tetrahedra of $S$ and $\xi_{\tau}$ is the probe attached to tetrahedron $\tau$.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual-vanishing target for product-filter Regge-to-continuum convergence. Each cardinality slice already carries a Track 1.B local correspondence witness, the cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$. From that bound alone one builds a damped within-slice schedule so the residual vanishes uniformly, with no supplied analytic field.
A slice packages grid cardinalities $(N_x,N_y,N_z)$, limiting cell volume, local radius and cubic constant, and a probe map on periodic Freudenthal tetrahedra. Those tetrahedra are the six Freudenthal tets inside each periodic cubic cell; tetFinEquiv supplies a canonical Fin index of the right cardinality. The cubed-norm sum over that index is the geometric weight that multiplies volume and $C$ in the residual coefficient.
proof idea
Definition, not a proof. Install the three NeZero instances carried by the slice so the periodic tet type is finite and nonempty, then sum $|\mathrm{tetProbe}(\tau)|^3$ over the canonical Fin enumeration of PeriodicTet N_x N_y N_z via the finite equivalence. No lemmas are applied beyond the typeclass instances and the equivalence.
why it matters
This sum is the geometric factor inside the slice residual coefficient $K_S=(|V_S|/6)\cdot C_S\cdot\sum_\tau|\xi_\tau|^3$. That coefficient, together with the local radius, defines the per-slice damping factor that keeps every scaled probe inside the local-correspondence ball and shrinks the residual below a slice-independent envelope $|\sigma(t)|$. Downstream, nonnegativity of the sum is recorded separately, and the residual coefficient feeds the damped-family construction that discharges uniform residual vanishing. The module then obtains full nonlinear Regge product-filter convergence for the damped family from quadrature convergence alone, closing the second analytic gap named in the D2 scoping audit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.