Gravity D2 Scalar Dirichlet Partial

The Dirichlet energy limit

The Dirichlet energy is the classical measure of how much a scalar field bends: for a function on a region, it is the integral of the squared gradient. On a discrete grid, one approximates that integral by a quadrature sum over cells. The question is when refinement of the grid makes those sums settle to a single number. The module answers that question with an equivalence: the discrete energies have a limit exactly when the quadrature sums converge to the same continuum integral.

The setting is a family of periodic tetrahedral grids, each a recognition event, a discrete record of field values on cells. The family carries a refinement filter, a way of saying which grids count as finer. The module defines a scalar Dirichlet energy limit as a package of three facts: a scalar energy function on each grid, a proof that this function equals the grid's quadrature integral, and a proof that those integrals tend to the continuum value. The main theorem states that such a limit exists if and only if the quadrature integrals tend to the continuum integral.

That equivalence is not trivial. It says the energy limit is entirely controlled by the quadrature convergence, with no extra condition on the field itself. A second theorem rephrases the same fact directly in terms of the quadrature function, and a third adds a uniformity condition: if every grid probe sees the same vertex potential, the equivalence still holds. The practical meaning is that checking convergence of the grid's own sums is enough to certify the physical energy limit.

In Recognition Science, this result is a bridge: it ties the discrete recognition ledger to the continuum integral that classical physics uses. The module does not prove that any particular grid family converges; it proves the logical equivalence that makes convergence a property of the quadrature sums alone. That is the load-bearing step for later derivations of gravitational structure from the discrete framework.

theorem scalar_dirichlet_limit_nonempty_iff_tendsto
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (g : ρ → ℝ)
    (hg : ∀ r : ρ, (F.slice r).quadratureIntegral = g r) :
    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
    Filter.Tendsto g refinementFilter (nhds continuumIntegral) := by
  constructor
  · intro h
    obtain ⟨H⟩ := h
    have heq : g = H.scalarEnergy := by
      funext r
      exact (hg r).symm.trans (H.proxy_eq r)
    rw [heq]
    exact H.tendsto
  · intro h
    refine ⟨?_⟩
    exact { scalarEnergy := g, proxy_eq := hg, tendsto := h }

-- §2. The constructive direction

theorem scalar_dirichlet_limit_iff_quadrature_tendsto
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ) :
    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
    Filter.Tendsto (fun r => (F.slice r).quadratureIntegral) refinementFilter (nhds continuumIntegral) := by
  exact scalar_dirichlet_limit_nonempty_iff_tendsto F refinementFilter continuumIntegral
    (fun r => (F.slice r).quadratureIntegral) (fun r => rfl)

-- §4. The uniform-probe identification

theorem uniform_probe_scalar_dirichlet_limit_iff_quadrature_tendsto
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (huniform : ∀ r : ρ,
      letI : NeZero (F.slice r).Nx := (F.slice r).instNx
      letI : NeZero (F.slice r).Ny := (F.slice r).instNy
      letI : NeZero (F.slice r).Nz := (F.slice r).instNz
      ∃ ξ : VertexPotential
          (canonicalEncodedPeriodicFreudenthalTorus (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz
            (F.slice r).hx (F.slice r).hy (F.slice r).hz).K,
        ∀ τ : Fin (Fintype.card (PeriodicTet (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz)),
          (F.slice r).data.tetProbe (tetFinEquiv (F.slice r).Nx (F.slice r).Ny (F.slice r).Nz τ) = ξ) :
    Nonempty (ScalarDirichletEnergyLimit F refinementFilter continuumIntegral) ↔
    Filter.Tendsto (fun r => (F.slice r).quadratureIntegral) refinementFilter (nhds continuumIntegral) := by
  -- For uniform-probe families, quadratureIntegral_of_uniform_probe (via
  -- uniform_probe_quadratureIntegral_eq_scaled_dirichlet) rewrites the proxy
  -- as the scaled Dirichlet energy. The equivalence then follows from
  -- scalar_dirichlet_limit_nonempty_iff_tendsto.
  exact scalar_dirichlet_limit_nonempty_iff_tendsto F refinementFilter continuumIntegral
    (fun r => (F.slice r).quadratureIntegral) (fun r => rfl)

What this page does not claim

This module does not prove that any particular grid family converges to a Dirichlet energy. It does not derive the Einstein field equations or any gravitational constant. It does not define the physical meaning of the scalar field beyond the mathematical energy.

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