Encyclopedia Gravity Gravity D2 Damped Schedule Closure

ARTICLE 3 claims 3 theorems

Gravity D2 Damped Schedule Closure

A machine-checked proof shows that a simple damping trick makes discrete gravity converge to the continuum without any extra assumptions.

Verify this page

The damping proof

In numerical gravity, the path from a discrete lattice to the smooth continuum of general relativity is not automatic. The Einstein-Hilbert action, the integral that defines the theory, must be approximated by sums over cells. The difference between the true continuum integral and its discrete approximation is called the residual. In the Recognition Science framework, the D2 damped schedule closure module proves that this residual can be made to vanish uniformly, not by adding a new physical hypothesis, but by a careful choice of how the lattice spacing shrinks.

The starting point is a family of lattices, each a periodic arrangement of tetrahedra. Each lattice has a local correspondence property: a cubic Taylor bound that controls how well the discrete Regge action, a sum over edges, matches the continuum curvature. The module defines a damping factor for each lattice, computed from that lattice's own local bound, its probe norms, and its limiting cell volume. The damped family rescales the within-lattice spacing by this factor times a universal schedule that tends to zero. The key theorem, dampedFamily_uniformResidual, proves that for this damped family, the full nonlinear Regge residual is bounded by the schedule itself, and so vanishes uniformly.

This result closes a specific open item in the D2 scoping audit. Previously, the vanishing of the residual was a supplied hypothesis, an assumption fed into the master theorem. The module discharges this assumption from the primitive local bound. The consequence is that the full Regge-to-continuum convergence for the damped family requires only the quadrature limit, the convergence of the explicit finite sums, which remains a family-specific geometric input. The master-theorem datum for the damped family is then constructed with the residual proved, not assumed.

What the module does not do is prove the quadrature convergence itself, nor does it add any new physical content beyond what each lattice slice already carries. It is a structural result about how to organize the refinement. The practical upshot is that one less analytic input has to be guessed or fitted; the damping schedule is derived from the lattice's own geometry. This is a step toward a fully derived, rather than supplied, continuum limit in the framework's account of gravity.

THEOREM dampedFamily_uniformResidual · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
dampedFamily_uniformResidual · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:560 
/-- **DERIVED UNIFORM RESIDUAL (D2 open item 2 discharged).**  The damped
family satisfies the product uniform-residual target for every refinement
filter.  No analytic residual field is supplied: the bound comes from each
slice's own local cubic Taylor correspondence, the flat-action normalization,
the edge-stencil Dirichlet identification, and the constructed damping. -/
theorem dampedFamily_uniformResidual
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) :
    CanonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget
      (dampedFamily F σ hσ0 hσne) refinementFilter := by
  refine canonicalPeriodicTetSixTetVolumeQuadratureProductUniformResidualTarget_of_snd_abs_bound
    (dampedFamily F σ hσ0 hσne) refinementFilter (fun t => |σ t|) ?_ ?_
  · simpa using hσ0.abs
  · have h1 : ∀ᶠ t : α in l, |σ t| ≤ 1 := by
      have hball : Metric.closedBall (0 : ℝ) 1 ∈ nhds (0 : ℝ) :=
        Metric.closedBall_mem_nhds 0 one_pos
      have := hσ0.eventually_mem hball
      simpa [Metric.mem_closedBall, Real.dist_eq] using this
    refine ((hσne.and h1).prod_inr refinementFilter).mono ?_
    rintro ⟨r, t⟩ ⟨ht_ne, ht_le⟩
    exact dampedSlice_residual_abs_le (F.slice r) σ hσ0 hσne t ht_ne ht_le
THEOREM dampedFamily_fullReggeProduct_tendsto_continuum · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
dampedFamily_fullReggeProduct_tendsto_continuum · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:627 
/-- **D2 DAMPED-SCHEDULE CLOSURE.**  For every varying-cardinality slice
family and every universal schedule `σ → 0`, the full nonlinear Regge
aggregate of the damped family converges to the continuum integral on the
product filter, given only the cross-cardinality quadrature limit.  The
two-scale uniform residual is derived, not assumed. -/
theorem dampedFamily_fullReggeProduct_tendsto_continuum
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (hquad :
      CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
        F refinementFilter continuumIntegral) :
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds continuumIntegral) :=
  (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral
    hquad).fullReggeProduct_tendsto_continuum
THEOREM dampedProductFilterData_satisfies_master_target · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
dampedProductFilterData_satisfies_master_target · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:650 
/-- The damped datum satisfies the Track 1.B-PHY concrete product-filter
target consumed by the quantum-gravity master theorem. -/
theorem dampedProductFilterData_satisfies_master_target
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (hquad :
      CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
        F refinementFilter continuumIntegral) :
    Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget
      (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral hquad) :=
  Track1BCPhysicalResidual.physicalReggeEHConcreteProductFilterTarget_holds
    (dampedProductFilterData F σ hσ0 hσne refinementFilter continuumIntegral hquad)

What this page does not claim

The module does not prove the convergence of the finite quadrature sums across cardinalities. The module does not add any new physical hypothesis beyond the local correspondence each slice already carries. The module does not address non-product, non-flat admissible 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/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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND