Gravity Nonlinear Convergence Rsregge Convergence

The convergence bridge

Regge calculus is a way to do general relativity on a discrete mesh. Instead of a smooth spacetime, you build the geometry from flat pieces, such as tetrahedra in four dimensions, joined along their faces. Curvature appears where these pieces meet: the deficit angle around a hinge measures how much local geometry is missing from flatness. The Regge action, a sum over hinges of deficit angle times hinge area, approximates the Einstein-Hilbert action of smooth gravity. The question of when and how fast this approximation improves as the mesh gets finer is the convergence problem of Regge calculus.

The classical literature supplies the main answers. Cheeger, Müller, and Schrader proved in 1984 a measure-convergence result: for a fine triangulation with mesh size η, the difference between the smooth and the piecewise-flat curvature measures is bounded by a term proportional to the square root of η plus a term involving the volume of a thin tube around the boundary. That is a general statement, and it is not a quadratic error bound. Stronger second-order convergence, with error proportional to the square of the mesh size, appears in special numerical settings, such as the Kasner-type tests of Gentle and Miller in 1998 and the reconciliation work of Brewin and Gentle in 2001. Christiansen added a spectral analysis of the linearized theory in 2011.

In Recognition Science, the declaration RSReggeConvergence records these inputs as axioms. The framework treats the convergence of Regge calculus to general relativity as an established mathematical fact from the literature, and it packages that fact so that its own discrete ledger, a record of recognition events, can build on it. The structure bundles four assumptions: the general Cheeger-Müller-Schrader measure bound, the stronger quadratic action convergence for special cases, a corresponding quadratic convergence of the Regge Ricci scalar, and a derived value for the gravitational coupling constant, κ = 8·φ⁵, where φ is the golden ratio. The declaration also states that this coupling is positive.

What the declaration does not claim is as important as what it records. It does not prove the convergence results from scratch. The machine-checked library of formal statements, the framework's library, axiomatizes them, with a clear label, rather than reproving forty years of Regge calculus. The stronger quadratic hypotheses are not the general Cheeger-Müller-Schrader result; they are special-purpose inputs for modules that need second-order control. The library also records what a full proof would require: simplicial geometry with Cayley-Menger determinants, the Schläfli identity, comparison geometry between smooth and piecewise-flat metrics, curvature error analysis, and compactness arguments. That is a multi-year project, and the framework does not pretend to have completed it.

The consequence is a conditional bridge. If the convergence axioms hold, then the framework's discrete ledger produces the full nonlinear Einstein field equations, not just a linearized approximation. The bridge is real, but it rests on axioms that the framework states plainly and does not hide. A reader who wants the convergence proved, not assumed, knows exactly what remains to be done.

/-- **CMS Theorem 5.1 shape, scalar real abstraction.**

For a smooth Riemannian manifold `M`, a sufficiently fine `Θ`-fat
triangulation with mesh `η`, and a submanifold `U` with smooth boundary, CMS
prove a curvature-measure estimate of the form

`|R_i(U) - R_{i,η}(U)| ≤ c · (Vol(U) · sqrt η + Vol(B_{sqrt η}(∂U)))`.

The real variables here are the scalar placeholders for those geometric
quantities:

* `RiU`: smooth Lipschitz-Killing curvature measure on `U`;
* `RiEtaU`: piecewise-flat / Regge curvature measure on `U`;
* `VolU`: volume of `U`;
* `boundaryTubeVol`: volume of the `sqrt η`-tubular neighborhood of `∂U`;
* `η`: mesh size;
* `c`: the CMS constant depending on curvature bounds and fatness.

This is deliberately **not** an `O(η^2)` statement. -/
def cms_theorem_5_1_measure_bound : Prop :=
  ∀ (RiU RiEtaU VolU boundaryTubeVol η c : ℝ),
    0 ≤ VolU → 0 ≤ boundaryTubeVol → 0 < η → η < 1 → 0 < c →
      |RiU - RiEtaU| ≤ c * (VolU * Real.sqrt η + boundaryTubeVol)

/-- In the RS framework, the Regge action convergence gives:
    S_Regge(J-cost lattice, a) -> (1/2*kappa_RS) * integral R sqrt(g)

    Combined with:
    - J-cost minimization implies delta S_Regge = 0 (variational dynamics)
    - delta S_EH = 0 implies EFE (Hilbert variation)
    - kappa_RS = 8*phi^5 (derived coupling)

    This gives the FULL (nonlinear) Einstein field equations
    from the RS discrete ledger, conditional on the convergence axiom. -/
structure RSReggeConvergence where
  /-- General CMS Theorem 5.1-style curvature-measure convergence. -/
  cms_measure_convergence : cms_theorem_5_1_measure_bound
  /-- Stronger special-purpose action convergence, if a module needs `O(a^2)`. -/
  action_convergence : regge_to_eh_convergence_axiom
  ricci_convergence : regge_ricci_convergence_axiom
  kappa_derived : rs_kappa = 8 * phi ^ 5
  kappa_positive : 0 < rs_kappa

/-- **Special stronger hypothesis (not CMS Theorem 5.1 in general).**

Some weak-field cubic-lattice or numerical Regge settings can carry
second-order truncation/convergence estimates.  That is a separate input from
the general CMS curvature-measure theorem above.

This is the old `regge_to_eh_convergence_axiom` statement, retained under a
more honest name. -/
def special_quadratic_regge_to_eh_convergence_hypothesis : Prop :=
  ∀ (S_EH : ℝ) (a : ℝ), 0 < a → a < 1 →
    ∃ (S_Regge : ℝ) (C : ℝ), 0 < C ∧
      |S_Regge - S_EH| ≤ C * a ^ 2

/-- To PROVE the convergence axioms from scratch in Lean, one would need:

    1. Simplicial geometry: volumes, angles, areas as functions of edge lengths
       (Cayley-Menger determinants, generalized to all dimensions)
    2. The Schläfli identity: sum A_h * d(delta_h)/dL_e = 0
       (a purely geometric identity; provable but technical)
    3. Comparison geometry: relating simplicial metrics to smooth metrics
       (this requires Riemannian geometry in Mathlib, which is incomplete)
    4. Error analysis: bounding the difference between Regge curvature
       measures and smooth curvature measures in terms of mesh quality.
       CMS gives the `η^(1/2)` + boundary-tube form above; `O(a^2)` needs
       extra special structure.
    5. Compactness and convergence: extracting a convergent subsequence
       and identifying the limit (standard but requires functional analysis)

    This is a multi-year project for the Mathlib community.
    We axiomatize instead, clearly labeling the axioms. -/
def proof_requirements : List String :=
  [ "Simplicial geometry (Cayley-Menger)"
  , "Schläfli identity"
  , "Comparison geometry (smooth vs piecewise-flat)"
  , "Curvature error analysis"
  , "Compactness and convergence extraction" ]

What this page does not claim

The convergence axioms are not proved inside the framework's machine-checked library. The quadratic convergence hypothesis is not the general Cheeger-Müller-Schrader result. The declaration does not derive the Einstein field equations without assuming the convergence axioms.

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