Gravity D2 Scalar Dirichlet Quadrature Limit Flat Family Scalar Dirichlet Limit

The flat family's trivial limit

In numerical analysis, a quadrature rule approximates an integral by a weighted sum of function values at discrete points. The Recognition Science framework builds such rules on tetrahedral meshes and asks whether, as the mesh refines, the discrete sum approaches the true continuum integral. For a flat family, where the probe potential is identically zero, the answer is trivial: the sum is always zero and the integral is zero, so convergence is immediate.

The declaration flatFamily_scalarDirichletLimit packages this observation as a formal structure. It states that for the flat family, the scalar energy function is the constant zero function, the quadrature proxy equals this zero energy at every refinement, and the zero energies converge to the continuum integral zero. The proof is a direct application of the fact that a constant sequence converges to itself.

This flat case is a base case in a larger program. The framework proves a conditional theorem: if a scalar sequence of graph-Dirichlet energies converges to the continuum integral, then the full D2 quadrature convergence target holds. The flat family satisfies this hypothesis, so it inherits the quadrature target and, with a damped schedule, the full product-filter convergence to zero. These follow as corollaries of the scalar limit route.

The declaration does not claim the hard part. For curvature-bearing probe families, the scalar Dirichlet energy limit remains an open analytic input. The structure demands a genuine convergence proof for those cases, and that proof is not supplied here. The flat case is a check that the machinery is consistent, not a solution to the general problem.

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

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

What this page does not claim

The declaration does not prove the scalar Dirichlet energy limit for curvature-bearing probes. It does not establish any numerical value for a curved-space quadrature limit. It does not claim the flat case is physically interesting beyond being a consistency check.

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: