localRadius_pos
plain-language theorem explainer
Any cardinality slice carries a strictly positive local-correspondence radius. D2 gravity analysts cite this when forming the per-slice damping factor that keeps scaled probes inside the cubic Taylor ball. The proof is a direct unpack of the existential witness already stored on the slice's local-correspondence field.
Claim. For every canonical periodic tet-six-tet volume quadrature slice $S$ on a filter, writing $r_S$ for the local-correspondence radius extracted from $S$, one has $0 < r_S$.
background
The D2 damped-schedule module discharges the residual-vanishing target that earlier product-filter data carried as a supplied analytic field. Each cardinality slice already stores a Track 1.B local correspondence: there exist $r>0$ and $C\ge 0$ such that $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ whenever $|\xi|<r$.
The definition localRadius simply projects out that radius $r_S$ from the slice's local-correspondence witness. The companion cubic constant and the probe-norm sums then enter the damping factor
$d_S=\min\bigl(r_S/(1+\sum_\tau|\xi_\tau|),,1/(1+K_S)\bigr)$,
which rescales within-slice spacing so every probe stays inside the Taylor ball and the residual coefficient collapses under any schedule $\sigma\to 0$.
Positivity of $r_S$ is the first arithmetic fact needed before $d_S$ itself can be shown positive and before residual bounds can be stated.
proof idea
Term-mode unpack. The three NeZero instances for the slice grid sizes are restored so that localRadius typechecks, then the proof returns the first conjunct of the second choose_spec on the slice's local-correspondence hypothesis: that hypothesis is an existential pair $(r,C)$ with $0<r$, and localRadius is defined to be that $r$. No further lemma is applied.
why it matters
This positivity is consumed immediately by dampingFactor_pos (the min of two positive terms is positive) and by dampedSlice_residual_abs_le, which bounds the full nonlinear Regge-minus-quadrature residual of the damped slice by $|\sigma t|$ uniformly in the slice. Together those results let the module replace the supplied residual-vanishing field of D2ScopingAudit by a derived statement: once the schedule is damped from the local cubic bound alone, the product-filter residual target holds with no extra analytic hypothesis. That is open item 2 of the D2 scoping audit, and it clears the path to full Regge-to-continuum product-filter convergence for the damped family.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.