Encyclopedia Gravity Gravity D2 Scalar Dirichlet Quadrature Limit

ARTICLE 5 claims 5 theorems

Gravity D2 Scalar Dirichlet Quadrature Limit

A machine-checked proof reduces a hard gravity convergence question to one concrete numerical limit, and shows the flat case already works.

Verify this page

The scalar limit

In Recognition Science, gravity emerges from a discrete ledger: a record of recognition events on a periodic lattice of tetrahedra. The D2 quadrature problem asks whether, as the lattice refines, the discrete sum over tetrahedra converges to the continuum Einstein-Hilbert integral. The module D2ScalarDirichletQuadratureLimit (a machine-checked library of formal theorems) establishes a conditional result: if a certain scalar sequence of graph-Dirichlet energies converges to the continuum integral, then the full D2 quadrature convergence target follows. The scalar energy is a function g : ρ → ℝ connected to the quadrature proxies by proxy_eq and converging to the continuum integral by tendsto.

The main theorem, scalar_dirichlet_limit_implies_d2_quadrature_target, proves this implication. It uses the proxy-transport theorem D2QuadratureInstances.quadrature_target_iff_of_proxy_eq to connect the scalar energy to the quadrature proxies. Combined with the damped-schedule closure (D2DampedScheduleClosure.dampedFamily_fullReggeProduct_tendsto_continuum), the scalar Dirichlet energy limit alone suffices for the full D2 product-filter convergence, as shown by scalar_limit_and_damped_implies_full_convergence. This is the sharpest reduction of D2 to a single analytic input: the scalar graph-Dirichlet energy limit for curvature-bearing probe families.

The flat case is fully proved. The flat family (zero probes) satisfies ScalarDirichletEnergyLimit at zero trivially, since the Dirichlet energy of the zero potential vanishes. This recovers the flat-sector quadrature target and full product-filter convergence via the scalar Dirichlet route, as shown by flatFamily_quadrature_target_via_scalar_limit and dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit. So for the flat sector, the D2 quadrature convergence is established unconditionally.

What remains open is the tendsto field of ScalarDirichletEnergyLimit for curvature-bearing uniform-probe families: the concrete numerical limit of finite graph-Dirichlet energies. This is the genuine Riemann-sum content of D2 and is not proved here. For uniform-probe slices, the proxy_eq field is discharged by D2QuadratureInstances.quadratureIntegral_of_uniform_probe, which collapses the quadrature proxy to (card tets) · (V/6) · (½ · DirichletEnergy ξ). The scalar limit itself for curvature-bearing probes remains the open analytic content of D2.

In plain language: the module proves that if one can show a certain scalar energy sequence converges, then the whole D2 gravity quadrature converges. It also proves the flat case works unconditionally. The remaining hard part is the concrete numerical limit for curved space, which is a named open target, not a proved theorem.

THEOREM scalar_dirichlet_limit_implies_d2_quadrature_target · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
scalar_dirichlet_limit_implies_d2_quadrature_target · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:90 
/-- **The scalar Dirichlet energy limit implies the D2 quadrature convergence
target.**  This is the sharpest honest conditional implication for the
curvature-bearing sector: if a scalar sequence of graph-Dirichlet energies
(connected to the quadrature proxies by `proxy_eq`) converges to the
continuum integral, then the D2 quadrature convergence target holds.

Combined with the damped-schedule residual closure
(`D2DampedScheduleClosure`), this reduces the full D2 product-filter
convergence to the scalar Dirichlet energy limit alone (see
`scalar_limit_and_damped_implies_full_convergence`).

The scalar limit itself for curvature-bearing probes remains the open
analytic content of D2. -/
theorem scalar_dirichlet_limit_implies_d2_quadrature_target
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (H : ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) :
    D2ScopingAudit.D2QuadratureConvergenceTarget l F refinementFilter continuumIntegral :=
  (quadrature_target_iff_of_proxy_eq
    F refinementFilter continuumIntegral H.scalarEnergy H.proxy_eq).mpr H.tendsto
THEOREM scalar_limit_and_damped_implies_full_convergence · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
scalar_limit_and_damped_implies_full_convergence · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:114 
/-- **The scalar Dirichlet energy limit plus the damped schedule implies full
D2 product-filter convergence.**  Since the damped-schedule closure
discharges the uniform residual target unconditionally for damped schedules
(via `dampedFamily_fullReggeProduct_tendsto_continuum`), the scalar
Dirichlet energy limit alone suffices for the full nonlinear Regge aggregate
to converge to the continuum Einstein-Hilbert/Dirichlet integral on the
product filter.

This is the sharpest reduction of D2 to a single analytic input: the scalar
graph-Dirichlet energy limit for curvature-bearing probe families. -/
theorem scalar_limit_and_damped_implies_full_convergence
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (σ : α → ℝ)
    (hσ0 : Filter.Tendsto σ l (nhds 0))
    (hσne : ∀ᶠ t : α in l, σ t ≠ 0)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (H : ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) :
    Filter.Tendsto
      (CanonicalPeriodicTetSixTetVolumeQuadratureProductFullReggeAggregate
        (α := α) (ρ := ρ) (dampedFamily F σ hσ0 hσne))
      (refinementFilter ×ˢ l : Filter (ρ × α))
      (nhds continuumIntegral) :=
  dampedFamily_fullReggeProduct_tendsto_continuum F σ hσ0 hσne
    refinementFilter continuumIntegral
    (scalar_dirichlet_limit_implies_d2_quadrature_target F refinementFilter
      continuumIntegral H)
THEOREM flatFamily_scalarDirichletLimit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
flatFamily_scalarDirichletLimit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:144 
/-- The flat family satisfies the scalar Dirichlet energy limit at zero:
the scalar energy is identically zero (the Dirichlet energy of the zero
potential vanishes), and zero converges to zero. -/
noncomputable def flatFamily_scalarDirichletLimit
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) :
    ScalarDirichletEnergyLimit (flatFamily F) refinementFilter 0 where
  scalarEnergy := fun _ => 0
  proxy_eq := by
    intro r
    exact flattenSlice_quadratureIntegral (F.slice r)
  tendsto := tendsto_const_nhds
THEOREM flatFamily_quadrature_target_via_scalar_limit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
flatFamily_quadrature_target_via_scalar_limit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:158 
/-- The flat-sector quadrature target follows from the scalar limit
hypothesis, recovering `D2QuadratureInstances.flatFamily_quadrature_target`
via the scalar Dirichlet route. -/
theorem flatFamily_quadrature_target_via_scalar_limit
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) :
    D2ScopingAudit.D2QuadratureConvergenceTarget l (flatFamily F) refinementFilter 0 :=
  scalar_dirichlet_limit_implies_d2_quadrature_target (flatFamily F) refinementFilter 0
    (flatFamily_scalarDirichletLimit F refinementFilter)
THEOREM dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:169 
/-- The flat-sector full product-filter convergence follows from the scalar
limit hypothesis, recovering
`D2QuadratureInstances.dampedFlat_fullReggeProduct_tendsto_zero` via the
scalar Dirichlet route. -/
theorem dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit
    {α ρ : 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) :=
  scalar_limit_and_damped_implies_full_convergence (flatFamily F) σ hσ0 hσne
    refinementFilter 0 (flatFamily_scalarDirichletLimit F refinementFilter)

What this page does not claim

The scalar Dirichlet energy limit for curvature-bearing probe families is not proved. The D2 quadrature convergence target for curved space is not established unconditionally. The module does not provide the numerical value of the continuum integral for curved space.

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/D2ScalarDirichletQuadratureLimit.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