Gravity D2 Scoping Audit D2 Residual Vanishing Target

The residual target

In numerical relativity, Regge calculus approximates spacetime by a discrete lattice of simplices, and the Einstein-Hilbert action is recovered as the lattice spacing shrinks to zero. The Recognition Science framework's library, a machine-checked collection of formal theorems, studies this recovery on a canonical periodic six-tet cubic torus. The declaration D2ResidualVanishingTarget names one of the two analytic inputs needed for that recovery: the residual, the difference between the full nonlinear Regge expression and a quadrature approximation, must vanish uniformly as the lattice refines. It is a genuine convergence statement, not a trivial truth, and it does not by itself assert that Regge calculus converges to the continuum.

The framework proves a reduction theorem: if both the quadrature convergence and the residual vanishing hold, then the full nonlinear Regge aggregate converges to the continuum Einstein-Hilbert integral on the product filter. This is the honest content of the D2 master witness; it reduces a difficult convergence problem to two cleaner analytic targets. The residual target was originally an independent hypothesis, but a 2026 closure derived it for a damped schedule class: for every slice family, a rescheduling that damps the spacing per slice, using constants from the slice's own local cubic Taylor bound, satisfies the residual target outright. That leaves only the quadrature limit as the open analytic input for D2, at least within that schedule class.

What the declaration does not claim is as important as what it proves. It does not discharge the residual target for an arbitrary supplied schedule; that remains open. It does not prove convergence on non-product or non-flat triangulations, which is the load-bearing geometric problem. It does not assert that the continuum limit exists without the two analytic inputs. The reduction theorem is a conditional statement, and the residual target is one of its conditions, now closed for a specific family of schedules but not in general.

/-- **Remaining target 2 (residual vanishing).**  The (full nonlinear Regge −
quadrature) residual is uniformly controlled on the product filter.
Currently supplied as the `uniform_residual` field. -/
def D2ResidualVanishingTarget
    {α ρ : Type*} (l : Filter α)
    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) : Prop :=
  CanonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget
    family refinementFilter

/-- **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 })

/-- D2 scope after `Gravity.D2DampedScheduleClosure`: one analytic input
(the quadrature limit) instead of two. -/
def d2ScopeStatusDamped : D2ScopeStatusDamped where
  reduction_proved := true
  quadrature_target_open := true
  residual_target_discharged_for_damped_schedules := true
  residual_target_open_for_arbitrary_schedules := true
  general_triangulation_open := true

What this page does not claim

The residual target is not discharged for an arbitrary supplied schedule. The reduction does not cover non-product or non-flat triangulations. The continuum limit is not proved to exist without the two analytic inputs.

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: