Gravity Regge Cubic Lattice Limit Physical Six Tet Cubic Dirichlet Model

The physical model

In numerical relativity, the Regge action is a way to write gravity on a lattice, a grid of points and edges, instead of on a smooth continuous manifold. The second-order Regge action is a particular version of this lattice action, and the question is whether it approaches the correct continuum limit as the lattice spacing shrinks. The declaration PhysicalSixTetCubicDirichletModel is a formal structure in the framework's machine-checked library of formal theorems that packages a specific answer to this question for a particular kind of lattice: a cubic lattice where each cube is divided into six tetrahedra.

The structure bundles together the data needed to state the claim. It includes a regular cubic lattice model, which specifies the lattice spacing and a continuum action to compare against. It also includes two propositions: that the six-tetrahedra-per-cube decomposition is in place, and that the canonical Hessian of the Regge action is equal to the finite-difference Dirichlet action. Finally, it carries the key estimate: the difference between the lattice action and the continuum action is bounded by a constant times the lattice spacing squared. This is the O(a^2) error estimate, the precise statement that the lattice action converges to the continuum action as the spacing goes to zero.

The declaration does not prove that this estimate holds. It defines what would have to be true for the physical model to be established. The structure is a target, a specification of a theorem to be proved, not the theorem itself. The library does contain a theorem that the error vanishes along a family of models when the error envelope tends to zero, but that theorem requires the O(a^2) estimate as an input. The physical six-tet model is the class of inputs that would supply that estimate, and the proof that the six-tet action is the finite-difference Dirichlet action remains a stated goal, not a finished result.

What the declaration does establish is a clean interface. It shows exactly what data and what proof obligations are needed to connect the lattice gravity action to a continuum description. It also provides a sanity-check instance where the continuum action is chosen to be the lattice action itself, giving a trivial zero error. This confirms the structure is constructible, but the docstring is explicit that this is not the physical model. The physical instance still has to identify the action with the finite-difference Dirichlet action, a step the framework has not yet completed.

/-- Physical six-tet cubic Dirichlet model data.  This is the target class
for the real cubic-lattice instance: prove that the canonical second-order
Regge action on the six-tetrahedra-per-cube triangulation is the finite-
difference Dirichlet action, then supply the O(a^2) estimate. -/
structure PhysicalSixTetCubicDirichletModel
    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  regularModel : RegularCubicLatticeModel K hK
  sixTetCubicDecomposition : Prop
  canonicalHessian_is_dirichlet : Prop
  finiteDifferenceEstimate :
    ReggeSecondOrderCubicLatticeLimit K hK regularModel

/-- Physical six-tet cubic Dirichlet model data.  This is the target class
for the real cubic-lattice instance: prove that the canonical second-order
Regge action on the six-tetrahedra-per-cube triangulation is the finite-
difference Dirichlet action, then supply the O(a^2) estimate. -/
structure PhysicalSixTetCubicDirichletModel
    (K : Triangulation3D) (hK : IncidenceConsistent K) where
  regularModel : RegularCubicLatticeModel K hK
  sixTetCubicDecomposition : Prop
  canonicalHessian_is_dirichlet : Prop
  finiteDifferenceEstimate :
    ReggeSecondOrderCubicLatticeLimit K hK regularModel

/-- 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 the six-tet Regge action equals the finite-difference Dirichlet action. The declaration does not prove that the O(a^2) error estimate holds for any specific physical lattice. The declaration does not establish a continuum limit for any lattice other than the regular cubic one.

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: