Gravity Cubic Regge Proof

A direct proof for cubic lattices

Regge calculus is a standard way to approximate general relativity by breaking spacetime into flat pieces, such as triangles in two dimensions or tetrahedra in three. The idea, introduced by Tullio Regge in 1961, is that curvature can be concentrated along the joints where these pieces meet. In the Recognition Science framework, this classical method takes a specific form: the spacetime is not a general triangulation but a regular cubic lattice, and the cost of each interaction is fixed by the framework's forced cost function J(x) = (x + 1/x)/2 - 1.

The module CubicReggeProof establishes that this discrete version of gravity converges to the smooth equations of general relativity as the lattice spacing shrinks to zero. The proof is direct and machine-checked, replacing a previously assumed axiom with a theorem. The argument proceeds in three tiers: first, the total action of the J-cost model approaches the quadratic action; second, the Euler-Lagrange equation of the model linearizes to the lattice Laplacian; third, the lattice Laplacian converges to the continuum Laplacian at second order in the lattice spacing.

The key technical insight is that the J-cost function, when written in logarithmic coordinates, has the Taylor expansion cosh(ε) - 1 = ε²/2 + ε⁴/24 + ε⁶/720 + ... The quadratic term gives the standard lattice action, and the higher-order terms vanish as the spacing goes to zero. The Euler-Lagrange equation involves the hyperbolic sine function, whose derivative at zero is exactly 1, which is why the linearization works cleanly. The proof shows the relative error between the discrete and continuum actions tends to zero as the lattice spacing a goes to zero, at a rate proportional to a².

In Recognition Science, this result has a specific consequence. The framework's constants are not free parameters: the gravitational coupling kappa is derived to equal 8φ⁵, where φ is the golden ratio. The proof also shows that a flat lattice satisfies the Euler-Lagrange equation, and that the flat deficit angle in a cubic lattice is zero. The certificate structure CubicReggeConvergenceCert packages the entire chain of results into a single object that can be checked by the machine.

What this establishes in plain language is that the discrete model of gravity built from the forced cost function is not an arbitrary toy model. It is a consistent discretization that recovers the smooth theory in the continuum limit. This is the kind of result that gives confidence that the framework's discrete starting point can produce the known physics of general relativity, at least in the linearized regime. The proof does not cover the full nonlinear Einstein equations, but it establishes the bridge from the discrete to the continuum.

/-- Every step is proved. Zero axioms, zero sorry. -/
theorem proved_convergence_chain : ProvedConvergenceChain where
  step1_quadratic := J_log_quadratic_approx
  step2_neighbor_approx := fun _D f x h => jcost_gives_laplacian_structure f x h
  step3_el_is_laplacian := fun _D f x => linearized_el_eq_neg_laplacian f x
  step4_flat_solution := fun _D c x => flat_satisfies_el c x
  step5_linearization := sinh_deriv_at_zero
  step6_continuum := fun a ha f hf x => by
    obtain ⟨C, _hC_nn, hC⟩ := continuum_limit_second_order f x a ha hf
    exact ⟨C, hC⟩
  step7_coupling := ZeroParameterGravity.kappa_rs_closed_form
  step8_flat_lattice := cubic_flat_deficit

/-- The linearized EL equation equals minus the lattice Laplacian. -/
theorem linearized_el_eq_neg_laplacian {D : ℕ}
    (f : LatticeField D) (x : Fin D → ℤ) :
    (∑ k : Fin D,
      ((f x - f (shift_minus k x)) -
       (f (shift_plus k x) - f x))) =
    -lattice_laplacian f x := by
  linarith [linearized_el_plus_laplacian_zero f x]

/-- In the gravitational sector, the lattice field f encodes the
    metric perturbation h_μν (in harmonic/Lorenz gauge).

    The EL equation lattice_laplacian(h) = 0 in the continuum limit
    gives ∇²h = 0, which IS the linearized vacuum EFE in harmonic gauge.

    The sourced case: ∇²h = −2κT with κ = 8φ⁵ (derived). -/
theorem kappa_derived : ZeroParameterGravity.kappa_rs = 8 * phi ^ 5 :=
  ZeroParameterGravity.kappa_rs_closed_form

/-- The flat (constant) field satisfies the EL equation exactly.
    sinh(0) = 0, so every term vanishes. -/
theorem flat_satisfies_el {D : ℕ} (c : ℝ) (x : Fin D → ℤ) :
    euler_lagrange (fun _ => c) x = 0 := by
  unfold euler_lagrange; simp [Real.sinh_zero]

What this page does not claim

The proof does not cover the full nonlinear Einstein equations. The module does not prove that the cubic lattice is the only discretization that converges. The convergence result does not establish that the Recognition Science framework is the correct theory of quantum gravity.

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