reggeActionRemainder_cubic_bound
plain-language theorem explainer
On a finite 3D Regge triangulation that is incidence-consistent and flat, the nonlinear action remainder is locally O(‖ξ‖³) in the vertex potential, once a named Taylor-input package is supplied. Gravity and discrete-geometry workers cite it as the Phase-E cubic control. The proof is a one-field projection from that input structure.
Claim. Let $K$ be a finite 3D Regge triangulation with consistent incidence data, and suppose a flat analytic configuration is given. If the named cubic Taylor-remainder input holds at that flat base point, then there exist $r>0$ and $C\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, the canonical nonlinear Regge-action remainder satisfies $\|R(\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 facts that would normally come from multivariate Taylor theory are therefore stored in named input structures.
A Triangulation3D is a finite abstract 3-complex with nondegenerate squared-edge data on each tetrahedron; incidence consistency is a separate hypothesis. A flat configuration supplies the arccos-endpoint freeness, zero-deficit flatness, and the smoothness fact needed to invoke Taylor theory at the base point.
The local cubic bound asserts existence of a radius $r>0$ and constant $C\ge 0$ so that the canonical remainder (action minus value and Hessian quadratic form) is $O(|\xi|^3)$ for small vertex potentials $\xi$. The cubic-remainder input is exactly the structure whose single field is that bound; the module doc flags it as the hook for Mathlib’s multivariate Taylor theorem or an IsBigO fallback.
proof idea
One-line term proof: project the cubic_bound field out of the supplied ReggeActionCubicRemainderInput package. No further rewriting or lemma applications occur; the theorem is the interface that turns the named input into the bare LocalCubicRemainderBound proposition.
why it matters
This is the Phase-E cubic remainder theorem for the nonlinear Regge action, stated conditionally on the named Taylor input. It closes the local cubic-control interface that second-variation and continuum-limit arguments need once the Hessian identity is in place.
No downstream consumers are wired yet in the graph, so the declaration presently serves as the stable API surface: anything that later proves the cubic bound (via Mathlib Taylor or an IsBigO estimate on the Cayley–Menger/arccos expansion) discharges the input structure and immediately obtains this theorem. In the broader Recognition geometry stack it sits beside the first-variation and canonical-Hessian identities that prepare a discrete Einstein–Hilbert-type action for continuum comparison.
The open work it points at is materializing the lower-level expansion so the input structure can be constructed rather than assumed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.