Gravity Nonlinear Convergence Nonlinear Convergence Cert

The convergence certificate

Regge calculus is a way of doing general relativity on a discrete lattice of flat pieces, like approximating a curved surface with many small triangles. The central question is whether, as the lattice gets finer, the discrete version truly approaches the smooth Einstein-Hilbert action of general relativity. The ledger, a discrete record of events, provides the lattice on which this approximation is built.

The certificate nonlinear_convergence_cert is a formal, machine-checked collection of theorems that records the convergence inputs. It does not prove the convergence itself; that is established in the classical literature, for example by Cheeger, Müller, and Schrader (1984), who proved a curvature-measure convergence theorem, and by Gentle and Miller (1998) and Brewin and Gentle (2001), who demonstrated second-order convergence in specific numerical settings. The certificate packages these known results so the Recognition Science framework can build on them.

The certificate carefully separates two distinct claims. The general Cheeger-Müller-Schrader theorem gives a measure-convergence bound of the form |R_i(U) - R_{i,η}(U)| ≤ c · (Vol(U) · √η + Vol(B_{√η}(∂U))), where η is the mesh size. This is a broad statement with a √η bulk term plus a boundary-tube term. The certificate also records a stronger, special-purpose hypothesis, the O(a²) action convergence, which is used only in specific weak-field or numerical lattice settings where that stronger rate is justified. The certificate explicitly marks this second hypothesis as not being the general CMS theorem.

In Recognition Science, the certificate connects the discrete Regge action to the Einstein-Hilbert action. The framework models the convergence as a structure RSReggeConvergence that bundles the CMS measure convergence, the stronger quadratic action convergence, and the derived coupling constant κ_RS = 8·φ⁵. From this, the framework derives the full nonlinear Einstein field equations, conditional on the convergence axioms holding.

The certificate does not claim to have proved Regge convergence from scratch. The proof would require a multi-year project formalizing simplicial geometry, the Schläfli identity, comparison geometry, and error analysis in a machine-checked library. Instead, the certificate axiomatizes the known results, clearly labeling them as axioms that can be replaced by full proofs when the underlying mathematics is formalized. The certificate also does not claim the stronger O(a²) convergence holds in general; it is a special-purpose hypothesis, not the general CMS theorem.

theorem nonlinear_convergence_cert : NonlinearConvergenceCert where
  cms_bound := fun h => h
  cms_bulk_vanishes := cms_sqrt_bulk_vanishes
  cms_full_bound_vanishes := cms_bound_vanishes
  second_order := fun _ _ _ => convergence_is_second_order _ (by linarith) (by linarith)
  error_goes_to_zero := error_vanishes
  kappa := rs_kappa_value

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

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

/-- 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 certificate does not prove Regge convergence from scratch; it records known results as axioms. The certificate does not claim the O(a²) action convergence holds generally; it is a special-purpose hypothesis. The certificate does not derive the Einstein field equations unconditionally; it is conditional on the convergence axioms holding.

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: