Gravity Regge Cubic Lattice Limit Regge Cubic Lattice Limit Input

The lattice limit input

In numerical approaches to gravity, space is often approximated by a lattice of tetrahedra, and the gravitational action is written as a sum over the lattice edges and hinges. The Regge action is the standard discrete version of the Einstein-Hilbert action. A key question is whether this discrete action approaches the continuum action as the lattice spacing shrinks to zero. The declaration ReggeCubicLatticeLimitInput packages the data needed to answer that question for a regular cubic lattice.

The declaration is a structure, a formal container that bundles two pieces of information. First, it holds a RegularCubicLatticeModel, which specifies the lattice spacing, the continuum action to compare against, and an error constant. Second, it holds a proof that the second-order Regge action on the lattice differs from the continuum action by at most that error constant times the square of the lattice spacing. In symbols, for any vertex potential ξ, the inequality |ReggeAction(ξ) − ContinuumAction(ξ)| ≤ C · a² holds, where a is the lattice spacing and C is the error constant. This is an O(a²) error estimate, meaning the discrete action converges to the continuum action as the lattice spacing goes to zero.

The declaration itself does not prove that any particular lattice model satisfies this bound. It is a named input, a formal interface that a concrete model must instantiate. The library provides a trivial sanity-check instance where the continuum action is chosen to be the discrete action itself, making the error zero. But the physically relevant instance, where the six-tetrahedra-per-cube triangulation is shown to reproduce the finite-difference Dirichlet action, remains a target. The declaration PhysicalSixTetCubicDirichletModel is the structure that would carry that proof, with fields asserting the six-tet decomposition, the identification of the canonical Hessian with the Dirichlet action, and the finite-difference estimate.

What the declaration does establish, once an input is supplied, is a theorem: given a ReggeCubicLatticeLimitInput, the second-order Regge action indeed satisfies the O(a²) continuum limit. The library also proves that if a family of such models has error envelopes tending to zero, then the discrete actions converge pointwise to the continuum action. This is the convergence statement that makes the lattice approximation meaningful. The declaration is the formal contract that connects a concrete lattice model to the convergence theorem.

/-- Named input connecting a concrete regular triangulation model to the
canonical second-order Regge action. -/
structure ReggeCubicLatticeLimitInput
    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  model : RegularCubicLatticeModel K hK
  limit_estimate : ReggeSecondOrderCubicLatticeLimit K hK model

/-- Phase-G cubic-lattice `O(a^2)` continuum-limit theorem for the canonical
second-order Regge action. -/
theorem reggeActionSecondOrder_cubic_lattice_limit
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (h_limit : ReggeCubicLatticeLimitInput K hK) :
    ReggeSecondOrderCubicLatticeLimit K hK h_limit.model :=
  h_limit.limit_estimate

/-- A family of cubic-lattice comparison models converges pointwise whenever
its certified `O(a^2)` error envelope tends to zero along the refinement
parameter. -/
theorem reggeSecondOrderCubicLatticeLimit_error_vanishes_along_models
    {α : Type*} {l : Filter α}
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (M : α → RegularCubicLatticeModel K hK)
    (hLimit : ∀ t : α, ReggeSecondOrderCubicLatticeLimit K hK (M t))
    (hEnvelope :
      Filter.Tendsto
        (fun t : α => (M t).errorConstant * (M t).latticeSpacing ^ (2 : ℕ))
        l (nhds 0))
    (ξ : VertexPotential K) :
    Filter.Tendsto
      (fun t : α =>
        |reggeActionSecondOrder K hK (canonicalReggeHessian K hK) ξ -
          (M t).continuumAction ξ|)
      l (nhds 0) := by
  apply squeeze_zero
  · intro t
    exact abs_nonneg _
  · intro t
    exact hLimit t ξ
  · exact hEnvelope

What this page does not claim

The declaration does not prove that any particular physical lattice model satisfies the O(a²) bound. The declaration does not identify the second-order Regge action with the finite-difference Dirichlet action on the six-tet triangulation. The declaration does not address convergence for non-regular or adaptive lattice refinements.

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