NonlinearReggeCubicTaylorTheorem
plain-language theorem explainer
Names the exact finite-dimensional cubic Taylor estimate required for the canonical nonlinear Regge remainder on an incidence-consistent 3D triangulation: the remainder is locally O(‖ξ‖³) in vertex-potential space. Downstream cascade closures and the T5-to-nonlinear-Regge bridge cite this Prop as the analytic target. The body is a pure abbreviation of the local cubic remainder bound.
Claim. For an incidence-consistent 3D Regge triangulation $K$, the nonlinear Regge cubic Taylor theorem is the assertion that there exist $r>0$ and $C\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$, the canonical Regge-action remainder satisfies $\|R(\xi)\|\le C\|\xi\|^3$.
background
The module isolates the last analytic Taylor statement needed once the nonlinear Hessian of the Regge action is identified. The setting is finite-dimensional: vertex potentials on a 3D Regge triangulation with abstract incidence data and nondegenerate squared-edge lengths on every tetrahedron.
Incidence consistency packages global squared-edge data, agreement of local tetrahedral edge slots with global endpoints (up to orientation), and the local closed-form Schläfli identity used to assemble global Schläfli without caller-supplied data.
Upstream, LocalCubicRemainderBound already states the concrete estimate: existence of a radius $r>0$ and constant $C\ge 0$ so that the canonical remainder (Regge action minus its quadratic Hessian jet) is bounded by $C|\xi|^3$ whenever $|\xi|<r$. This definition simply promotes that bound to the named theorem target for the nonlinear remainder.
proof idea
One-line definitional wrapper: the proposition is definitionally equal to the local cubic remainder bound on the same triangulation and incidence hypothesis. No tactics, no lemmas, no extra hypotheses. The companion identity lemma records this as an Iff.rfl equivalence so audits see that nothing analytic is hidden in the name.
why it matters
This is the exact Taylor theorem the nonlinear Regge remainder needs after the Hessian is fixed. Module siblings use it as the discharge target: cubic remainder input is assembled from Hessian identification plus this theorem; cascade closures derive it from flat configuration plus first- and second-variation jet inputs; analytic-closure certificates package the line-contDiff and jet path into a single cert.
In the forcing chain it feeds the T5/J-cost → nonlinear Regge curvature-action bridge certificate, linking J-uniqueness (T5) to the discrete curvature action. Within RS geometry it is the finite-dimensional $O(|\xi|^3)$ control that lets the canonical remainder sit under the cubic envelope required for the nonlinear analysis, without introducing an axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.