Encyclopedia Gravity Gravity D2 Scalar Dirichlet Quadrature Limit Scalar Dirichlet Energy Limit

ARTICLE 5 claims 3 theorems 1 model

Gravity D2 Scalar Dirichlet Quadrature Limit Scalar Dirichlet Energy Limit

A machine-checked theorem shows that a single unproved numerical limit would complete a key gravity calculation, but that limit itself remains open.

Verify this page

The scalar Dirichlet limit

In numerical gravity, a common goal is to show that a sequence of discrete approximations converges to a smooth continuum answer as the mesh is refined. The Recognition Science framework's ledger, a discrete record of events, reaches this goal through a specific structure called Dirichlet energy, a measure of how much a field varies across a region. The declaration ScalarDirichletEnergyLimit packages the hypothesis that a single scalar sequence of these energies converges to the desired continuum integral. The framework's machine-checked library of formal theorems proves a conditional statement: if this scalar limit holds, then the full D2 quadrature convergence target is achieved.

The proof works by connecting the scalar energy to the quadrature proxies, the discrete sums that approximate the integral. A theorem named scalar_dirichlet_limit_implies_d2_quadrature_target establishes this implication. When combined with a separate damped-schedule closure, which handles residual terms for damped families, the scalar limit alone suffices for the full nonlinear Regge aggregate to converge to the continuum Einstein-Hilbert/Dirichlet integral. This is the sharpest reduction of the D2 problem to a single analytic input: one numerical limit for curvature-bearing probe families.

The flat case, where the probe potential is zero, is handled completely. The Dirichlet energy of the zero potential vanishes, so the scalar limit holds trivially at zero. Theorems recover the flat-sector quadrature target and full product-filter convergence through this scalar route. This provides a fully proved baseline for the simplest case.

What the declaration does not claim is the scalar limit itself for curvature-bearing families. The tendsto field, which asserts the concrete numerical limit of finite graph-Dirichlet energies, remains the genuine Riemann-sum content of D2 and is not proved here. For uniform-probe slices, the proxy equality is discharged by a separate instance, collapsing the quadrature proxy to a product of the number of tetrahedra, a volume factor, and half the Dirichlet energy. But the convergence of that energy to the continuum integral for curved probes stays an open analytic input, a named target rather than an established result.

MODEL ScalarDirichletEnergyLimit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean
ScalarDirichletEnergyLimit · IndisputableMonolith/Gravity/D2ScalarDirichletQuadratureLimit.lean:64 
/-- The scalar Dirichlet energy limit hypothesis for a quadrature refinement
family.  This packages the explicit numerical limit of finite graph-Dirichlet
energies that the D2 quadrature target reduces to for uniform-probe families.

For uniform-probe families, the `proxy_eq` field is discharged by
`D2QuadratureInstances.quadratureIntegral_of_uniform_probe`, which collapses
the quadrature proxy to `(card tets) · (V/6) · (½ · DirichletEnergy ξ)`.
The `tendsto` field is then the concrete scalar Dirichlet energy limit — the
genuine Riemann-sum content of D2 that remains open for curvature-bearing
probes. -/
structure ScalarDirichletEnergyLimit
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) where
  /-- The scalar energy function: typically the scaled Dirichlet energy of
  the uniform probe at each refinement. -/
  scalarEnergy : ρ → ℝ
  /-- The scalar energy computes the quadrature proxy at each refinement.
  For uniform-probe slices, this is `quadratureIntegral_of_uniform_probe`. -/
  proxy_eq : ∀ r : ρ, (F.slice r).quadratureIntegral = scalarEnergy r
  /-- The scalar Dirichlet energies converge to the continuum integral.
  This is the open analytic input for curvature-bearing probe families. -/
  tendsto : Filter.Tendsto scalarEnergy refinementFilter (nhds continuumIntegral)
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

What this page does not claim

The scalar Dirichlet energy limit for curvature-bearing probes is not proved, only the conditional implication from it. The flat case convergence does not extend to curved probe families without the open tendsto input. The declaration does not establish the D2 quadrature target unconditionally; it requires the scalar limit hypothesis.

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