Gravity D2 Scoping Audit D2 Reduction Statement

The D2 reduction

In general relativity, the Einstein-Hilbert action is the integral that yields Einstein's field equations. Regge calculus is a discrete approximation: it replaces smooth spacetime with a network of flat tetrahedra, and the action becomes a sum over the network. The framework's D2 reduction is a theorem about when that discrete sum actually converges to the continuum integral as the tetrahedra are refined.

The theorem, d2_reduction_statement, states a conditional result. On a canonical periodic six-tet cubic torus, if two analytic conditions hold, then the full nonlinear Regge aggregate converges to the continuum Einstein-Hilbert integral. The two conditions are: first, that the quadrature rule used to approximate the integral converges to the continuum value; second, that the residual, the difference between the full nonlinear Regge expression and the quadrature approximation, vanishes uniformly under refinement. The theorem proves that these two conditions together are sufficient for the convergence statement.

What the declaration explicitly does not claim is just as important as what it proves. It does not assert that either of the two analytic conditions is true for a concrete refinement family. It does not claim convergence for non-product or non-flat triangulations. The theorem is a reduction, not a closure: it shows that the remaining work is precisely to discharge the two analytic targets, and it names them so they cannot hide inside a data structure.

Later work in the same library has partially closed those targets. For damped schedules, where the spacing between slices is rescaled using local curvature bounds, the residual vanishing condition is proved outright, leaving only the quadrature limit as an open analytic input. The general geometric problem, extending convergence beyond the flat product torus to physically admissible non-product, non-flat triangulations, remains open and is flagged as the load-bearing item.

The practical consequence for a reader is a precise map of the frontier. The reduction is a proved theorem, the residual target is closed for a damped schedule class, and the quadrature limit plus the general triangulation extension are the named open problems. This is the honest status of the D2 classical-recovery witness.

/-- The reduction, packaged as a single implication for citation. -/
theorem d2_reduction_statement
    {α ρ : Type*} {l : Filter α}
    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
    D2QuadratureConvergenceTarget l family refinementFilter continuumIntegral →
    D2ResidualVanishingTarget l family refinementFilter →
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) family)
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds continuumIntegral) :=
  fun hquad hres => d2_reduction family refinementFilter continuumIntegral hquad hres

/-- The current D2 scope on the canonical periodic six-tet torus.

The `residual_target_open` flag refers to the residual target for an
arbitrary supplied schedule.  For the damped schedule class the target is a
theorem (`D2DampedScheduleClosure.dampedFamily_uniformResidual`), recorded in
the refined status below. -/
def d2ScopeStatus : D2ScopeStatus where
  reduction_proved := true
  quadrature_target_open := true
  residual_target_open := true
  general_triangulation_open := true

/-- D2 scope after `Gravity.D2DampedScheduleClosure`: one analytic input
(the quadrature limit) instead of two. -/
def d2ScopeStatusDamped : D2ScopeStatusDamped where
  reduction_proved := true
  quadrature_target_open := true
  residual_target_discharged_for_damped_schedules := true
  residual_target_open_for_arbitrary_schedules := true
  general_triangulation_open := true

What this page does not claim

The D2 reduction does not prove that the Einstein-Hilbert action is the unique continuum limit of Regge calculus. The theorem does not establish convergence for arbitrary triangulations, only for the canonical periodic six-tet cubic torus. The quadrature convergence target is not proved for curvature-bearing refinement families; it remains an open analytic input.

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/D2ScopingAudit.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: