Encyclopedia Gravity Gravity D2 Damped Schedule Closure Normalized Regge Sub Limit Abs Le

ARTICLE 3 claims 3 theorems

Gravity D2 Damped Schedule Closure Normalized Regge Sub Limit Abs Le

A machine-checked theorem shows that a carefully slowed refinement schedule makes a discrete model of gravity converge to its continuous limit, with the error bounded by the schedule itself.

Verify this page

The damped limit

In numerical analysis, a common worry is that a discrete approximation to a continuous problem may not converge, or may converge too slowly to be useful. The declaration normalized_regge_sub_limit_abs_le addresses this worry for a specific family of discrete gravity models. These models, called Regge slices, approximate spacetime by a grid of tetrahedra, and the theorem concerns a quantity called the residual, which measures the difference between the discrete model's output and the ideal continuous integral it approximates.

The theorem states that for any such slice, and for any nonzero real number s, the absolute value of a normalized version of the residual is bounded by that number s. In plainer terms, if one chooses a target error size s, then after applying a damping factor to the slice's internal spacing, the error will be no larger than s. The damping factor is computed from the slice's own local properties, such as its curvature bound and the norms of its probe functions. This is not a vague asymptotic statement; it is a concrete bound that holds for every slice and every nonzero s.

This result is a theorem in the framework's machine-checked library of formal theorems, meaning it has been verified by a computer proof checker with no unproven assumptions. It is part of a larger effort to show that a discrete, combinatorial description of gravity can recover the smooth, continuous theory. The theorem is a key step: it shows that the residual, the error term, can be made arbitrarily small by choosing a sufficiently damped refinement schedule. This does not mean the discrete model is the same as the continuous one; it means the discrete model can be made to approximate it as closely as desired.

The theorem does not claim that the discrete model converges on its own, without damping. Nor does it claim that the quadrature sums, the finite approximations to integrals, converge across different grid sizes; that remains a separate, open target. It also does not claim that the local correspondence bound, the cubic Taylor estimate that underlies the damping construction, holds for all possible triangulations; it is assumed as a property of each slice. What the theorem establishes is a precise, machine-checked control on the residual, given that local bound and a chosen schedule.

THEOREM normalized_regge_sub_limit_abs_le · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
normalized_regge_sub_limit_abs_le · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:326 
/-- Normalized nonlinear Regge action minus the quadratic Dirichlet limit is
bounded by the slice's cubic constant times `|s|` times the cubed probe norm,
whenever the scaled probe sits inside the local-correspondence radius.  This
is the local cubic Taylor bound divided by `s²`. -/
theorem normalized_regge_sub_limit_abs_le
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
    (s : ℝ) (hs : s ≠ 0) :
    letI : NeZero S.Nx := S.instNx
    letI : NeZero S.Ny := S.instNy
    letI : NeZero S.Nz := S.instNz
    ∀ ξ : VertexPotential
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K,
      ‖s • ξ‖ < localRadius S →
        |reggeAction
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
            (s • ξ) / s ^ (2 : ℕ) -
          (1 / 2) *
            canonicalDirichletEnergy
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
              ξ| ≤
          localConstant S * |s| * ‖ξ‖ ^ (3 : ℕ) := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  intro ξ hsmall
  have hb := local_bound S (s • ξ) hsmall
  have h0 :
      reggeAction
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
        (zeroPotential
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K) = 0 :=
    canonicalPeriodicReggeAction_zeroPotential_eq_zero_of_flatConfiguration
      S.Nx S.Ny S.Nz S.hx S.hy S.hz
      (canonicalPeriodicFlatConfiguration S.Nx S.Ny S.Nz S.hx S.hy S.hz)
  have hES :
      canonicalDirichletEnergy
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
        (s • ξ) =
        periodicEdgeStencilDirichletAction
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz) (s • ξ) :=
    canonicalPeriodicEdgeStencilTarget S.Nx S.Ny S.Nz S.hx S.hy S.hz (s • ξ)
  have hsm :
      canonicalDirichletEnergy
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
        (s • ξ) =
        s ^ (2 : ℕ) *
          canonicalDirichletEnergy
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
            ξ :=
    canonicalDirichletEnergy_smul _ _ s ξ
  rw [h0, sub_zero, ← hES, hsm, Real.norm_eq_abs] at hb
  have hs2 : (0 : ℝ) < s ^ (2 : ℕ) := by positivity
  have key :
      reggeAction
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
        (s • ξ) / s ^ (2 : ℕ) -
        (1 / 2) *
          canonicalDirichletEnergy
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
            ξ =
        (reggeAction
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
          (s • ξ) -
          (1 / 2) *
            (s ^ (2 : ℕ) *
              canonicalDirichletEnergy
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
                ξ)) / s ^ (2 : ℕ) := by
    field_simp
  rw [key, abs_div, abs_of_pos hs2]
  have hnorm3 : ‖s • ξ‖ ^ (3 : ℕ) = |s| ^ (3 : ℕ) * ‖ξ‖ ^ (3 : ℕ) := by
    rw [norm_smul, Real.norm_eq_abs, mul_pow]
  have habs3 : |s| ^ (3 : ℕ) = |s| * s ^ (2 : ℕ) := by
    rw [pow_succ, sq_abs, mul_comm]
  have hdivle :
      |reggeAction
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
          (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
          (s • ξ) -
          (1 / 2) *
            (s ^ (2 : ℕ) *
              canonicalDirichletEnergy
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
                ξ)| / s ^ (2 : ℕ) ≤
        (localConstant S * ‖s • ξ‖ ^ (3 : ℕ)) / s ^ (2 : ℕ) := by
    gcongr
  refine le_trans hdivle (le_of_eq ?_)
  rw [hnorm3, habs3]
  field_simp
THEOREM d2_damped_schedule_closure_one_statement · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
d2_damped_schedule_closure_one_statement · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:706 
/-- One-statement bundle for citation: damping preserves quadrature proxies,
derives the uniform residual outright, and reduces full D2 convergence to the
quadrature limit alone. -/
theorem d2_damped_schedule_closure_one_statement
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) :
    (∀ r : ρ,
      ((dampedFamily F σ hσ0 hσne).slice r).quadratureIntegral =
        (F.slice r).quadratureIntegral) ∧
    D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily F σ hσ0 hσne)
      refinementFilter ∧
    (∀ continuumIntegral : ℝ,
      D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral →
        Filter.Tendsto
          (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
            (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
          (refinementFilter ×ˢ l : Filter (ρ × α))
          (nhds continuumIntegral)) :=
  ⟨fun r => dampedSlice_quadratureIntegral (F.slice r) σ hσ0 hσne,
   d2_residual_vanishing_target_damped F σ hσ0 hσne refinementFilter,
   fun continuumIntegral hquad =>
     d2_reduction_to_quadrature_only F σ hσ0 hσne refinementFilter continuumIntegral hquad⟩
THEOREM dampedSlice_residual_abs_le · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
dampedSlice_residual_abs_le · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:430 
/-- The damped slice's full nonlinear Regge aggregate minus its quadrature
proxy is bounded by `|σ t|`, uniformly in the slice, whenever `σ t ≠ 0` and
`|σ t| ≤ 1`.  The damping factor absorbs the slice's local radius, cubic
constant, probe norms, and limiting cell volume. -/
theorem dampedSlice_residual_abs_le
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (t : α) (hne : σ t ≠ 0) (hle : |σ t| ≤ 1) :
    |(dampedSlice S σ hσ0 hσne).fullReggeAggregate t -
      (dampedSlice S σ hσ0 hσne).quadratureIntegral| ≤ |σ t| := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  have hd_pos : 0 < dampingFactor S := dampingFactor_pos S
  have hs_ne : σ t * dampingFactor S ≠ 0 := mul_ne_zero hne hd_pos.ne'
  have habs_s : |σ t * dampingFactor S| = |σ t| * dampingFactor S := by
    rw [abs_mul, abs_of_pos hd_pos]
  have habs_s_le : |σ t * dampingFactor S| ≤ dampingFactor S := by
    rw [habs_s]
    exact mul_le_of_le_one_left hd_pos.le hle
  -- The damped aggregate and quadrature proxy as explicit tetrahedron sums.
  have hAgg : (dampedSlice S σ hσ0 hσne).fullReggeAggregate t =
      ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
            S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
          (reggeAction
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
            ((σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) /
            (σ t * dampingFactor S) ^ (2 : ℕ)) := rfl
  have hQuad : (dampedSlice S σ hσ0 hσne).quadratureIntegral =
      ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
            S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
          ((1 / 2) *
            canonicalDirichletEnergy
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
              (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) := rfl
  rw [hAgg, hQuad, ← Finset.sum_sub_distrib]
  simp only [canonicalPeriodicFreudenthalTetVolumeWeight, ← mul_sub]
  -- Every damped probe sits inside the local-correspondence radius.
  have hsmall : ∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
      ‖(σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ <
        localRadius S := by
    intro τ
    have hM : ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ≤ probeNormSum S :=
      Finset.single_le_sum (f := fun τ' =>
          ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ')‖)
        (fun τ' _ => norm_nonneg _) (Finset.mem_univ τ)
    have h1M : 0 < 1 + probeNormSum S := one_add_probeNormSum_pos S
    have hM_lt : ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ < 1 + probeNormSum S := by
      linarith
    have hq_pos : 0 < localRadius S / (1 + probeNormSum S) :=
      div_pos (localRadius_pos S) h1M
    calc ‖(σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖
        = |σ t * dampingFactor S| *
            ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ := by
          rw [norm_smul, Real.norm_eq_abs]
      _ ≤ (localRadius S / (1 + probeNormSum S)) *
            ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ := by
          exact mul_le_mul_of_nonneg_right
            (le_trans habs_s_le (dampingFactor_le_radius_quotient S)) (norm_nonneg _)
      _ < (localRadius S / (1 + probeNormSum S)) * (1 + probeNormSum S) := by
          exact mul_lt_mul_of_pos_left hM_lt hq_pos
      _ = localRadius S := div_mul_cancel₀ _ h1M.ne'
  -- Per-tetrahedron bound from the normalized cubic Taylor estimate.
  have hper : ∀ τ ∈ (Finset.univ : Finset (Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)))),
      |S.data.limitCellVolume / 6 *
        (reggeAction
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
            (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
            ((σ t * dampingFactor S) • S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) /
            (σ t * dampingFactor S) ^ (2 : ℕ) -
          (1 / 2) *
            canonicalDirichletEnergy
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
              (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)))| ≤
        |S.data.limitCellVolume| / 6 *
          (localConstant S * |σ t * dampingFactor S| *
            ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ)) := by
    intro τ _
    rw [abs_mul]
    have hwabs : |S.data.limitCellVolume / 6| = |S.data.limitCellVolume| / 6 := by
      rw [abs_div, abs_of_pos (by norm_num : (0 : ℝ) < 6)]
    rw [hwabs]
    exact mul_le_mul_of_nonneg_left
      (normalized_regge_sub_limit_abs_le S (σ t * dampingFactor S) hs_ne
        (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)) (hsmall τ))
      (div_nonneg (abs_nonneg _) (by norm_num))
  refine le_trans (Finset.abs_sum_le_sum_abs _ _) (le_trans (Finset.sum_le_sum hper) ?_)
  -- Collapse the sum to the residual coefficient and absorb the damping.
  have hrc : residualCoefficient S =
      |S.data.limitCellVolume| / 6 * localConstant S *
        (∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
          ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ)) := rfl
  have hsum_eq :
      (∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        |S.data.limitCellVolume| / 6 *
          (localConstant S * |σ t * dampingFactor S| *
            ‖S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ)‖ ^ (3 : ℕ))) =
        |σ t * dampingFactor S| * residualCoefficient S := by
    rw [hrc]
    simp only [Finset.mul_sum]
    exact Finset.sum_congr rfl fun τ _ => by ring
  rw [hsum_eq, habs_s]
  calc |σ t| * dampingFactor S * residualCoefficient S
      = |σ t| * (dampingFactor S * residualCoefficient S) := by ring
    _ ≤ |σ t| * 1 :=
        mul_le_mul_of_nonneg_left
          (dampingFactor_mul_residualCoefficient_le_one S) (abs_nonneg _)
    _ = |σ t| := mul_one _

What this page does not claim

The theorem does not prove that the quadrature sums converge across different grid sizes. The theorem does not establish the local correspondence bound for all triangulations; it assumes it as a property of each slice. The theorem does not claim the discrete model is identical to the continuous one, only that it can approximate it arbitrarily well.

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