Gravity D2 Scalar Dirichlet Quadrature Limit Damped Flat Full Regge Product Tend

The flat damped limit

The declaration dampedFlat_fullReggeProduct_tendsto_zero_via_scalar_limit is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It establishes a convergence result for a specific family of discrete gravity models. In plain terms, it says that if you take a flat (zero-probe) family of tetrahedral volume quadratures, apply a damping schedule that shrinks a parameter to zero while never exactly hitting zero, and then form the full Regge product aggregate, this aggregate tends to zero on the product filter. The proof routes through a scalar Dirichlet energy limit: the flat family satisfies this limit trivially because its scalar energy is identically zero.

The theorem is a corollary of two more general results. The first, scalar_dirichlet_limit_implies_d2_quadrature_target, proves that if a scalar sequence of graph-Dirichlet energies converges to a continuum integral, then the D2 quadrature convergence target holds. The second, scalar_limit_and_damped_implies_full_convergence, combines that scalar limit with the damped-schedule closure to force full product-filter convergence. The flat case is the easy instance: the scalar energy is zero, zero converges to zero, and the D2 target is recovered. This is a fully proved statement with zero gaps and zero RS-internal axioms.

What the theorem does not claim is the hard part. The scalar Dirichlet energy limit for curvature-bearing probe families, the case where the probes are not flat, remains an open analytic input. The tendsto field of ScalarDirichletEnergyLimit, which packages the concrete numerical limit of finite graph-Dirichlet energies, is not proved for curvature-bearing uniform-probe families. That limit is the genuine Riemann-sum content of the D2 problem. The flat theorem works because the energy is trivially zero, not because the general limit has been established.

The practical consequence is a sharp reduction of the open D2 target. For the flat sector, convergence is settled. For the curvature-bearing sector, the entire remaining difficulty collapses into a single named analytic input: the scalar graph-Dirichlet energy limit. If that limit is ever proved, the full D2 product-filter convergence follows immediately by the theorems already in the library.

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

/-- 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 here. The theorem does not establish convergence for non-flat families. The result does not derive the fine-structure constant or any other physical constant.

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: