Gravity Cubic Regge Proof Cubic Shape Bound Positive

A positive shape bound

In the study of gravity as a discrete lattice, the shape of the lattice matters. A cubic lattice is the simplest regular arrangement of points, like the grid of a city but extended into three dimensions. The declaration cubic_shape_bound_positive establishes that a certain parameter measuring this shape, called the cubic shape bound, is strictly greater than zero. This is a technical but necessary condition: it guarantees that the lattice's geometry is well-behaved and does not collapse or become degenerate when the discrete model is compared to the continuous theory of gravity.

The result is part of a larger proof that a discrete model of gravity, based on a cost function J, converges to the standard continuum equations of general relativity. The framework models spacetime as a lattice of points where each bond carries a cost, and the Euler-Lagrange equation of this cost function linearizes to the familiar lattice Laplacian. The positivity of the shape bound ensures that the lattice's geometric structure remains stable throughout this convergence, preventing any singular behavior that would invalidate the comparison.

This positivity is not a physical prediction about the universe. It is a mathematical property of the cubic lattice model itself. The theorem is proved in the framework's machine-checked library of formal theorems, meaning the logical derivation is verified by a computer. It does not claim that the cubic shape bound has any particular numerical value, only that it is positive. It also does not claim that the cubic lattice is the only possible discretization of gravity, nor that the convergence proof applies to arbitrary simplicial complexes, which require a more general and deeper theorem.

/-- The cubic lattice has shape bound σ = 1 (all cells identical). -/
theorem cubic_shape_bound_positive : 0 < ReggeConvergence.cubic_shape_bound :=
  ReggeConvergence.cubic_shape_optimal

/-- **THE CERTIFICATE**: all proved. Zero axioms. Zero sorry. -/
theorem cubic_regge_convergence_cert : CubicReggeConvergenceCert where
  action_quadratic := J_log_quadratic_approx
  action_symmetric := J_log_symmetric
  action_vacuum := J_log_zero
  el_is_laplacian := fun D f x => linearized_el_eq_neg_laplacian f x
  flat_solution := fun D c x => flat_satisfies_el c x
  linearization_coeff := sinh_deriv_at_zero
  laplacian_converges := fun a ha f hf x => by
    obtain ⟨C, _hC_nn, hC⟩ := continuum_limit_second_order f x a ha hf
    exact ⟨C, hC⟩
  kappa_derived := ZeroParameterGravity.kappa_rs_closed_form
  kappa_positive := ZeroParameterGravity.kappa_pos
  flat_deficit := cubic_flat_deficit
  shape_optimal := cubic_shape_bound_positive
  second_order := fun _ _ _ => by ring
  error_vanishes := NonlinearConvergence.error_vanishes
  quartic_fixed := quartic_coeff
  sextic_fixed := sextic_coeff
  relative_rate := fun M a ha ha1 hM =>
    relative_convergence_rate M a ha ha1 hM

What this page does not claim

The cubic shape bound has any specific numerical value beyond being positive. The convergence proof applies to arbitrary simplicial complexes, which require the general Cheeger-Müller-Schrader theorem. The cubic lattice is the only possible discretization of spacetime within the framework.

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: