Gravity D2 Quadrature Instances Quadrature Target Iff Of Proxy Eq

The proxy equivalence

In the Recognition Science framework, gravity is studied not as a continuous field but as a discrete structure built from tetrahedra, the smallest building blocks of a curved space. The framework's library of formal theorems works with a quantity called the quadrature proxy, a number attached to each slice of this discrete structure that measures how close that slice comes to reproducing the continuous Einstein-Hilbert action of general relativity. The declaration quadrature_target_iff_of_proxy_eq (a machine-checked theorem in the framework's library) establishes a bridge: if you can write down an explicit formula for the proxy on every slice, then the condition that the proxies converge to a target value is exactly equivalent to the condition that your formula converges to that same value.

The theorem itself is a formal statement about limits. It says that for any family of slices, any filter on the refinement index, and any real number representing the continuum integral, if the quadrature proxy on each slice equals some function g of the refinement parameter, then the cross-cardinality quadrature target holds for that family if and only if the function g tends to the continuum integral along the refinement filter. In plainer terms: the abstract, opaque condition that a family of discrete approximations converges to a continuum value is logically identical to the concrete condition that an explicit sequence of numbers converges. The proof is a one-line application of the fact that two functions which agree pointwise have the same limit behavior.

This equivalence matters because it transforms an open problem. The framework's D2 reduction program needs to show that certain discrete quadrature schemes converge to the correct continuum gravitational action. Before this theorem, the convergence condition was stated in terms of the proxies themselves, which are complex objects built from the geometry of tetrahedra. After the theorem, for any family where the proxy has an explicit formula, the convergence condition becomes a statement about a simple real-valued sequence. The theorem is used in the framework to show that for uniform-probe families, where every tetrahedron carries the same potential, the quadrature target is equivalent to the convergence of a scalar sequence of scaled Dirichlet energies.

What the theorem does not claim is equally important. It does not prove that any particular family of slices satisfies the quadrature target. It only establishes the equivalence between two formulations of the target condition. The theorem does not supply the explicit formula g for any specific family; it requires such a formula as a hypothesis. And it does not prove that the scalar Dirichlet energy limit itself converges for curvature-bearing probe families. That genuine Riemann-sum content remains open in the framework. The theorem is a logical tool that reduces one problem to another, not a solution to the underlying convergence question.

/-- 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 theorem does not prove that any particular discrete gravity family converges to the continuum. The theorem does not supply the explicit proxy formula; it requires one as a hypothesis. The theorem does not establish the scalar Dirichlet energy limit for curved probe families, which remains open.

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: