LocalCubicRemainderBound
plain-language theorem explainer
On an incidence-consistent 3D triangulation, the nonlinear Regge action remainder about the canonical Hessian is locally O(‖ξ‖³) in the vertex-potential norm: some radius r>0 and constant C≥0 make the cubic bound hold for all ‖ξ‖<r. Analysts of discrete gravity and anyone wiring Mathlib Taylor or IsBigO estimates into the Regge stack cite this Prop. It is a pure definition of that existence statement, not a proved estimate.
Claim. For an incidence-consistent 3-dimensional triangulation $K$, the following holds: there exist $r>0$ and $C\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, the norm of the nonlinear Regge-action remainder (relative to the canonical graph-Laplacian Hessian) satisfies $\|R(K,\xi)\|\le C\|\xi\|^3$.
background
The module packages second-variation and cubic-remainder targets for the nonlinear Regge action in a form usable before the full Cayley–Menger/arccos chain-rule expansion is finished. Analytic obligations sit in named input structures rather than unfinished proofs.
The remainder here is the nonlinear Regge action minus its quadratic part built from the canonical Hessian. That Hessian is the graph Laplacian induced by incidence dual weights on the triangulation: diagonal entries sum dual weights, off-diagonal entries are minus the dual weight. Vertex potentials are real assignments to vertices; the bound is in their Euclidean (or equivalent finite-dimensional) norm.
Upstream, canonicalReggeHessian and reggeActionRemainder from the concrete Regge-action layer supply the objects being estimated. The module imports the first-variation development so the second-variation and remainder story sits on the same triangulation and incidence hypotheses.
proof idea
No proof: this is a definition of a proposition. The body is an existential statement over a positive radius $r$ and a nonnegative constant $C$, with a universal quantifier over vertex potentials inside the ball $|\xi|<r$, asserting the cubic majorization of the remainder norm. Downstream constructors and iff lemmas treat the Prop as the exact analytic obligation to discharge (e.g. via multivariate Taylor or an IsBigO fallback).
why it matters
This Prop is the single analytic hinge for the cubic Taylor story of nonlinear Regge action. NonlinearReggeCubicTaylorTheorem is definitionally identical to it; the iff lemma makes that audit explicit so no hidden analytic assumption sits in a constructor. ReggeActionCubicRemainderInput packages it as a named field, and reggeActionRemainder_cubic_bound simply projects that field (Phase-E remainder theorem conditional on the input).
nonlinearRegge_localCorrespondence_of_cubicBound unpacks the existential and builds the local J-cost correspondence from the same $r,C$ and inequality. In the broader Recognition geometry stack, controlling the cubic remainder is what lets discrete curvature/action expansions match continuum second-variation structure without spoiling the leading Hessian term. The open work is connecting Mathlib’s multivariate Taylor theorem (or an IsBigO surrogate) to close the named input.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.