d2_damped_schedule_closure_one_statement
plain-language theorem explainer
For any varying-cardinality six-tet refinement family and schedule σ→0, the damped family keeps the same quadrature proxies, satisfies residual vanishing on the product filter with no supplied analytic field, and full nonlinear Regge to continuum convergence follows from the quadrature limit alone. Gravity auditors cite this as the one-statement D2 schedule-closure package. The proof is a three-conjunct term packing three prior lemmas.
Claim. Let $F$ be a canonical periodic six-tet volume-quadrature refinement family along a filter $\ell$, and let $\sigma\to 0$ along $\ell$ with $\sigma$ eventually nonzero. Write $F^\sigma$ for the family with the same cardinalities, probes, and limiting cell volumes, but with within-slice spacing damped by $\sigma$. Then: (i) every slice of $F^\sigma$ has the same finite quadrature proxy as $F$; (ii) the uniform residual-vanishing target holds for $F^\sigma$ on any refinement filter; (iii) if the quadrature proxies of $F$ converge to a continuum integral $I$, then the full nonlinear Regge aggregate of $F^\sigma$ tends to $I$ on the product filter.
background
The D2 product-filter datum originally carried two analytic inputs as supplied fields: quadrature proxies converging to the continuum EH/Dirichlet integral across cardinalities, and uniform vanishing of the (full nonlinear Regge minus quadrature) residual on the product filter. The scoping audit names these as the two remaining targets.
This module discharges the residual target from the primitive curvature bound alone. Every cardinality slice already carries Track 1.B local correspondence: a cubic Taylor bound on the Regge deficit inside a local radius. From the slice witnesses, probe norms, and limiting cell volume one builds a damping factor so scaled probes stay inside the local ball and the per-slice residual coefficient is dominated by a slice-independent envelope $|\sigma(t)|$.
The damped family keeps cardinalities, probes, and quadrature proxies fixed while replacing within-slice spacing by $\sigma(t)$ times that factor. Upstream, residual vanishing for the damped family is already a theorem, and full product-filter convergence reduces to the quadrature limit alone.
proof idea
Term-mode triple conjunction, no tactics.
First conjunct: pointwise on each refinement index, apply the slice lemma that damping leaves the finite quadrature proxy unchanged.
Second conjunct: invoke the theorem that the residual-vanishing target holds for every damped family built from a universal schedule $\sigma\to 0$, with the bound assembled from each slice's local-correspondence witnesses and the constructed spacing damping.
Third conjunct: for an arbitrary continuum integral, assume the quadrature-convergence target on the undamped family and apply the reduction theorem stating that, for the damped family, that single analytic input implies product-filter convergence of the full nonlinear Regge aggregate.
why it matters
This is the citation-facing master package for D2 open item 2 in the scoping audit: the uniform residual is derived from the primitive curvature bound once the within-slice schedule is damped, not supplied as a hypothesis field. The audit's older reduction consumed both residual vanishing and quadrature convergence; the damped-schedule path leaves only the quadrature limit as an analytic input.
The module records that full nonlinear Regge to continuum product-filter convergence for the damped family needs only that quadrature limit, closing the residual half of the D2 analytic debt with zero sorry and no RS-internal axiom. No further parent theorems currently depend on this bundle in the graph; it is the terminal one-statement export of the damped-schedule closure module.
Within Recognition gravity this sits on the discrete-to-continuum bridge for the canonical periodic six-tet cubic Dirichlet instance: local cubic control plus schedule damping yields uniform residual decay.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.