Pith. sign in
module module high

IndisputableMonolith.Gravity.D2ScopingAudit

show as:
view Lean formalization →

Audit module that pins what the D2 gravity target actually is: Filter.Tendsto convergence of the full nonlinear Regge aggregate to the continuum Einstein–Hilbert integral, not a trivial True and not the master conclusion. Gravity workers cite it to separate the product-filter datum from residual and schedule hypotheses. Structure is definitional scoping plus named reduction statements, not a deep proof.

claimThe D2 product-filter target is the statement that the nonlinear Regge curvature aggregate converges (in the filter sense) to the continuum Einstein–Hilbert integral. The module records that this target is a genuine convergence claim, not $\mathsf{True}$, and that it does not assert the unconditional master gravity theorem. It also names the residual-vanishing and quadrature-convergence subtargets and a reduction that relates them.

background

Recognition Science gravity work routes continuum Einstein–Hilbert recovery through a discrete Regge calculus on triangulations. The unconditional master theorem needs several named inputs; D2 is the physical convergence route for the Regge aggregate under a product filter (mesh refinement and related limits).

Upstream, MasterTheoremUnconditional installs zero-argument witnesses for the five inputs of the older conditional master theorem, with D2 as the physical convergence witness. Track1BCPhysicalResidual supplies the Track 1.B-PHY structural upgrade: finite-probe Regge-to-EH residual theorems beyond a flat-substrate witness.

This module does not prove those limits. It scopes the D2 claim so later closures cannot smuggle the master conclusion or a vacuous True into the product-filter slot.

proof idea

Definition and audit module, not a single theorem proof. It introduces named targets (quadrature convergence, residual vanishing), a status record for what D2 still treats as hypothesis versus derived, and a reduction statement that the product-filter D2 datum is literally Tendsto of the nonlinear Regge aggregate to the continuum integral. Sibling declarations package that scoping; deep analytic work lives in the imported residual track and in downstream damped-schedule closure.

why it matters in Recognition Science

Without an explicit scope, D2 can be misread as either trivial or as already implying the master gravity theorem. The module blocks both errors and lists open analytic inputs the product-filter datum still carried as hypotheses.

Downstream, D2DampedScheduleClosure closes open item 2 of this audit: it derives the uniform residual on a damped schedule rather than leaving it supplied. That feeds the unconditional master surface’s D2 witness path (Session 566 physical convergence route). In the broader RS gravity stack, clean D2 scoping is what lets Regge-to-continuum convergence sit as a real analytic claim inside the forcing chain toward quantum-gravity master closure.

scope and limits

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (7)