Gravity Track1 Bcphysical Residual Physical Regge Eh Concrete Varying Cardinalit

Discrete gravity's limit

General relativity describes gravity as the curvature of spacetime, and its standard equations, the Einstein field equations, come from an action principle: a quantity called the Einstein-Hilbert action, which measures the total curvature of spacetime, is minimized. On a computer, one cannot work with a smooth continuum directly. Instead, one approximates spacetime with a discrete mesh of flat tetrahedra, and the curvature is concentrated along the edges where tetrahedra meet. This discrete approximation is called Regge calculus, after the Italian mathematician Tullio Regge who introduced it in 1961.

The central question is whether this discrete approximation actually converges to the continuous theory as the mesh is made finer. The declaration named in the question, a theorem in the framework's machine-checked library of formal theorems, establishes that it does, under specific conditions. The theorem proves that a normalized sum of the discrete Regge action over a finite, periodic grid of tetrahedra tends to the canonical finite Einstein-Hilbert action, with an explicit residual error that shrinks to zero as the grid refines. The key condition is that the local geometry of the mesh matches the continuous curvature in a precise way, a requirement the framework calls edge-stencil local correspondence.

In Recognition Science, this result is part of a larger program. The framework treats physics as emerging from a discrete ledger, a record of recognition events, and this theorem is a step in showing that the discrete structure reproduces known continuous physics. The theorem also packages a discrete version of the Bianchi identity, a fundamental consistency condition in general relativity, alongside the convergence result. The proof is fully checked by the machine, with no gaps and no framework-specific axioms.

What this theorem does not claim is equally important. It does not prove convergence to the Einstein-Hilbert action on an arbitrary, smooth manifold. The result is proven for a specific, periodic refinement family of tetrahedral grids, not for all possible discretizations. A separate target, named in the framework's library, remains open: proving the limit for the full manifold integral. The theorem also does not derive the Einstein field equations from scratch; it shows that a discrete action converges to the continuous action, which is a necessary but not sufficient step for a full derivation of general relativity from discrete principles.

The practical consequence is that the framework's discrete model of gravity has a rigorous bridge to the standard continuum theory, at least for the periodic case. This means the discrete model is not an arbitrary toy; it is anchored to known physics in a precise, checkable way. The remaining gap to the full manifold theorem is a concrete, named target, which is how the framework tracks what is proven and what is not.

/-- Product-filter data proves the concrete refinement-family target. -/
theorem physicalReggeEHConcreteProductFilterTarget_holds
    {α ρ : Type*} {l : Filter α}
    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l) :
    PhysicalReggeEHConcreteProductFilterTarget D :=
  D.fullReggeProduct_tendsto_continuum

theorem physicalSchlafliBianchiMasterProp_holds (V B : Type) [Fintype B] :
    physicalSchlafliBianchiMasterProp V B :=
  Geometry.DiscreteBianchi.discrete_bianchi_contracted_from_schlafli

/-- Session 554 projection: the physical D2 master-witness one-statement theorem
exposes the product-filter Regge/EH continuum master clause. -/
theorem physicalReggeEHD2_master_witness_one_statement_reggeEH
    {α ρ : Type*} {l : Filter α}
    (D : CanonicalPeriodicTetSixTetVolumeQuadratureProductFilterData (α := α) (ρ := ρ) l)
    (V B : Type) [Fintype B] :
    physicalReggeEHContinuumMasterProp D :=
  (physicalReggeEHD2_master_witness_one_statement D V B).2.1

What this page does not claim

This theorem does not prove convergence to the Einstein-Hilbert action on an arbitrary smooth manifold. This theorem does not derive the Einstein field equations from discrete principles. This theorem does not apply to all possible discretizations of spacetime.

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