Gravity D2 Scoping Audit D2 Target Is Convergence

A convergence target, made explicit

In numerical analysis, a convergence statement is a precise promise: as a computation is refined, its output approaches a fixed value. The Recognition Science declaration d2_target_is_convergence makes exactly this kind of promise explicit for a particular gravity computation. It states that the target of the D2 recovery problem is a filter limit, a technical way of saying the sequence of approximations tends to a definite continuum result. This is not a vague aspiration; it is a formal identity, proved by definition in the framework's machine-checked library.

The computation in question is a discrete model of gravity called the Regge aggregate. It approximates the smooth Einstein-Hilbert action, the quantity whose minimisation gives general relativity, by summing over a lattice of simplices. The declaration says that this aggregate, as the lattice is refined, converges to the continuum integral. This is the honest content of the D2 target: it is a real Tendsto statement, not a trivial True placeholder, and it does not mention the master conclusion of the framework.

What the declaration does not claim is equally important. It does not assert that the convergence has been proved from first principles. That remains open. The declaration merely identifies the target and reduces it to two analytic inputs: the convergence of the quadrature rule and the vanishing of a residual error term. A separate theorem, d2_reduction, shows that if both inputs hold, the full convergence follows. This is a reduction, not a closure. The two inputs themselves remain targets, though the residual term has been discharged for a special class of damped schedules.

The declaration also scopes the claim to a specific geometry: the canonical periodic six-tet cubic torus. It says nothing about non-product or non-flat triangulations, which remain open. This is the load-bearing geometric problem. The value of the declaration is that it names the precise remaining targets, so they are not hidden inside a data structure. A reader can see exactly what is proved and what is not.

/-- The D2 product-filter target is literally a `Filter.Tendsto` convergence
of the full nonlinear Regge aggregate to the continuum integral.  It is not
`True` and it does not mention the master conclusion. -/
theorem d2_target_is_convergence
    {α ρ : Type*} {l : Filter α}
    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
    Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget D =
      Filter.Tendsto
        (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
          (α := α) (ρ := ρ) D.family)
        (D.refinementFilter ×ˢ l : Filter (ρ × α))
        (nhds D.continuumIntegral) := rfl

/-- The D2 product-filter target is literally a `Filter.Tendsto` convergence
of the full nonlinear Regge aggregate to the continuum integral.  It is not
`True` and it does not mention the master conclusion. -/
theorem d2_target_is_convergence
    {α ρ : Type*} {l : Filter α}
    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
    Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget D =
      Filter.Tendsto
        (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
          (α := α) (ρ := ρ) D.family)
        (D.refinementFilter ×ˢ l : Filter (ρ × α))
        (nhds D.continuumIntegral) := rfl

/-- **D2 REDUCTION THEOREM (what is actually proved).**  On the canonical
periodic six-tet cubic torus, the two named analytic targets — quadrature
convergence to the continuum integral and a vanishing Regge-residual — imply
that the full nonlinear Regge aggregate converges to the continuum
Einstein-Hilbert/Dirichlet integral on the product filter.

This is the honest content of the D2 master witness: convergence is reduced
to the two analytic inputs, which remain the open targets (§2).  It makes no
claim about non-product or non-flat triangulations. -/
theorem d2_reduction
    {α ρ : Type*} {l : Filter α}
    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (hquad : D2QuadratureConvergenceTarget l family refinementFilter continuumIntegral)
    (hres : D2ResidualVanishingTarget l family refinementFilter) :
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) family)
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds continuumIntegral) :=
  (CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData.fullReggeProduct_tendsto_continuum
    (α := α) (ρ := ρ) (l := l)
    { family := family
      refinementFilter := refinementFilter
      continuumIntegral := continuumIntegral
      quadrature_tendsto := hquad
      uniform_residual := hres })

What this page does not claim

The declaration does not prove the convergence from primitive mesh geometry. The declaration does not claim the quadrature convergence target is closed. The declaration does not cover non-product or non-flat triangulations.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/D2ScopingAudit.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: