dampedFamily
plain-language theorem explainer
Damps every cardinality slice of a varying-cardinality Regge quadrature refinement family by one universal schedule σ → 0. Cardinalities, probes, and quadrature proxies are left unchanged; only within-slice spacing is scaled. Downstream D2 closure results cite this construction to derive the product uniform residual from local cubic Taylor data alone. The body is a one-line slicewise application of the damped-slice map.
Claim. Given a canonical periodic tet-six-tet volume quadrature refinement family $F$ along a filter $\ell$, and a schedule $\sigma:\alpha\to\mathbb{R}$ with $\sigma\to 0$ along $\ell$ and $\sigma$ eventually nonzero, form the damped family whose slice at each refinement index is the corresponding slice of $F$ with within-slice spacing scaled by $\sigma$. Cardinalities, probes, and quadrature proxies are identical to those of $F$.
background
The module closes D2 open item 2 from the scoping audit: the product-filter residual-vanishing target had been carried as a supplied analytic hypothesis. Each 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 local bound alone forces the two-scale residual to vanish once within-slice spacing is damped.
A canonical periodic tet-six-tet volume quadrature refinement family packages, for each refinement index, a fixed-cardinality Regge slice with probes, limiting cell volumes, and quadrature proxies. The damping factor on a slice is built from the slice's own local-correspondence witnesses $(r_S,C_S)$, probe norms, and limiting cell volume: $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$.
The damped family keeps every scaled probe inside the local-correspondence radius and shrinks the per-slice residual coefficient below a slice-independent envelope $|\sigma(t)|$, while leaving quadrature proxies untouched.
proof idea
Definitional construction, not a proof. The returned family reuses the same filter and parameter type as $F$, and sets each slice to the image of $F$'s slice under the damped-slice map at the common schedule $\sigma$ (with the given tendsto-zero and eventually-nonzero hypotheses). All structure fields other than the within-slice spacing schedule are inherited unchanged from the base slices.
why it matters
This is the central object of the D2 damped-schedule closure. It feeds dampedFamily_uniformResidual, which discharges the residual-vanishing target with no supplied analytic residual field, and dampedFamily_quadrature_target, which inherits the cross-cardinality quadrature limit because proxies are preserved. Those two facts yield dampedFamily_fullReggeProduct_tendsto_continuum and the reduction d2_reduction_to_quadrature_only: full nonlinear Regge-to-continuum product-filter convergence for the damped family needs only the quadrature limit. The one-statement bundle d2_damped_schedule_closure_one_statement packages the same story for citation, and the flat-sector instance path in D2QuadratureInstances reuses the construction. In the audit vocabulary, item 2 is derived from the primitive curvature bound rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.