Gravity D2 Quadrature Instances Canonical Dirichlet Energy Zero

The zero-energy flat slice

The theorem canonicalDirichletEnergy_zero states a fact so plain it can sound trivial: for any consistent triangulation of a three-dimensional space, the canonical Dirichlet energy (a measure of how much a field varies across a region) of the zero potential is exactly zero. A field that is zero everywhere has no variation, so its energy is zero. The declaration proves this by unfolding definitions and simplifying, a direct calculation in the machine-checked library of formal theorems.

The result matters because of what it enables. In the framework's program to derive gravity from a discrete ledger of recognition events, a family of triangulations is "flattened" by replacing every probe with the zero potential. The theorem guarantees that each flattened slice has a quadrature proxy of exactly zero, which means the approximation's integral converges to the flat value 0 with no extra hypothesis. This closes the flat sector of the D2 reduction: the full nonlinear Regge aggregate of the damped flattened family converges to the flat Einstein-Hilbert value on the product filter, with both former analytic inputs proved rather than supplied.

The theorem does not claim anything about curved space. For slices whose probes are all equal to one global potential, the quadrature proxy collapses to a scalar Dirichlet limit, but the convergence of that scalar sequence for curvature-bearing families remains open. The theorem also does not establish the Track 1.B local correspondence at each cardinality, nor does it handle non-product, non-flat admissible triangulations. It is a precise, narrow result: zero potential, zero energy, flat sector closed.

theorem canonicalDirichletEnergy_zero
    (K : Triangulation3D) (hK : IncidenceConsistent K) :
    canonicalDirichletEnergy K hK (zeroPotential K) = 0 := by
  unfold canonicalDirichletEnergy zeroPotential
  simp

/-- **FLAT-SECTOR D2 CLOSURE (no supplied analytic inputs).**  For every
slice family and every universal schedule, the full nonlinear Regge aggregate
of the damped flattened family converges to the flat continuum value `0` on
the product filter.  Both former analytic inputs are theorems here: the
quadrature target by §3, the uniform residual by the damped-schedule
closure.  The only data consumed are the slices themselves, including the
Track 1.B local correspondence they carry by definition. -/
theorem dampedFlat_fullReggeProduct_tendsto_zero
    {α ρ : 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) :=
  dampedFamily_fullReggeProduct_tendsto_continuum (flatFamily F) σ hσ0 hσne
    refinementFilter 0 (flatFamily_quadrature_target F refinementFilter)

What this page does not claim

The theorem does not prove anything about curved space or non-zero potentials. The theorem does not establish the scalar Dirichlet limit for curvature-bearing families. The theorem does not handle non-product, non-flat admissible triangulations.

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/D2QuadratureInstances.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: