Encyclopedia Gravity Gravity D2 Quadrature Instances Quadrature Integral Of Uniform Probe

ARTICLE 2 claims 2 theorems

Gravity D2 Quadrature Instances Quadrature Integral Of Uniform Probe

When every probe in a gravity simulation carries the same field value, a hard convergence question collapses into a simple numerical limit.

Verify this page

The uniform-probe reduction

In numerical gravity, a common way to approximate a continuous field is to sample it at many discrete points and sum the results. The Recognition Science framework formalizes this as a quadrature proxy, a discrete stand-in for a continuum integral. The declaration quadratureIntegral_of_uniform_probe proves a collapse: if every tetrahedron probe in a slice carries the same global potential, the proxy simplifies from a complicated sum over many cells into a single explicit formula.

The formula is a product of three factors: the number of tetrahedra, a fixed cell-weight constant (V/6), and half the canonical Dirichlet energy of the shared potential. The Dirichlet energy here is a standard measure of how much a field varies across a region; for a constant field it is zero. This collapse matters because the original quadrature target, a statement about convergence of opaque proxies, becomes for uniform-probe families an equivalent statement about a concrete scalar sequence of scaled Dirichlet energies. The theorem quadrature_target_iff_of_proxy_eq then transports the target along any explicit proxy formula, turning an abstract convergence question into a checkable numerical limit.

The declaration does not prove that this scalar Dirichlet limit actually converges for curved probe families; that remains open. It also does not establish the local correspondence data that each slice carries by definition, nor does it handle non-product, non-flat admissible triangulations. What it does is reduce the open D2 quadrature input for uniform-probe families to a much simpler problem, a concrete limit of finite graph-Dirichlet energies rather than an opaque proxy limit.

THEOREM quadratureIntegral_of_uniform_probe · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
quadratureIntegral_of_uniform_probe · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:215 
/-- For a slice whose tetrahedron probes are all the same global potential,
the quadrature proxy collapses to tetrahedron count times limiting cell
weight times the Dirichlet limit action of that potential. -/
theorem quadratureIntegral_of_uniform_probe
    {α : Type*} {l : Filter α}
    (S : CanonicalPeriodicTetSixTetVolumeQuadratureSlice l) :
    letI : NeZero S.Nx := S.instNx
    letI : NeZero S.Ny := S.instNy
    letI : NeZero S.Nz := S.instNz
    ∀ ξ : VertexPotential
        (canonicalEncodedPeriodicFreudenthalTorus S.Nx S.Ny S.Nz S.hx S.hy S.hz).K,
      (∀ τ : Fin (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz)),
        S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ) = ξ) →
      S.quadratureIntegral =
        (Fintype.card (PeriodicTet S.Nx S.Ny S.Nz) : ℝ) *
          (S.data.limitCellVolume / 6) *
          ((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
              ξ) := by
  letI : NeZero S.Nx := S.instNx
  letI : NeZero S.Ny := S.instNy
  letI : NeZero S.Nz := S.instNz
  intro ξ hξ
  have h : 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
              (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) := rfl
  rw [h]
  have hterm : ∀ τ : 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
            (S.data.tetProbe (tetFinEquiv S.Nx S.Ny S.Nz τ))) =
        S.data.limitCellVolume / 6 *
          ((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
              ξ) := by
    intro τ
    rw [hξ τ]
    simp only [canonicalPeriodicFreudenthalTetVolumeWeight]
  rw [Finset.sum_congr rfl fun τ _ => hterm τ]
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  ring
THEOREM quadrature_target_iff_of_proxy_eq · IndisputableMonolith/Gravity/D2QuadratureInstances.lean
quadrature_target_iff_of_proxy_eq · IndisputableMonolith/Gravity/D2QuadratureInstances.lean:271 
/-- Transport the cross-cardinality quadrature target along any explicit
formula for the slice proxies.  Together with
`quadratureIntegral_of_uniform_probe`, this turns the open D2 quadrature
input for uniform-probe families into a scalar limit of scaled Dirichlet
energies. -/
theorem quadrature_target_iff_of_proxy_eq
    {α ρ : Type*} {l : Filter α}
    (F : CanonicalPeriodicTetSixTetVolumeQuadratureRefinementFamily l ρ)
    (refinementFilter : Filter ρ) (continuumIntegral : ℝ)
    (g : ρ → ℝ)
    (hg : ∀ r : ρ, (F.slice r).quadratureIntegral = g r) :
    CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
      F refinementFilter continuumIntegral ↔
      Filter.Tendsto g refinementFilter (nhds continuumIntegral) := by
  unfold CanonicalPeriodicTetSixTetVolumeQuadratureCrossCardinalityTarget
  exact Filter.tendsto_congr hg

What this page does not claim

The scalar Dirichlet limit itself for curvature-bearing probe families is not proved. The Track 1.B local correspondence at each cardinality is not established by this declaration. The reduction does not apply to 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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND