d2_reduction
plain-language theorem explainer
On the canonical periodic six-tet cubic torus, quadrature convergence to the continuum EH/Dirichlet integral plus a vanishing full-nonlinear-Regge residual together force the full Regge aggregate to tend to that continuum integral on the product filter. Gravity auditors and anyone citing the D2 classical-recovery witness use this as the honest reduction. The proof is a one-line packaging of the two hypotheses into the product-filter datum and a call to the existing triangle-inequality squeeze.
Claim. Let a canonical periodic six-tet volume-quadrature refinement family be given, together with a refinement filter and a continuum integral $I\in\mathbb{R}$. If the six-tet quadrature rule converges to $I$ on the cross-cardinality product schedule, and if the (full nonlinear Regge minus quadrature) residual vanishes uniformly on the product filter, then the full nonlinear Regge aggregate tends to $I$ along the product of the refinement filter with the base filter.
background
This module is the honest D2 (Regge → Einstein-Hilbert) scoping audit for Recognition Science gravity. The classical-recovery witness consumed by the master theorem is a universal statement over product-filter data packages: each package carries a refinement family on the canonical periodic six-tet cubic torus, a continuum integral, and two analytic fields.
Those fields are exactly the named remaining targets. Quadrature convergence asserts that the six-tet volume quadrature rule tends to the continuum EH/Dirichlet integral on the cross-cardinality product schedule. Residual vanishing asserts that the difference between the full nonlinear Regge action and that quadrature is uniformly controlled on the product filter.
Upstream, the product-filter datum structure already proves that those two fields imply full Regge → continuum convergence by a triangle-inequality squeeze (fullReggeProduct_tendsto_continuum). The present declaration simply externalizes that implication so the open analytic work is not buried inside a structure field.
proof idea
Term-mode one-liner. Build a CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData record whose family, refinementFilter, and continuumIntegral are the theorem parameters, and whose quadrature_tendsto and uniform_residual fields are the two named hypotheses. Apply fullReggeProduct_tendsto_continuum to that record; the conclusion is exactly the required Filter.Tendsto of the full Regge aggregate along the product filter to the continuum neighborhood filter.
why it matters
This is the proved content of D2 classical recovery: not a from-primitives closure, but a clean reduction of full nonlinear Regge → continuum EH convergence to two named analytic inputs. Downstream, d2_reduction_statement repackages the same fact as a single implication for citation. The master theorem's concrete physical Regge-EH continuum proposition is discharged precisely by the squeeze that this reduction exposes.
In the broader RS gravity stack, D2 is the continuum bridge from discrete Regge data on the six-tet cubic torus toward Einstein-Hilbert. The module status is theorem with zero sorry for what is claimed; the open frontier (quadrature from mesh geometry, residual envelope from curvature bounds) is named rather than asserted. No claim is made about non-product or non-flat triangulations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.