dampedProductFilterData
plain-language theorem explainer
Master D2 product-filter datum for a damped refinement family: packages the damped family, refinement filter, continuum integral, proved quadrature limit, and derived uniform residual. Gravity and Regge analysts cite it when wiring the quantum-gravity master theorem. The body is a structure assembly that fills the two analytic fields from already-proved damped-family lemmas.
Claim. Given a canonical periodic tet-six-tet volume quadrature refinement family $F$ along a filter $\ell$, a schedule $\sigma\to 0$ that is eventually nonzero, a refinement filter on the cardinality index, a continuum integral $I$, and the cross-cardinality quadrature limit for $F$, return the product-filter datum whose family is the $\sigma$-damped version of $F$, whose continuum value is $I$, whose quadrature field is the damped quadrature target, and whose uniform residual is the derived damped residual (not an extra hypothesis).
background
This module closes D2 open item 2 from the scoping audit. The product-filter datum for D2 originally carried two analytic inputs as supplied fields: cross-cardinality quadrature convergence to the continuum integral, and uniform vanishing of the full-nonlinear-Regge-minus-quadrature residual on the product filter. The residual field is discharged here from the Track 1.B local correspondence alone.
Every cardinality slice already supplies a cubic Taylor bound $|R(\xi)-R(0)-\tfrac12 ES(\xi)|\le C|\xi|^3$ inside a local radius $r$. For any varying-cardinality family $F$ and any universal schedule $\sigma\to 0$, the damped family keeps the same cardinalities, probes, and limiting cell volumes (hence the same quadrature proxies) but rescales within-slice spacing by a per-slice factor built from $(r_S,C_S)$, probe norms, and limiting volume. That damping keeps every scaled probe inside the local radius and shrinks the residual coefficient below a slice-independent envelope $|\sigma(t)|$.
The only remaining analytic input is therefore the cross-cardinality quadrature limit. The present definition packages that input with the derived residual into the structure consumed by the master theorem.
proof idea
Pure structure assembly, not a tactic proof. The family field is the damped family of $F$ under $\sigma$. The refinement filter and continuum integral are passed through unchanged. The quadrature field is filled by the already-proved damped-family quadrature target (same continuum limit as the undamped family, since damping preserves probes and limiting volumes). The uniform residual field is filled by the derived damped-family residual lemma, which obtains product-filter vanishing from the local cubic bound and $\sigma\to 0$ alone. No new analysis is performed at this site.
why it matters
This is the concrete master-theorem D2 product-filter datum whose uniform residual is proved rather than hypothesized. It feeds three immediate consumers: the damped-schedule closure theorem (full nonlinear Regge aggregate of the damped family tends to the continuum integral on the product filter, given only quadrature), the lemma that the damped datum satisfies the Track 1.B-PHY concrete product-filter target, and the flat-instance constructor that builds the first D2 master datum with both analytic fields proved.
In the broader Recognition gravity stack this discharges D2 open item 2 of the scoping audit: residual vanishing is no longer an external analytic assumption. The construction sits downstream of the local correspondence (cubic Taylor bound on each slice) and upstream of the quantum-gravity master theorem's product-filter hypothesis. It does not touch the forcing chain T0–T8 or the J-cost uniqueness step; its role is purely the continuum limit of discrete Regge curvature under controlled refinement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.