ReggeActionCubicRemainderInput
plain-language theorem explainer
Packages the local cubic bound on the canonical nonlinear Regge-action Taylor remainder as a named input at a flat configuration of a consistent 3D triangulation. Downstream Phase-E remainder theorems and Hessian-plus-Taylor assemblies cite this structure rather than the raw Prop. It is a one-field record: existence of radius and constant giving an O(||ξ||³) estimate on the remainder.
Claim. Fix a finite 3D Regge triangulation $K$ with incidence consistency and a flat analytic configuration. A cubic remainder input is a witness that the canonical nonlinear Taylor remainder $R(\xi)$ of the Regge action (relative to the canonical Hessian) obeys $\|R(\xi)\| \le C \|\xi\|^3$ for all vertex potentials $\xi$ with $\|\xi\| < r$, for some $r > 0$ and $C \ge 0$.
background
The module states nonlinear second-variation and cubic-remainder targets in usable form while the full Cayley-Menger/arccos chain-rule expansion is still being materialized. Analytic facts therefore live in named input structures rather than as closed theorems.
A Triangulation3D is a finite abstract 3D Regge complex with nondegenerate squared-edge data on each tetrahedron; incidence consistency supplies global squared edges, local-to-global edge matching, and the closed-form Schläfli data needed for global identities. A flat configuration adds the arccos endpoint conditions, zero-deficit flatness, and the smoothness fact required to invoke Taylor theory for the full nonlinear action.
The sole field is the local cubic remainder bound: existence of $r>0$ and $C\ge 0$ such that the norm of the canonical remainder is at most $C|\xi|^3$ inside the ball $|\xi|<r$ in the space of vertex potentials.
proof idea
No proof body: this is a structure definition. It records a single Prop-valued field equal to the local cubic remainder bound. Constructors elsewhere wrap a proved or assumed bound (or the identically-zero sanity case) into this named input; the Phase-E theorem simply projects the field back out.
why it matters
This is the exact interface where Mathlib multivariate Taylor (or an IsBigO fallback) is meant to connect to the Regge scaffold. The Phase-E cubic remainder theorem is conditional on this input and just returns its field. Downstream, Hessian-plus-Taylor packages include it as the cubic_remainder component once both the directional Hessian theorem and the cubic Taylor theorem are supplied; thin wrappers build the input from a Taylor theorem or from an explicit bound. In the Recognition geometry stack it keeps the nonlinear Regge second-variation story usable before the full arccos expansion is finished, without smuggling unfinished analysis into proved theorems.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.