exactSecondOrderCubicLatticeLimitInput
plain-language theorem explainer
Packages an incidence-consistent 3D triangulation and spacing a>0 into a cubic-lattice limit input whose continuum comparison is exactly the second-order Regge action, so the error constant vanishes. Cited as a constructibility sanity check for the limit-input structure, not as the physical six-tet continuum model. The limit estimate is discharged by simplifying the exact comparison model.
Claim. Given an incidence-consistent finite 3D Regge triangulation $K$ and a lattice spacing $a>0$, there is a cubic-lattice limit input for $K$ whose regular cubic model is the exact second-order comparison model at spacing $a$ (continuum action identical to the canonical second-order Regge action, error constant zero).
background
This module isolates the regular weak-field cubic-lattice case of the second-order Regge action. The general CMS theorem only yields weak curvature-measure convergence; a plain $O(a^2)$ action estimate is special to the cubic lattice and is packaged here.
A Triangulation3D is a finite 3D Regge complex with abstract incidence and nondegenerate squared-edge data on each tetrahedron. IncidenceConsistent strengthens that data: local tet edge slots match global endpoints (up to orientation) and supplies the local closed-form Schläfli identity needed for a global Schläfli identity without caller-supplied Schläfli data.
ReggeCubicLatticeLimitInput pairs a RegularCubicLatticeModel with a ReggeSecondOrderCubicLatticeLimit estimate. The upstream exact comparison model sets the continuum action equal to the canonical second-order Regge action itself, forcing the error constant to zero; it is explicitly a sanity-check instance, not the physical six-tet Dirichlet continuum model.
proof idea
Definitional construction of the limit-input structure. The model field is the exact second-order comparison model at the given spacing $a$. The limit_estimate field is a short tactic proof: introduce the test function $\xi$, then simp with the exact comparison model, which collapses the error to zero by construction.
why it matters
Shows that RegularCubicLatticeModel and ReggeCubicLatticeLimitInput are inhabited without extra caller data, so the cubic-lattice $O(a^2)$ packaging is not vacuous. The module's physical target remains the six-tet cubic Dirichlet model: identify the canonical second-order Regge action with the finite-difference Dirichlet action, then supply a genuine $O(a^2)$ estimate. This exact-comparison input does not perform that identification; it only certifies structural constructibility on the path from discrete Regge data toward continuum gravity limits in the Recognition scaffold. No downstream consumers are wired yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.