Gravity D2 Quadrature Instances D2 Flat Sector One Statement

The flat sector closes

In numerical gravity, one often approximates curved spacetime by a grid of tetrahedra, then checks that the discrete equations approach the continuous ones as the grid refines. The Recognition Science framework's library of machine-checked theorems contains a statement, d2_flat_sector_one_statement, that settles one part of this check. It concerns a Regge aggregate, a discrete version of the Einstein-Hilbert action built from edge lengths and angles, which should converge to the continuum value as the tetrahedra shrink.

The statement proves three things together for any family of tetrahedral grids and any damping schedule (a sequence of small perturbations that vanish in the limit). First, the quadrature target, a measure of how well the discrete sum approximates an integral, holds at the flat value zero with no hypothesis. Second, the residual, the error left after damping, also vanishes with no hypothesis. Third, the full nonlinear Regge aggregate of the damped flattened family converges to zero on the product filter, meaning the approximation improves as both the grid refines and the damping shrinks. The proof is unconditional: it consumes only the local correspondence data that every slice carries by definition, with no supplied analytic input.

The key mechanism is that flattening a slice, replacing every tetrahedron probe by the zero potential, makes the canonical Dirichlet energy vanish. Since the energy is quadratic in the potential, the zero potential gives zero energy exactly. This makes the quadrature proxy identically zero, so convergence to the flat continuum integral is immediate. The library also shows that for uniform-probe families, where all probes equal one global potential, the quadrature proxy collapses to a simple scalar: the tetrahedron count times a cell weight times half the Dirichlet energy of that potential. This reduces the open quadrature question for such families to a concrete numerical limit of finite graph-Dirichlet energies.

What this statement does not claim is broader. It does not prove the scalar Dirichlet limit for curvature-bearing probe families, which remains the genuine Riemann-sum content of D2. It does not establish the local correspondence at each cardinality, carried by slices as before. And it does not cover non-product, non-flat admissible triangulations. The flat sector is closed end to end on the canonical route, but the curved sector remains open.

/-- **D2 status after this module, in one statement.**  For every slice
family `F` and universal schedule `σ`: the flattened family's quadrature
target holds at the flat value `0` with no hypothesis; the damped flattened
family's residual target holds with no hypothesis; and the full nonlinear
Regge aggregate of the damped flattened family converges to `0` on the
product filter.  The flat sector of D2 is closed end to end on the canonical
route, with no supplied analytic field anywhere. -/
theorem d2_flat_sector_one_statement
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) :
    D2ScopingAudit.D2QuadratureConvergenceTarget l (flatFamily F) refinementFilter 0 ∧
    D2ScopingAudit.D2ResidualVanishingTarget l (dampedFamily (flatFamily F) σ hσ0 hσne)
      refinementFilter ∧
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) (dampedFamily (flatFamily F) σ hσ0 hσne))
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds 0) :=
  ⟨d2_quadrature_target_flat F refinementFilter,
   d2_residual_vanishing_target_damped (flatFamily F) σ hσ0 hσne refinementFilter,
   dampedFlat_fullReggeProduct_tendsto_zero F σ hσ0 hσne refinementFilter⟩

/-- **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 canonicalDirichletEnergy_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    canonicalDirichletEnergy K hK (zeroPotential K) = 0 := by
  unfold canonicalDirichletEnergy zeroPotential
  simp

What this page does not claim

The scalar Dirichlet limit for curvature-bearing probe families is not proved. The Track 1.B local correspondence at each cardinality is not established here. Non-product, non-flat admissible triangulations are not covered.

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: