Gravity Nonlinear Convergence

The convergence bridge

Gravity nonlinear convergence is the question of when a lumpy, discrete approximation to spacetime becomes indistinguishable from the smooth geometry described by Einstein's equations. The standard tool for this is Regge calculus, invented by Tullio Regge in 1961, which replaces a smooth manifold with a patchwork of flat triangular pieces, like a geodesic dome made of rigid panels. Curvature then lives only along the hinges where panels meet, measured by the deficit angle: how much the panels fail to close up flat around a hinge. The central hope is that as the panels shrink, the discrete picture converges to the smooth one, and the Einstein-Hilbert action, the integral of curvature that governs general relativity, emerges from the sum of deficit angles.

That hope is not a new claim. The literature contains real theorems. Cheeger, Müller, and Schrader (1984) proved a curvature-measure convergence result for piecewise-flat spaces, with a bound of the form |R_i(U) - R_{i,η}(U)| ≤ c · (Vol(U) · √η + Vol(B_{√η}(∂U))). Here η is the mesh size, the first term controls the bulk error, and the second controls error near the boundary. Gentle and Miller (1998) demonstrated explicit second-order convergence in special numerical settings, and Brewin and Gentle (2001) reconciled convergence behavior across numerical Regge schemes. Christiansen (2011) added spectral analysis of the linearized problem. These are the pillars the framework stands on.

In Recognition Science, this convergence is packaged as a set of clearly labeled axioms, not as a new proof. The machine-checked library of formal theorems records the general CMS-style measure bound as an input, and separately records a stronger special-purpose hypothesis: that in some weak-field or numerical cubic-lattice settings, the error between the Regge action and the Einstein-Hilbert action is O(a^2), where a is the lattice spacing. The library proves that this quadratic error vanishes as a goes to zero, and that the CMS bulk term √η also vanishes. What it does not do is prove the O(a^2) bound from first principles; that requires a multi-year program in simplicial geometry, the Schläfli identity, and comparison geometry, which the library lists as open requirements.

The payoff, conditional on those axioms, is the full nonlinear Einstein field equations. The framework's chain runs: the J-cost lattice minimizes its Regge action, the Regge action converges to the Einstein-Hilbert action, and varying that action gives the field equations, with the derived coupling κ_RS = 8·φ^5. The library's structure RSReggeConvergence bundles the convergence inputs and the derived coupling into a single certificate. The honest verdict is that this is a bridge built on named, published theorems and clearly marked assumptions, not a proof that the discrete ledger must produce general relativity. The bridge stands, but its pylons are axioms awaiting full formalization.

/-- **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)

/-- Second-order convergence implies the special quadratic error vanishes as
`a -> 0`. -/
theorem quadratic_error_vanishes (C : ℝ) (_hC : 0 < C) :
    Filter.Tendsto (fun a => C * a ^ 2) (nhds 0) (nhds 0) := by
  have h : Continuous (fun a : ℝ => C * a ^ 2) := by continuity
  have := h.tendsto (0 : ℝ)
  simp at this
  exact this

/-- The CMS bulk term `sqrt η` vanishes as `η -> 0`. -/
theorem cms_sqrt_bulk_vanishes (C VolU : ℝ) :
    Filter.Tendsto (fun η : ℝ => C * (VolU * Real.sqrt η)) (nhds 0) (nhds 0) := by
  have hsqrt : Filter.Tendsto (fun η : ℝ => Real.sqrt η) (nhds 0) (nhds 0) := by
    simpa using (Real.continuous_sqrt.tendsto 0)
  have hVol : Filter.Tendsto (fun η : ℝ => VolU * Real.sqrt η) (nhds 0) (nhds 0) := by
    have hconst : Filter.Tendsto (fun _ : ℝ => VolU) (nhds 0) (nhds VolU) :=
      tendsto_const_nhds
    simpa using hconst.mul hsqrt
  have hC : Filter.Tendsto (fun _ : ℝ => C) (nhds 0) (nhds C) := tendsto_const_nhds
  simpa using hC.mul hVol

/-- 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

What this page does not claim

The O(a^2) action convergence is proved as a general theorem; it is a special-purpose hypothesis. The convergence of Regge calculus to general relativity is a new result of Recognition Science. The Einstein field equations are derived unconditionally from the discrete ledger without 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: