Gravity Regge Cubic Lattice Limit Exact Second Order Cubic Lattice Limit Input

A sanity check on the lattice

In numerical relativity, the Regge action is a way of writing gravity on a discrete mesh of tetrahedra, the higher-dimensional analogue of triangulating a surface. The second-order version is a particular refinement of that action, and a natural question is whether it converges to the smooth continuum theory as the mesh spacing shrinks. The framework's library of formal theorems treats this question by defining a comparison model: a lattice spacing, a continuum action, and a certified error bound that shrinks as the spacing to the second power.

The declaration exactSecondOrderCubicLatticeLimitInput constructs one such comparison model in the most trivial way possible. It sets the continuum action to be exactly the same second-order Regge action defined on the lattice, and sets the error constant to zero. The proof is then immediate: the difference between the action and itself is zero, which is certainly bounded by zero times the spacing squared. This is a sanity check that the framework's definitions are internally consistent and that the input structure can be constructed without any extra assumptions.

This is not the physical continuum limit. The physical target, called the six-tet cubic Dirichlet model, would identify the canonical second-order Regge action on a specific six-tetrahedra-per-cube triangulation with the finite-difference Dirichlet action, and then supply a genuine O(a^2) error estimate. That identification remains an open problem, stated as a target in the library. The exact comparison model deliberately bypasses it by choosing the continuum action to be the lattice action itself, which makes the error vanish identically.

What the declaration does establish is that the formal scaffolding works: the structures for lattice spacing, continuum action, and error bound can be instantiated, and the limit theorem can be applied to this trivial model. It also proves a separate convergence statement: if a family of such comparison models has error envelopes that tend to zero, then the actions converge pointwise to the continuum action. That is a real theorem about the framework's definitions, but it does not by itself show that any physical lattice action converges to general relativity.

/-- Exact comparison model: the continuum action is chosen to be the
canonical second-order Regge action itself, so the error constant is zero.

This is not the physical regular cubic-lattice continuum model.  It is a
sanity-check instance showing that `RegularCubicLatticeModel` and
`ReggeCubicLatticeLimitInput` are constructible without further caller data.
The real cubic-lattice instance still has to identify this action with the
finite-difference Dirichlet action. -/
def exactSecondOrderComparisonModel
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (a : ℝ) (ha : 0 < a) :
    RegularCubicLatticeModel K hK where
  latticeSpacing := a
  spacing_pos := ha
  continuumAction := reggeActionSecondOrder K hK (canonicalReggeHessian K hK)
  errorConstant := 0
  errorConstant_nonneg := le_rfl
  secondOrder_action_error := by
    intro ξ
    simp

def exactSecondOrderCubicLatticeLimitInput
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (a : ℝ) (ha : 0 < a) :
    ReggeCubicLatticeLimitInput K hK where
  model := exactSecondOrderComparisonModel K hK a ha
  limit_estimate := by
    intro ξ
    simp [exactSecondOrderComparisonModel]

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

This declaration does not prove that the second-order Regge action on any physical lattice converges to the Einstein-Hilbert action. It does not establish the finite-difference Dirichlet identification for the six-tet cubic model. It does not provide any non-trivial error estimate for a physical lattice spacing.

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: