Gravity D2 Quadrature Instances Flatten Slice Quadrature Integral

The flat slice's quadrature integral

The declaration flattenSlice_quadratureIntegral is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It concerns a quadrature slice, a discrete record of geometric data attached to a tetrahedral mesh, used to approximate a continuum integral. The theorem states that if you take any such slice and flatten it, meaning you replace every tetrahedron probe with the zero potential, then the slice's quadrature integral is exactly zero.

The proof is immediate from a more basic fact: the canonical Dirichlet energy of the zero potential vanishes. Since the quadrature integral is built from these energies, flattening forces the integral to zero. This is not an approximation or a limit; it is an exact equality, holding for every slice that satisfies the incidence consistency condition.

This single theorem powers a broader result. When an entire family of slices is flattened, every quadrature proxy becomes identically zero, so the family's quadrature target holds at the continuum value 0 with no additional hypotheses. Combined with a separate damped-residual closure, this yields the full nonlinear Regge aggregate of the damped flattened family converging to the flat Einstein-Hilbert value 0 on the product filter. The flat sector of the D2 reduction is thereby closed end to end, with both former analytic inputs now proved rather than supplied.

In Recognition Science, this matters because the D2 reduction is a step toward showing that the framework's discrete geometry recovers continuum gravity. The flattening result is the easy case: it confirms that when all curvature-bearing content is removed, the discrete approximation agrees with the flat continuum value exactly. The hard case, where probes carry curvature, remains open.

What the theorem does not claim is just as important. It does not establish the scalar Dirichlet limit for curvature-bearing probe families, which is the genuine Riemann-sum content of D2. It does not prove the Track 1.B local correspondence at each cardinality, which slices carry as a standing assumption. And it says nothing about non-product, non-flat admissible triangulations. The flat sector is closed; the curved sector is reduced to a concrete numerical limit, but that limit itself remains an open target.

/-- The flattened slice's quadrature proxy is exactly zero. -/
theorem flattenSlice_quadratureIntegral
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
    (flattenSlice S).quadratureIntegral = 0 := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  have h : (flattenSlice S).quadratureIntegral =
      ∑ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        canonicalPeriodicFreudenthalTetVolumeWeight S.Nx S.Ny S.Nz
            S.data.limitCellVolume (tetFinEquiv S.Nx S.Ny S.Nz τ) *
          ((1 / 2) *
            canonicalDirichletEnergy
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K
              (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).hK
              (zeroPotential
                (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K)) :=
    rfl
  rw [h]
  simp [canonicalDirichletEnergy_zero]

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

/-- **The flat-sector quadrature target holds with no hypothesis.**  The
flattened family's quadrature proxies are identically zero, so they converge
to the flat continuum Einstein-Hilbert value `0` along every refinement
filter. -/
theorem flatFamily_quadrature_target
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) :
    CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
      (flatFamily F) refinementFilter 0 := by
  unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
  have h : (fun r : ρ => ((flatFamily F).slice r).quadratureIntegral) =
      fun _ : ρ => (0 : ℝ) := by
    funext r
    exact flattenSlice_quadratureIntegral (F.slice r)
  rw [h]
  exact tendsto_const_nhds

/-- **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 establish the scalar Dirichlet limit for curvature-bearing probe families. The theorem does not prove the Track 1.B local correspondence at each cardinality. The theorem says nothing about 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: