d2_reduction_statement
plain-language theorem explainer
On the canonical periodic six-tet cubic torus, quadrature convergence plus a vanishing Regge-minus-quadrature residual imply that the full nonlinear Regge product aggregate tends to the continuum Einstein-Hilbert integral on the product filter. Gravity classical-recovery arguments cite this as the packaged D2 reduction. The proof is a one-line wrapper re-exporting the core reduction lemma as a single implication.
Claim. Let $\mathcal{F}$ be a canonical periodic six-tet volume quadrature refinement family along a base filter $\ell$, with refinement filter $\rho$ and continuum integral $I\in\mathbb{R}$. If the six-tet quadrature rule converges to $I$ on the cross-cardinality product schedule, and the full nonlinear Regge-minus-quadrature residual is uniformly controlled on the product filter, then the full Regge product aggregate tends to $I$ along $\rho\times\ell$.
background
This module audits the honest status of D2 classical recovery (Regge calculus to continuum Einstein-Hilbert) inside the gravity master theorem. The D2 witness consumed downstream is a product-filter Tendsto statement: the full nonlinear Regge aggregate converges to the continuum EH/Dirichlet integral. That Tendsto is not free; it is discharged by combining two analytic inputs carried on the product-filter datum.
The first input, packaged here as the quadrature-convergence target, asserts that the canonical periodic six-tet quadrature rule converges to the continuum integral on the cross-cardinality product schedule. The second, the residual-vanishing target, asserts that the full nonlinear Regge-minus-quadrature residual is uniformly controlled on the product filter. The module doc states the reduction cleanly: on this mesh family, those two hypotheses imply full Regge-to-continuum EH convergence via a triangle-inequality squeeze.
The local setting is deliberately scoped: the reduction is proved with zero sorry; the two analytic inputs and any general-triangulation extension remain named open targets, not hidden fields.
proof idea
One-line term-mode wrapper. Given hypotheses hquad (quadrature convergence target) and hres (residual vanishing target), the proof applies the sibling lemma d2_reduction at the same family, refinement filter, and continuum integral, forwarding both hypotheses unchanged. No new analytic work occurs here; the declaration exists only to expose the reduction as a single citable implication arrow.
why it matters
D2 is the classical-recovery leg of the unconditional gravity master theorem: full nonlinear Regge must recover continuum Einstein-Hilbert on the product filter. This declaration is the peer-review-facing packaging of that reduction (module findings F2 / Rec 3), so citations need not dig into the internal product-filter datum fields.
Downstream, d2_residual_vanishing_target_damped in the damped-schedule closure module states the residual target in exactly this vocabulary, discharging residual vanishing for damped schedules built from local curvature bounds and spacing damping. The reduction then becomes the bridge from those schedule results (and any future quadrature discharge) to the master-theorem Tendsto.
Within Recognition Science gravity, this pins what is actually proved versus open: the squeeze is closed; mesh-primitive quadrature convergence and general-triangulation extension remain the named frontier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.