Encyclopedia Gravity Gravity D2 Scoping Audit D2 Scope Status

ARTICLE 3 claims 3 theorems

Gravity D2 Scoping Audit D2 Scope Status

A machine-checked status record that says exactly what is proved in a gravity derivation and, just as precisely, what remains open.

Verify this page

Scope status

D2ScopeStatus is a small data structure in the framework's machine-checked library of formal theorems. It records, as four boolean flags, the current state of a particular derivation in discrete gravity: whether a reduction theorem is proved, and whether three further targets remain open. The declaration exists to make the boundary between proved and unproved explicit and auditable, so that no one mistakes a conditional result for a closed one.

The derivation in question concerns how a discrete model of spacetime, built from tetrahedra on a periodic torus, converges to the continuum Einstein-Hilbert action as the mesh refines. The reduction theorem, proved in the library, states that if two analytic conditions hold, then the full nonlinear discrete aggregate converges to the continuum integral. The first condition is that a quadrature rule converges to the integral; the second is that a residual term vanishes uniformly. D2ScopeStatus records that the reduction is proved, and that both conditions, plus the extension to general triangulations, remain open.

The status record has a refined companion, D2ScopeStatusDamped, which reflects a later closure. For a class of "damped" refinement schedules, the residual vanishing condition is no longer an open input: it is derived from a local cubic bound, leaving only the quadrature convergence as the remaining analytic target. The refined record states this precisely, distinguishing the damped case from arbitrary supplied schedules, where the residual target stays open.

What D2ScopeStatus does not claim is as important as what it records. It does not assert that the reduction theorem holds unconditionally; it merely records that the reduction is proved conditional on the two analytic inputs. It does not claim that the quadrature convergence or residual vanishing are established; the flags mark them open. And it makes no claim about non-product or non-flat triangulations, which remain the load-bearing geometric problem. The declaration is a scope audit, not a proof of the full convergence result.

THEOREM D2ScopeStatus · d2ScopeStatus · IndisputableMonolith/Gravity/D2ScopingAudit.lean
D2ScopeStatus · IndisputableMonolith/Gravity/D2ScopingAudit.lean:169 
/-- Honest D2 scope: the reduction is proved; the two analytic inputs and the
general-triangulation extension are open. -/
structure D2ScopeStatus where
  reduction_proved : Bool
  quadrature_target_open : Bool
  residual_target_open : Bool
  general_triangulation_open : Bool
d2ScopeStatus · IndisputableMonolith/Gravity/D2ScopingAudit.lean:177 
/-- 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
THEOREM d2_reduction · IndisputableMonolith/Gravity/D2ScopingAudit.lean
d2_reduction · IndisputableMonolith/Gravity/D2ScopingAudit.lean:125 
/-- **D2 REDUCTION THEOREM (what is actually proved).**  On the canonical
periodic six-tet cubic torus, the two named analytic targets — quadrature
convergence to the continuum integral and a vanishing Regge-residual — imply
that the full nonlinear Regge aggregate converges to the continuum
Einstein-Hilbert/Dirichlet integral on the product filter.

This is the honest content of the D2 master witness: convergence is reduced
to the two analytic inputs, which remain the open targets (§2).  It makes no
claim about non-product or non-flat triangulations. -/
theorem d2_reduction
    {α ρ : Type*} {l : Filter α}
    (family : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (hquad : D2QuadratureConvergenceTarget l family refinementFilter continuumIntegral)
    (hres : D2ResidualVanishingTarget l family refinementFilter) :
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) family)
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds continuumIntegral) :=
  (CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData.fullReggeProduct_tendsto_continuum
    (α := α) (ρ := ρ) (l := l)
    { family := family
      refinementFilter := refinementFilter
      continuumIntegral := continuumIntegral
      quadrature_tendsto := hquad
      uniform_residual := hres })
THEOREM D2ScopeStatusDamped · d2ScopeStatusDamped · IndisputableMonolith/Gravity/D2ScopingAudit.lean
D2ScopeStatusDamped · IndisputableMonolith/Gravity/D2ScopingAudit.lean:189 
/-- Refined D2 scope after the damped-schedule closure (2026-06-11). -/
structure D2ScopeStatusDamped where
  reduction_proved : Bool
  quadrature_target_open : Bool
  /-- The uniform residual is derived from the per-slice local cubic bound
  for the damped schedule class; it is no longer an independent analytic
  input for D2. -/
  residual_target_discharged_for_damped_schedules : Bool
  /-- The residual target for arbitrary (undamped) supplied schedules. -/
  residual_target_open_for_arbitrary_schedules : Bool
  general_triangulation_open : Bool
d2ScopeStatusDamped · IndisputableMonolith/Gravity/D2ScopingAudit.lean:201 
/-- 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

D2ScopeStatus does not assert that the reduction theorem holds unconditionally. It does not claim that the quadrature convergence or residual vanishing targets are proved. It makes no claim about convergence on non-product or non-flat 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/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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND