Encyclopedia Gravity Gravity D2 Quadrature Instances

ARTICLE 4 claims 4 theorems

Gravity D2 Quadrature Instances

A machine-checked proof shows that a flattened model of spacetime gravity converges exactly to the flat value, closing a key technical gap.

Verify this page

The flat sector closes

In numerical approaches to gravity, one often approximates curved spacetime by a collection of flat tetrahedra, then refines the collection to approach a smooth limit. A central question is whether the approximate 'action' or energy of the configuration converges to the correct continuum value as the tetrahedra shrink. This gravity d2 quadrature instances (a set of concrete convergence examples within a larger program) addresses that question for a special case: when the tetrahedra are all flattened to have zero potential.

The classical setup is a Riemann sum: the integral of a function is approximated by summing its values at sample points, weighted by cell volumes. Here the role of the function is played by a Dirichlet energy (a measure of how much a field varies), and the tetrahedra are the cells. The proof shows, with no unproved assumptions, that for a flattened family, the quadrature proxy (the discrete approximation to the continuum integral) is exactly zero, and hence converges trivially to the flat continuum value of zero.

The key theorem, dampedFlat_fullReggeProduct_tendsto_zero, states that the full nonlinear Regge aggregate (a discrete gravity action) of the damped flattened family converges to zero on the product filter. This closes the 'flat sector' of the D2 reduction: both previously assumed analytic inputs, the quadrature target and the uniform residual, are now proved theorems. The proof also shows that for uniform-probe families (where every tetrahedron has the same potential), the quadrature proxy simplifies to a scalar multiple of the Dirichlet energy, reducing the open problem to a concrete limit of finite graph-Dirichlet energies.

In plain language: if you take any family of tetrahedral meshes and set the field to zero everywhere, the discrete gravity action provably vanishes in the limit, matching the flat spacetime value. This is a necessary consistency check for the framework's approach to quantum gravity, confirming that the discrete formalism does not introduce spurious curvature in the flat case. The remaining open problem is the genuine Riemann-sum content: proving the same convergence for families with non-zero curvature-bearing potentials.

THEOREM flattenSlice_quadratureIntegral · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
flattenSlice_quadratureIntegral · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:104 
/-- The flattened slice's quadrature proxy is exactly zero. -/
theorem flattenSlice_quadratureIntegral
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
    (flattenSlice S).quadratureIntegral = 0 := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  have h : (flattenSlice S).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
              (zeroPotential
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K)) :=
    rfl
  rw [h]
  simp [canonicalDirichletEnergy_zero]
THEOREM flatFamily_quadrature_target · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
flatFamily_quadrature_target · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:135 
/-- **The flat-sector quadrature target holds with no hypothesis.**  The
flattened family's quadrature proxies are identically zero, so they converge
to the flat continuum Einstein-Hilbert value `0` along every refinement
filter. -/
theorem flatFamily_quadrature_target
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) :
    CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
      (flatFamily F) refinementFilter 0 := by
  unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
  have h : (fun r : ρ => ((flatFamily F).slice r).quadratureIntegral) =
      fun _ : ρ => (0 : ℝ) := by
    funext r
    exact flattenSlice_quadratureIntegral (F.slice r)
  rw [h]
  exact tendsto_const_nhds
THEOREM dampedFlat_fullReggeProduct_tendsto_zero · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
dampedFlat_fullReggeProduct_tendsto_zero · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:163 
/-- **FLAT-SECTOR D2 CLOSURE (no supplied analytic inputs).**  For every
slice family and every universal schedule, the full nonlinear Regge aggregate
of the damped flattened family converges to the flat continuum value `0` on
the product filter.  Both former analytic inputs are theorems here: the
quadrature target by §3, the uniform residual by the damped-schedule
closure.  The only data consumed are the slices themselves, including the
Track 1.B local correspondence they carry by definition. -/
theorem dampedFlat_fullReggeProduct_tendsto_zero
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) :
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) (dampedFamily (flatFamily F) σ hσ0 hσne))
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds 0) :=
  dampedFamily_fullReggeProduct_tendsto_continuum (flatFamily F) σ hσ0 hσne
    refinementFilter 0 (flatFamily_quadrature_target F refinementFilter)
THEOREM quadratureIntegral_of_uniform_probe · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
quadratureIntegral_of_uniform_probe · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:215 
/-- For a slice whose tetrahedron probes are all the same global potential,
the quadrature proxy collapses to tetrahedron count times limiting cell
weight times the Dirichlet limit action of that potential. -/
theorem quadratureIntegral_of_uniform_probe
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
    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,
      (∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ) = ξ) →
      S.quadratureIntegral =
        (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz) : ℝ) *
          (S.data.limitCellVolume / 6) *
          ((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
              ξ) := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  intro ξ hξ
  have h : S.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 [h]
  have hterm : ∀ τ : 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 τ))) =
        S.data.limitCellVolume / 6 *
          ((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
              ξ) := by
    intro τ
    rw [hξ τ]
    simp only [canonicalPeriodicFreudenthalTetVolumeWeight]
  rw [Finset.sum_congr rfl fun τ _ => hterm τ]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  ring

What this page does not claim

The proof does not cover convergence for curved (non-flat) probe families. The proof does not establish the Track 1.B local correspondence at each cardinality. The proof does not address 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/D2QuadratureInstances.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