dampedSlice
plain-language theorem explainer
Builds a damped copy of a periodic tet-six-tet volume quadrature slice: same grid sizes, probes, local correspondence, and limiting cell volume, but with cell volumes frozen at the limit and spacing equal to a universal schedule σ scaled by the slice's own damping factor. Gravity analysts cite it when discharging uniform residual vanishing from the cubic Taylor bound alone. Construction is a structure copy with spacing rewritten as σ·d_S and the two spacing filter hypotheses discharged by const-tendsto and mul_ne_zero.
Claim. Given a canonical periodic tet-six-tet volume quadrature slice $S$ along a filter $\ell$, and a schedule $\sigma:\alpha\to\mathbb{R}$ with $\sigma\to 0$ along $\ell$ and $\sigma$ eventually nonzero, form a new slice with the same cardinalities $N_x,N_y,N_z$, the same local-correspondence witness, the same tet probes, and cell volume fixed at $S$'s limiting cell volume, while the spacing schedule is $u\mapsto \sigma(u)\cdot d_S$ where $d_S$ is the per-slice damping factor of $S$.
background
Module D2DampedScheduleClosure closes D2 open item 2 from the scoping audit: the uniform residual-vanishing target that the product-filter datum previously carried as a supplied analytic field. Every cardinality slice already carries Track 1.B local correspondence, the cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ for $|\xi|<r$. That bound alone forces the two-scale residual to vanish once within-slice refinement is damped per slice.
The per-slice damping factor is $d_S=\min\bigl(r_S/(1+\sum_\tau|\xi_\tau|),,1/(1+K_S)\bigr)$ with $K_S=(|V_S|/6),C_S\sum_\tau|\xi_\tau|^3$, built from the local radius, cubic constant, probe norms, and limiting cell volume. The first factor keeps every scaled probe inside the local-correspondence ball; the second shrinks the residual coefficient below one. Positivity of $d_S$ is recorded by dampingFactor_pos.
A quadrature slice packages finite grid sizes, a local-correspondence witness, tet probes, a cell-volume schedule tending to a limit, and a spacing schedule tending to zero and eventually nonzero. The damped slice freezes cell volume at that limit and multiplies spacing by $d_S$.
proof idea
Pure structure construction, not a proof. Copy $N_x,N_y,N_z$, their NeZero instances, the three mesh sizes, and the local-correspondence field from $S$. Rebuild the data record with: limiting cell volume unchanged; cell-volume schedule the constant function at that limit (tendsto by tendsto_const_nhds); tet probes unchanged; spacing $u\mapsto\sigma(u)\cdot\mathrm{dampingFactor}(S)$. Spacing tends to zero by Tendsto.mul_const on $h_{\sigma0}$ and the constant damping factor. Eventual nonzeroness is hσne.mono plus mul_ne_zero against dampingFactor_pos S.
why it matters
This is the per-slice primitive behind the module's closure of D2 residual vanishing. Downstream, dampedFamily applies it to every slice of a varying-cardinality refinement family under one universal schedule $\sigma$, keeping cardinalities, probes, and quadrature proxies fixed. The companion lemma dampedSlice_quadratureIntegral records that damping does not change the finite quadrature proxy. The key residual bound dampedSlice_residual_abs_le then shows that the full nonlinear Regge aggregate minus the quadrature proxy is $\le|\sigma t|$ uniformly in the slice whenever $\sigma t\ne 0$ and $|\sigma t|\le 1$, with the damping factor absorbing local radius, cubic constant, probe norms, and cell volume.
Together these feed dampedFamily_uniformResidual (no supplied analytic residual field) and the master product-filter convergence for the damped family, which needs only the quadrature limit. In the Recognition gravity stack this is the analytic step that turns the cubic local bound into uniform residual control on the product filter, without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.