Gravity D2 Damped Schedule Closure D2 Damped Schedule Closure One Statement

The damped schedule closure

In numerical analysis, when approximating a continuous problem by a discrete one, one must show that the approximation improves as the grid gets finer. The ledger, the framework's discrete record of events, faces the same test in its gravity model. The declaration d2_damped_schedule_closure_one_statement is a theorem in the framework's machine-checked library of formal theorems. It establishes that one of the two required convergence conditions, the vanishing of the residual error, follows automatically from a local bound that each refinement step already carries.

The theorem concerns a family of triangulations of a three-dimensional torus, each with a different number of cells. The local bound, a cubic Taylor estimate, says that the difference between the full nonlinear Regge action and its quadratic approximation is controlled by the cube of the probe displacement. The declaration constructs a damped family: it keeps the same cell volumes but shrinks the within-slice spacing by a factor computed from that slice's own local bound. This damping keeps every probe inside the radius where the local bound holds, and it forces the per-slice residual coefficient below a universal envelope that vanishes with the schedule. The result is that the product-filter uniform residual target holds for the damped family with no supplied analytic field.

The payoff is a reduction. The full nonlinear Regge to continuum convergence for the damped family now needs only the quadrature limit, the convergence of the explicit finite sums across cardinalities. That quadrature convergence remains a supplied input, a family-specific geometric datum. The declaration does not establish it. It also does not establish the local correspondence itself, which remains a field of every slice exactly as before. And it does not cover non-product, non-flat admissible triangulations, which stay open.

What the declaration changes is the structure of the remaining work. One of the two analytic inputs that the D2 scoping audit had listed as supplied hypotheses is now derived. A reader of the framework can now state the convergence problem with a single unproved geometric input, the quadrature limit, rather than two. The residual vanishing is no longer a hypothesis to be checked but a consequence of the local bound that was already there.

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

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

What this page does not claim

The declaration does not establish the quadrature convergence target, which remains a supplied input. The declaration does not establish the local correspondence bound itself, which remains a field of every slice. The declaration does not cover non-product, non-flat admissible triangulations, which remain open.

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: