Gravity D2 Damped Schedule Closure D2 Residual Vanishing Target Damped

The damped closure

In numerical analysis, a residual is the difference between an approximate solution and the exact one. In the Recognition Science framework's gravity program, the residual measures how far a discrete, grid-based version of the Einstein-Hilbert action, built from tetrahedra, sits from its continuum limit. The declaration d2_residual_vanishing_target_damped is a theorem in the framework's machine-checked library of formal theorems. It proves that this residual can be forced to vanish uniformly, but only for a specially constructed family of grids.

The construction works by damping, or shrinking, the spacing within each grid slice according to a schedule that tends to zero. The key insight is that each slice already carries a local cubic error bound, a Taylor-style estimate that limits how fast the discrete action deviates from the continuum value. The damping factor, computed from that bound, keeps every probe inside the radius where the bound applies. The theorem then shows that the residual of the damped family is bounded by the schedule itself, which goes to zero. This closes one of two analytic gaps in the D2 audit: the residual vanishing target is now derived, not supplied as an assumption.

The proof also preserves the quadrature integrals, the discrete sums that approximate the continuum integral. Because the damping does not change the limiting cell volumes or the probes, the quadrature proxies are identical for the damped and original families. The full discrete-to-continuum convergence then reduces to a single remaining input: the convergence of the quadrature sums themselves, which is family-specific geometric data and remains an open target.

In Recognition Science, this is a step toward showing that gravity, as a discrete recognition process, converges to the classical continuum theory. The theorem does not claim that the convergence holds for arbitrary grids, nor that the quadrature convergence is proved. It establishes a conditional bridge: if the quadrature sums converge, then the full nonlinear Regge action converges to the continuum integral for the damped family.

/-- **`D2ResidualVanishingTarget` holds for damped schedules.**  Stated in the
exact vocabulary of `D2ScopingAudit`: for every family, the residual target of
the damped family is a theorem, with the bound built from each slice's local
correspondence (the primitive curvature bound) and the constructed spacing
damping. -/
theorem d2_residual_vanishing_target_damped
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) :
    D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily F σ hσ0 hσne)
      refinementFilter :=
  dampedFamily_uniformResidual F σ hσ0 hσne refinementFilter

/-- **D2 reduced to one analytic input.**  In the audit's vocabulary: the
quadrature target alone implies the full nonlinear product-filter convergence
for the damped family.  Compare `D2ScopingAudit.d2_reduction_statement`,
which consumed both targets. -/
theorem d2_reduction_to_quadrature_only
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
    D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral →
      Filter.Tendsto
        (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
          (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
        (refinementFilter ×ˢ l : Filter (ρ × α))
        (nhds continuumIntegral) :=
  fun hquad =>
    dampedFamily_fullReggeProduct_tendsto_continuum F σ hσ0 hσne refinementFilter
      continuumIntegral hquad

What this page does not claim

The theorem does not prove that quadrature sums converge for any family. It does not apply to arbitrary grids, only to those with the damping schedule applied.

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/D2DampedScheduleClosure.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: