exactSecondOrderComparisonModel
plain-language theorem explainer
Exact comparison model for the second-order Regge action on an incidence-consistent 3D triangulation: continuum action equals the canonical second-order Regge action, so the error constant is zero. Cited by anyone building a regular cubic-lattice comparison model or checking that the cubic-lattice limit input structures are inhabited. Direct structure instance; a one-line simp discharges the zero-error bound.
Claim. Given an incidence-consistent 3D Regge triangulation $K$ and lattice spacing $a > 0$, there is a regular cubic-lattice comparison model with spacing $a$, continuum action equal to the canonical second-order Regge action (quadratic truncation via the incidence dual-weight Hessian), and error constant identically 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.
A Triangulation3D is a finite 3D Regge complex with abstract incidence and nondegenerate squared-edge data. IncidenceConsistent strengthens that to global edge-endpoint agreement plus a local closed-form Schläfli identity. The continuum object here is reggeActionSecondOrder: the quadratic truncation of the Regge action built from a candidate Hessian. The Hessian used is canonicalReggeHessian, the graph Laplacian induced by incidence dual weights.
RegularCubicLatticeModel packages a positive lattice spacing, a continuum action on vertex potentials, a nonnegative error constant $C$, and the bound that the second-order Regge action differs from the continuum action by at most $C a^2$.
proof idea
Direct structure construction, not a derived theorem. Lattice spacing is set to the given $a$; positivity is the hypothesis $a > 0$. Continuum action is definitionally reggeActionSecondOrder at the canonical Hessian. Error constant is the literal $0$, with nonnegativity by le_rfl.
The second-order error field asks
$|\mathrm{reggeActionSecondOrder}(\xi) - \mathrm{continuumAction}(\xi)| \le 0 \cdot a^2$
for every vertex potential $\xi$. Both sides of the absolute value are the same term, so intro ξ; simp closes the goal.
why it matters
Feeds exactSecondOrderCubicLatticeLimitInput, which wraps this model into a full ReggeCubicLatticeLimitInput (model plus limit estimate). The doc-comment is explicit: this is a sanity-check instance showing that RegularCubicLatticeModel and the limit-input structure are constructible with no further caller data.
It is not the physical regular cubic-lattice continuum model. The real six-tet cubic Dirichlet instance must still identify the canonical second-order Regge action with the finite-difference Dirichlet action and supply a genuine $O(a^2)$ estimate. Within the gravity track this sits under the cubic-lattice specialization of second-order Regge convergence, separate from the general CMS weak-measure statement.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.