localRadius
plain-language theorem explainer
Extracts the local-correspondence radius r_S from a cardinality slice's Track 1.B witness. Anyone building the damped schedule or residual bounds cites it as the geometric scale that keeps scaled probes inside the cubic Taylor ball. The body is a pure projection: install the three NeZero instances, then choose the radius from hLocal.
Claim. Given a canonical periodic six-tet volume quadrature slice $S$ on a filter, write $\mathrm{localRadius}(S)$ for the radius $r_S>0$ appearing in the local-correspondence cubic Taylor bound carried by $S$: $\|R(\xi)-R(0)-\tfrac12 ES(\xi)\|\le C_S\|\xi\|^3$ whenever $\|\xi\|<r_S$.
background
The module closes D2 open item 2 from the scoping audit: the uniform residual vanishing target is no longer a supplied analytic field. Every cardinality slice already carries Track 1.B local correspondence hLocal, a cubic Taylor bound
$|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$.
The pair $(r,C)$ is existential data on the slice. This definition names the radius component $r_S$. The companion cubic constant is extracted the same way as localConstant.
Downstream damping uses $r_S$ to keep every scaled probe inside the ball of validity: the first arm of the damping factor is $r_S/(1+\sum_\tau|\xi_\tau|)$. The setting is the product-filter D2 residual analysis for nonlinear Regge versus quadrature proxies on Freudenthal tori.
proof idea
Definition, not a proof. After installing the three NeZero instances for the lattice dimensions $N_x,N_y,N_z$ (required by the slice typeclass baggage), the body is simply S.hLocal.choose: classical choice of the radius witness from the existential local-correspondence hypothesis already stored on the slice.
why it matters
Without a named radius, the damped schedule cannot be written. dampingFactor takes min(localRadius S / (1 + probeNormSum S), 1/(1 + residualCoefficient S)), and dampingFactor_le_radius_quotient records the first arm. Positivity is immediate (localRadius_pos), and local_bound restates the cubic Taylor inequality on the canonical encoded torus using this radius.
Those feed normalized_regge_sub_limit_abs_le (cubic remainder over $s^2$) and ultimately dampedSlice_residual_abs_le, which bounds the full nonlinear Regge-minus-quadrature residual by $|\sigma t|$. That is the analytic step that discharges D2 residual vanishing for the damped family with no supplied residual field, leaving only quadrature convergence for the master product-filter theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.