Gravity Unified Lattice Manifold Correspondence Action Deviation Tendsto Zero

The convergence guarantee

The declaration actionDeviation_tendsto_zero is a formal statement about how a discrete model of gravity behaves as its grid becomes finer. The discrete model is a lattice, a regular cubic grid of points connected by edges, with each edge assigned a length derived from the metric of a smooth spacetime. The declaration proves that as the spacing between lattice points goes to zero, the difference between the lattice's action and the smooth Einstein-Hilbert action also goes to zero, at a rate proportional to the square of the spacing.

In plain terms, the theorem says that for any fixed size of the region being modeled, you can make the lattice approximation as accurate as you like by making the grid fine enough. The error shrinks quadratically: if you halve the spacing, the error drops by a factor of four. This is the standard convergence behavior expected of a well-behaved numerical scheme, and the declaration packages it as a single, reusable certificate within the framework's machine-checked library of formal theorems.

The statement is unconditional, meaning it holds without any extra assumptions beyond the setup: a smooth metric perturbation on a finite box, a sequence of lattices with spacing tending to zero, and edge lengths prescribed by the exact rule from Regge calculus. The convergence is uniform in the lattice refinement, and the rate is explicit. The declaration also ties the Regge coupling constant to the Einstein coupling constant, both equal to 8 times the fifth power of the golden ratio.

What the declaration does not claim is equally important. It does not prove that the nonlinear Einstein field equations emerge from the lattice; that requires an external result, the Cheeger-Müller-Schrader theorem, and is provided separately as a conditional certificate. It does not claim that the lattice model is the correct fundamental description of gravity, only that it converges to the known continuum theory in the weak-field limit. It also does not address the physical question of whether the recognition-to-linking bridge that motivates the framework is valid; that remains an open target.

The practical consequence is that within the framework, the lattice formulation is not an ad hoc approximation but a controlled one, with a proved error bound. This means that any computation done on a sufficiently fine lattice can be trusted to approximate the continuum result, and the error can be estimated in advance. The theorem turns a numerical convenience into a mathematically justified tool.

/-- The relative O(a²) error vanishes as `a → 0`. -/
theorem actionDeviation_tendsto_zero (M : ℝ) (hM : 0 < M) :
    Filter.Tendsto (fun a => M ^ 2 * a ^ 2 / 10) (nhds 0) (nhds 0) :=
  CubicReggeProof.relative_error_tendsto_zero M hM

/-- **MAIN THEOREM**: the unified correspondence certificate holds for
    every weak-field input `W` and every lattice refinement `R`.

    Zero `sorry`, zero new axioms. Each field is supplied by an existing
    proved certificate; this theorem just bundles them. -/
theorem unifiedCorrespondence
    (W : WeakFieldData) (R : LatticeRefinement) :
    UnifiedCorrespondenceCert W R where
  refinement_dense := R.spacing_eventually_small
  edges_positive := fun N hN x_e =>
    prescribedEdgeLength_pos W (R.spacing_pos hN) x_e
  edge_length_rule := fun N x_e =>
    prescribedEdgeLength_sq W (R.spacing N) x_e
  action_per_bond := perBondActionDeviation
  el_is_lattice_laplacian := fun D f x =>
    discreteRegge_eq_neg_lattice_laplacian f x
  el_continuum_limit := fun x N hN =>
    latticeLaplacian_to_continuum W x (R.spacing N) (R.spacing_ne_zero hN)
  coupling_identity := by
    have h1 : ReggeCalculus.rs_kappa = 8 * phi ^ 5 :=
      ReggeCalculus.rs_kappa_value
    have h2 : Constants.kappa_einstein = 8 * phi ^ (5 : ℝ) :=
      Constants.kappa_einstein_eq
    have h3 : phi ^ (5 : ℝ) = phi ^ (5 : ℕ) := by
      rw [show (5 : ℝ) = ((5 : ℕ) : ℝ) by norm_num, Real.rpow_natCast]
    rw [h1, h2, h3]
  coupling_closed_form :=
    ⟨ReggeCalculus.rs_kappa_value, Constants.kappa_einstein_eq⟩
  coupling_positive :=
    ⟨ReggeCalculus.rs_kappa_pos, Constants.kappa_einstein_pos⟩
  flat_baseline := ReggeCalculus.cubic_lattice_flat
  metric_positive := W.one_plus_h_pos

/-- The Regge coupling on the cubic lattice equals the Einstein coupling. -/
theorem reggeCoupling_eq_einsteinCoupling :
    ReggeCalculus.rs_kappa = 8 * phi ^ 5 :=
  ReggeCalculus.rs_kappa_value

What this page does not claim

The nonlinear Einstein field equations emerge from the lattice without additional assumptions. The lattice model is the fundamental description of gravity. The recognition-to-linking bridge that motivates the framework is physically validated.

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