Gravity D2 Scalar Dirichlet Quadrature Limit Flat Family Quadrature Target Via S

The flat case

The declaration flatFamily_quadrature_target_via_scalar_limit belongs to a program that approximates a continuous gravitational action by sums over finer and finer tetrahedral meshes. In the flat case, where the geometry has no curvature, the theorem proves that this approximation converges to zero as the mesh is refined. The result is stated in a machine-checked library of formal theorems, meaning the proof has been verified by a computer.

The proof works by reducing the problem to a simpler one. The framework defines a scalar energy limit: a condition that a sequence of numbers, each measuring some energy on a mesh, converges to a target integral. For a flat family, this scalar energy is identically zero, because the relevant potential vanishes. The theorem then shows that this trivial scalar limit implies the desired quadrature convergence, using a general implication proved earlier in the library.

The flat case is a special case of a broader strategy. The library also proves that if a scalar Dirichlet energy limit holds for a family, and a damping schedule is applied, then the full product-filter convergence follows. The flat case satisfies the scalar limit trivially, so it recovers the flat-sector convergence through this route. The theorem is a clean, honest result: it establishes convergence for the flat sector, and it explicitly identifies the scalar limit for curvature-bearing probes as the remaining open input.

What the declaration does not claim is just as important. It does not prove the scalar Dirichlet energy limit for curved geometries. That limit, the concrete numerical value of finite graph-Dirichlet energies for curvature-bearing probes, remains an open analytic problem. The theorem only shows that if such a limit exists and converges, then the quadrature target follows. The flat case is a proof of concept, not a proof for general gravity.

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

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

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

What this page does not claim

The scalar Dirichlet energy limit for curvature-bearing probe families is not proved. The theorem does not establish convergence for any curved geometry, only for the flat family. The flat case does not demonstrate that the full gravity program succeeds; it only shows a special case works.

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: