Encyclopedia Gravity Gravity D2 Damped Schedule Closure Damped Product Filter Data Satisfies Master T

ARTICLE 4 claims 4 theorems

Gravity D2 Damped Schedule Closure Damped Product Filter Data Satisfies Master T

A machine-checked proof shows that a finely tuned numerical recipe for gravity can be derived, not assumed, from a local bound on how curved space behaves.

Verify this page

The damped closure

In numerical gravity, one often approximates a continuous physical quantity by a family of discrete computations on finer and finer grids. A key question is whether the error between the discrete approximation and the true continuum value shrinks to zero as the grid refines. The Recognition Science declaration dampedProductFilterData_satisfies_master_target is a machine-checked theorem that answers this question for a specific construction: it proves that a particular family of discrete gravity computations, called the damped family, satisfies the master convergence target.

The construction works as follows. Start with any family of discrete gravity approximations, each with a different grid size, and a schedule that shrinks a damping factor to zero. The damped family keeps the same grid sizes and the same approximate integrals, but it shrinks the spacing within each grid by this damping factor. The theorem proves that this damped family has a uniform residual bound: the error between the full nonlinear discrete gravity expression and its approximate integral is bounded by the damping factor itself, uniformly across all grid sizes. This is derived from a local cubic Taylor bound on the discrete curvature, not assumed as an extra hypothesis.

Because this uniform residual bound holds, the full discrete gravity expression converges to the continuum integral for the damped family, provided only that the approximate quadrature sums converge. The declaration dampedProductFilterData_satisfies_master_target packages this into a single object: it takes the damped family, a quadrature convergence assumption, and produces a proof that the master physical target is satisfied. The quadrature convergence itself remains a supplied input, not something the theorem proves.

What the declaration does not claim is just as important. It does not prove that quadrature sums converge across grid sizes; that is a separate, family-specific geometric fact that remains an open supplied input. It does not prove anything about non-flat or non-product triangulations, which are outside its scope. And it does not claim that the local bound itself is derived here; that bound is a field carried by every slice, exactly as before. The theorem's contribution is narrower: it shows that, given that local bound and a damping schedule, the residual vanishing target follows with no additional analytic field supplied.

In plain terms, the declaration is a reduction result. It reduces the hard problem of proving convergence for the full nonlinear gravity expression to the easier problem of proving convergence of quadrature sums. The residual error, which could have been a separate obstacle, is shown to be controlled by the damping construction. This is a step toward making the discrete-to-continuum bridge in this framework fully derived rather than partially assumed.

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)
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 d2_reduction_to_quadrature_only · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
d2_reduction_to_quadrature_only · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:685 
/-- **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 across grid sizes. The theorem does not apply to non-flat or non-product triangulations. The theorem does not derive the local cubic Taylor bound; it assumes it as a field of each slice.

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