Encyclopedia Gravity Gravity D2 Damped Schedule Closure D2 Reduction To Quadrature Only

ARTICLE 4 claims 4 theorems

Gravity D2 Damped Schedule Closure D2 Reduction To Quadrature Only

A formal theorem shows that, for a carefully damped family of discrete gravity approximations, the only analytic input left to verify is the convergence of the quadrature sums.

Verify this page

The damped-schedule reduction

In numerical analysis, quadrature is the art of replacing an integral by a finite sum: the area under a curve becomes the sum of areas of thin rectangles or, in higher dimensions, of small cells. A Regge approximation is a discrete model of spacetime built from flat tetrahedra, where the curvature is concentrated along the edges. The question at hand is whether, as the tetrahedra are refined, the discrete Regge total converges to the continuum integral it approximates. The theorem named d2_reduction_to_quadrature_only answers a specific part of that question: it shows that, for a particular family of approximations, the only remaining analytic input needed to guarantee convergence is the convergence of the quadrature sums themselves.

The classical setting is the canonical Dirichlet energy, a measure of how much a function varies over a region. In the framework's library, a machine-checked collection of formal theorems, the energy is shown to be quadratically homogeneous: scaling the input by a factor scales the energy by the square of that factor. The theorem also relies on a local correspondence, a cubic Taylor bound that controls how well the discrete Regge aggregate approximates the continuum integral within a small radius. The key move is to construct a damped family: starting from any refinement family and a schedule that shrinks to zero, the within-slice spacing is multiplied by a damping factor computed from the slice's own local-correspondence witnesses. This damping keeps every scaled probe inside the local-correspondence radius and shrinks the per-slice residual coefficient below a slice-independent envelope.

The theorem then proves that, for this damped family, the uniform residual target holds with no supplied analytic field: the difference between the full nonlinear Regge aggregate and the quadrature integral vanishes uniformly as the schedule tends to zero. Consequently, the full Regge-to-continuum convergence for the damped family needs only the quadrature limit, which is the statement of d2_reduction_to_quadrature_only. The master-theorem D2 datum for the damped family is constructed with the uniform residual proved, not supplied.

What the theorem does not claim is equally important. It does not prove the convergence of the explicit finite quadrature sums across cardinalities; that remains a family-specific geometric input. It does not add a new hypothesis beyond the local correspondence that every slice already carries. And it does not cover non-product, non-flat admissible triangulations. The reduction is conditional: if the quadrature sums converge, then the full Regge product filter converges to the continuum integral. The theorem isolates the analytic content, leaving the geometric convergence as the remaining supplied input.

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
THEOREM canonicalDirichletEnergy_smul · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean
canonicalDirichletEnergy_smul · IndisputableMonolith/Gravity/D2DampedScheduleClosure.lean:73 
/-- The canonical graph-Dirichlet energy is quadratically homogeneous under
scalar rescaling of the vertex potential. -/
theorem canonicalDirichletEnergy_smul
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (a : ℝ) (ξ : VertexPotential K) :
    canonicalDirichletEnergy K hK (a • ξ) =
      a ^ (2 : ℕ) * canonicalDirichletEnergy K hK ξ := by
  unfold canonicalDirichletEnergy
  have h : ∀ i j : Fin K.nV,
      canonicalDualWeight K hK i j * ((a • ξ) i - (a • ξ) j) ^ (2 : ℕ) =
        a ^ (2 : ℕ) * (canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
    intro i j
    have hsm : (a • ξ) i - (a • ξ) j = a * (ξ i - ξ j) := by
      simp [Pi.smul_apply, smul_eq_mul, mul_sub]
    rw [hsm, mul_pow]
    ring
  calc (1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
        canonicalDualWeight K hK i j * ((a • ξ) i - (a • ξ) j) ^ (2 : ℕ)
      = (1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
          a ^ (2 : ℕ) * (canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
        congr 1
        exact Finset.sum_congr rfl fun i _ =>
          Finset.sum_congr rfl fun j _ => h i j
    _ = a ^ (2 : ℕ) *
          ((1 / 2) * ∑ i : Fin K.nV, ∑ j : Fin K.nV,
            canonicalDualWeight K hK i j * (ξ i - ξ j) ^ (2 : ℕ)) := by
        simp only [← Finset.mul_sum]
        ring
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

What this page does not claim

The theorem does not prove the convergence of the quadrature sums themselves. The theorem does not add a new hypothesis beyond the local correspondence that every slice already carries. The theorem does not cover 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