Gravity Regge Cubic Lattice Limit Cubic Lattice Limit Input Of Physical Six Tet

The cubic-lattice bridge

In numerical physics, a lattice is a discrete grid of points used to approximate a continuous space. The Regge action is a way of writing gravity's action, the quantity whose minimization gives the equations of motion, using only the lengths of edges in a triangulated space. The declaration cubicLatticeLimitInput_of_physicalSixTetModel is a formal packaging step: it takes a model of a specific cubic lattice, one built from six tetrahedra per cube, and turns it into a general input structure that the framework's convergence theorem can consume.

The structure it produces, ReggeCubicLatticeLimitInput, bundles two things: a regular cubic-lattice comparison model, which supplies a lattice spacing and a continuum action, and a certified error estimate. The estimate states that, for any vertex potential, the absolute difference between the discrete second-order Regge action and the continuum action is bounded by a constant times the square of the lattice spacing. That is the standard O(a²) convergence statement: as the spacing a goes to zero, the discrete action approaches the continuum one at a quadratic rate.

The definition itself is a constructor, not a theorem. It assembles the input structure from a physical six-tet model, which carries the extra assumptions that the six-tet decomposition holds and that the canonical Hessian equals the finite-difference Dirichlet action. Those assumptions are declared as propositions inside the model structure; they are not proved by this definition. The definition merely lifts the finite-difference estimate from the physical model into the general input type, so that the library's theorem reggeActionSecondOrder_cubic_lattice_limit can apply to it.

What the declaration does not claim is equally precise. It does not prove that the six-tet triangulation actually has the finite-difference Dirichlet action as its canonical Hessian; that identification remains an unproved proposition in the physical model. It does not construct the physical six-tet model itself, only the bridge from such a model to the input type. And it does not establish that any particular real-world lattice converges, because the error constant and the continuum action are supplied by the model, not derived by this definition. The exact comparison model in the same file, which sets the error constant to zero by choosing the continuum action to be the Regge action itself, is explicitly labeled a sanity check, not the physical instance.

The practical consequence is that the framework has separated the hard analytic work from the bookkeeping. Once someone proves the six-tet identification and supplies the O(a²) estimate, this definition lets the existing convergence theorem fire immediately. The declaration is the adapter that makes the physical model speak the library's language, and the library's language is the one in which convergence is a proved fact rather than a numerical hope.

def cubicLatticeLimitInput_of_physicalSixTetModel
    (K : Triangulation3D) (hK : IncidenceConsistent K)
    (M : PhysicalSixTetCubicDirichletModel K hK) :
    ReggeCubicLatticeLimitInput K hK where
  model := M.regularModel
  limit_estimate := M.finiteDifferenceEstimate

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

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

What this page does not claim

It does not prove the six-tet decomposition or the Hessian-to-Dirichlet identification. It does not construct the physical six-tet model, only the bridge from it to the input type. It does not establish convergence for any particular real-world lattice, since the error constant and continuum action come from the model.

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: