Pith. sign in
module module high

IndisputableMonolith.Gravity.D2ScopingAudit

show as:
view Lean formalization →

The D2 product-filter target is scoped as genuine filter-limit convergence of the full nonlinear Regge aggregate to the continuum Einstein-Hilbert integral, not a trivial True placeholder and not the master gravity conclusion. Gravity auditors cite this module to separate the analytic D2 obligation from the unconditional master-theorem surface. It records reduction statements and named status flags for the two open analytic inputs later discharged downstream.

claimThe D2 product-filter target asserts $\mathrm{Tendsto}$ convergence of the full nonlinear Regge curvature aggregate to the continuum Einstein-Hilbert integral under the product filter. It is not the constant-true proposition, and it does not encode the master gravity theorem conclusion. The module records a reduction of D2 onto quadrature-convergence and residual-vanishing subtargets, together with an explicit scope-status summary of which analytic inputs remain open.

background

In the Recognition Science gravity stack, the unconditional master theorem closes five named inputs that an older conditional quantum-gravity master theorem took as hypotheses. One of those inputs is the D2 witness: a physical convergence route from discrete Regge calculus to the continuum Einstein-Hilbert action.

Upstream, Track 1.B-PHY packages finite-probe Regge-to-EH residual theorems as a structural upgrade beyond flat-substrate witnesses. The present module sits between that residual infrastructure and the master-theorem closure surface. Its role is audit: it forces the D2 datum to be literally a filter-limit statement about the nonlinear Regge aggregate, rather than a collapsed True or a restatement of the master conclusion.

Sibling definitions name the quadrature-convergence target, the residual-vanishing target, the reduction of D2 onto those subtargets, and a scope-status record of open analytic fields.

proof idea

This is a scoping and definition module, not a deep proof development. It introduces named proposition targets for D2 quadrature convergence and residual vanishing, asserts that the product-filter D2 obligation is filter-limit convergence (not True), and packages a reduction statement plus a scope-status summary of which analytic inputs are still carried as hypotheses. Downstream modules discharge those open fields; this file only names and separates them.

why it matters in Recognition Science

The module feeds the damped-schedule closure, which closes D2 open item 2 of this audit: the uniform residual that the product-filter datum had carried as a supplied hypothesis. By pinning D2 as a real Tendsto obligation and listing the open analytic inputs, the audit prevents the master-theorem surface from silently absorbing unresolved continuum-limit work. In the broader RS gravity program this keeps the physical Regge-to-EH route honest relative to the unconditional master-theorem witnesses installed upstream.

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)