reggeActionCubicRemainderInput_of_bound
plain-language theorem explainer
Packages a local cubic bound on the nonlinear Regge-action Taylor remainder into the named remainder-input structure used by discrete-gravity second-variation arguments. Anyone wiring flat triangulations into cubic-control hypotheses cites this. The body is a one-field structure constructor: it just records the supplied bound.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation that is flat. Given a local cubic bound on the canonical nonlinear Taylor remainder of the Regge action on $K$ (i.e., constants $r>0$ and $C\ge 0$ such that the remainder is $O(\|\xi\|^3)$ for all vertex potentials with $\|\xi\|<r$), obtain the named cubic-remainder input package for $(K,\text{flat})$.
background
This module fixes the nonlinear second-variation and cubic-remainder targets for the Regge action on a 3D triangulation in a form usable before the full Cayley-Menger/arccos chain-rule expansion is written out. Analytic facts therefore live in named input structures rather than as closed theorems.
The local cubic bound asserts existence of $r>0$ and $C\ge 0$ so that, for every vertex potential $\xi$ with $|\xi|<r$, the norm of the canonical Regge remainder (relative to the canonical Hessian) is at most $C|\xi|^3$. The cubic-remainder input is the thin structure whose single field is exactly that bound; the flat-configuration hypothesis is carried only as a parameter, marking the expansion point.
The constructor sits next to the second-variation input package and the canonical-Hessian identification lemmas in the same file, all of which prepare directional second derivatives of the action along lines of vertex potentials.
proof idea
One-line structure constructor. The four arguments (triangulation, incidence consistency, flatness, and the local cubic bound) are accepted as parameters; the returned package is built by setting its sole field cubic_bound equal to the supplied bound. No algebraic rewriting or lemma application occurs.
why it matters
This is the standard entry point that turns a raw cubic estimate into the named input expected by the cubic Taylor layer. Downstream, the Taylor-theorem packaging constructor applies it directly: once a nonlinear cubic Taylor theorem is assumed for $K$, that theorem is re-read as a local cubic bound and fed through this constructor to produce a cubic-remainder input.
In the Recognition geometry stack the object supports controlled expansion of the discrete gravitational action about flat configurations, the setting in which second-variation positivity and higher-order remainder estimates must eventually connect to continuum curvature. Until the large Cayley-Menger expansion is fully materialized, this named input is the exact socket where Mathlib multivariate Taylor or an IsBigO fallback is meant to plug in.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.