Gravity D2 Scoping Audit D2 Reduction

The D2 reduction

Regge calculus is a discrete approximation to general relativity: it replaces smooth spacetime with a network of flat tetrahedra, and the Einstein-Hilbert action becomes a sum over the network's edge lengths. The D2 reduction is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that 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 quadrature convergence and residual vanishing. Quadrature convergence means the canonical periodic six-tet quadrature rule converges to the continuum integral. Residual vanishing means the difference between the full nonlinear Regge expression and the quadrature rule is uniformly controlled on the product filter. The theorem d2_reduction proves that these two conditions together imply the desired convergence. It is a reduction, not a from-primitives closure: it packages the convergence statement as an implication, so that proving the two inputs would complete the D2 target.

The theorem also discloses that the D2 target is a genuine convergence statement, not a trivial one. The declaration d2_target_is_convergence shows that the target is literally a Filter.Tendsto convergence of the full nonlinear Regge aggregate to the continuum integral. This matters because it prevents the target from being hidden inside a data structure or discharged by assumption.

What the reduction does not claim is as important as what it proves. It makes no claim about non-product or non-flat triangulations. The two analytic inputs, quadrature convergence and residual vanishing, remain open targets for arbitrary supplied schedules. The residual target is closed for damped schedules, where the spacing is rescaled per slice using the slice's own local cubic Taylor bound, but it remains open for arbitrary undamped schedules. The general-triangulation extension is the load-bearing geometric problem.

In Recognition Science, this reduction is the honest content of the D2 master witness. It names the precise remaining targets so they are not hidden. The framework's library shows that the reduction is proved with zero sorry and zero RS-internal axiom, but it does not assert that the open targets are closed. The reader can now see exactly what would complete the D2 target: prove the two analytic limits on the canonical torus, or extend the argument to non-product, non-flat triangulations.

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

/-- 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 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 quadrature convergence or residual vanishing from primitive mesh geometry. It does not cover non-product or non-flat triangulations. It does not assert that the residual target is closed for arbitrary supplied schedules.

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: