Gravity D2 Scoping Audit

The D2 scoping audit

Regge calculus is a discrete approach to general relativity, where spacetime is built from flat triangular pieces, and gravity emerges as the pieces are refined. The D2 scoping audit in Recognition Science examines a specific convergence claim: as the discrete pieces shrink, does the full nonlinear Regge action approach the continuum Einstein-Hilbert action? The audit's plain verdict is that this convergence is reduced, not yet fully established, to two analytic conditions, and one of those conditions has now been discharged for a wide class of refinement schedules.

The audit begins by stating exactly what the target is. The target is a genuine convergence statement, a filter limit of the discrete Regge aggregate to the continuum integral. It is not a tautology and it does not mention the master conclusion. The audit then names the two analytic inputs that would complete the proof: quadrature convergence, meaning the discrete summation rule approaches the continuum integral, and residual vanishing, meaning the difference between the full nonlinear Regge expression and the quadrature rule shrinks uniformly.

The central proved result is a reduction theorem. On the canonical periodic six-tet cubic torus, the audit proves that if both analytic conditions hold, then the full nonlinear Regge aggregate converges to the continuum Einstein-Hilbert integral. This is a genuine theorem, machine-checked with no unproved assumptions. The reduction is packaged cleanly as an implication: quadrature convergence and residual vanishing together force the desired convergence. This is the honest content of the D2 master witness.

In June 2026, the residual vanishing target was closed for damped schedules. For every slice family, a damped rescheduling, where the spacing is reduced per slice according to constants computed from the slice's own local cubic Taylor bound, satisfies the residual vanishing target outright. This means the full nonlinear product-filter convergence now needs only the quadrature limit, not both conditions. The residual target for an arbitrary supplied schedule remains open, but it is no longer an independent analytic input for D2.

What remains open is precisely stated. The quadrature convergence target for curvature-bearing families is not yet discharged from primitive mesh geometry, though the flat sector closes with no hypothesis. The generalization beyond the canonical periodic, flat, product six-tet torus to physically admissible non-product, non-flat triangulations is the load-bearing geometric problem. The audit's value is that it tells you exactly which of these is a proved theorem and which is a named target, so no one mistakes the reduction for a from-primitives closure.

/-- The D2 product-filter target is literally a `Filter.Tendsto` convergence
of the full nonlinear Regge aggregate to the continuum integral.  It is not
`True` and it does not mention the master conclusion. -/
theorem d2_target_is_convergence
    {α ρ : Type*} {l : Filter α}
    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
    Track1BCPhysicalResidual.PhysicalReggeEHConcreteProductFilterTarget D =
      Filter.Tendsto
        (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
          (α := α) (ρ := ρ) D.family)
        (D.refinementFilter ×ˢ l : Filter (ρ × α))
        (nhds D.continuumIntegral) := rfl

/-- **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 })

/-- 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 convergence is not proved from primitive mesh geometry for general curvature-bearing families. The reduction does not extend to non-product or non-flat triangulations. The residual vanishing for arbitrary supplied schedules is not proved. This audit does not claim the full Einstein-Hilbert action is derived from Regge calculus without the named analytic inputs.

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: