Gravity D2 Damped Schedule Closure Damping Factor Le Radius Quotient

The damping factor's bound

In numerical analysis, a quadrature rule approximates an integral by a finite sum. When the integral comes from a discrete model of spacetime that is refined to approach a continuum, the error between the discrete and continuum results must be shown to vanish. The declaration dampingFactor_le_radius_quotient is a step in that proof. It states that a certain damping factor, a positive real number, is no larger than a quotient formed from a local radius and a sum of probe norms.

The damping factor is defined as the minimum of two quantities. The first is the local radius divided by one plus the sum of the norms of the probes. The second is one divided by one plus a residual coefficient. The theorem in question proves the first inequality: the damping factor is at most the first quotient. This is a simple consequence of the definition of minimum, but it is the key that lets the proof proceed. Because the damping factor is bounded by that quotient, it stays inside the local radius, the region where the cubic Taylor bound on the error holds.

This bound is part of a larger construction called the damped family. Given a family of discrete slices and a schedule that tends to zero, the damped family rescales the within-slice spacing by the damping factor. The theorem dampedFamily_uniformResidual then shows that, for this damped family, the residual between the full nonlinear Regge and the quadrature integral vanishes uniformly. This means the error is controlled by the schedule itself, not by any supplied analytic field. The full convergence to the continuum then requires only the quadrature limit, which remains a separate input.

In Recognition Science, this is a theorem in the machine-checked library of formal theorems. It is part of a chain that derives the physical content of gravity from a discrete ledger of recognition events. The theorem does not claim that the quadrature sums converge; that is a separate target. It does not claim that the local correspondence bound holds; that is a field of every slice. It only establishes the inequality that makes the damping construction work.

theorem dampingFactor_le_radius_quotient
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
    dampingFactor S ≤ localRadius S / (1 + probeNormSum S) :=
  min_le_left _ _

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

What this page does not claim

The theorem does not prove that the quadrature sums converge; that is a separate target. The theorem does not supply the local correspondence bound; it is a field of every slice. The theorem does not apply to 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: