reggeActionCubicRemainderInput_of_taylorTheorem
plain-language theorem explainer
Packages a local cubic Taylor bound on the nonlinear Regge remainder as the named remainder-input structure used by second-variation arguments. Anyone assembling Hessian-plus-Taylor control of the Regge action near a flat configuration would cite this. The body is a one-line wrapper through the bound constructor, with no extra analytic content.
Claim. Given a 3D triangulation $K$ with consistent incidence, a flat configuration on $K$, and a proof of the local cubic remainder bound for the nonlinear Regge action on $K$, produce the named cubic-remainder input package for that flat configuration.
background
This module isolates the final analytic Taylor step needed after the nonlinear Hessian of the Regge action has been identified. The heavy content is a local third-order bound in the finite-dimensional space of vertex potentials on a fixed 3D triangulation.
The Taylor hypothesis is the proposition that the canonical nonlinear Regge remainder obeys a local cubic remainder bound on $K$. That proposition is definitionally identical to the finite-dimensional third-order estimate specialized to the Regge remainder. The target structure is the named Taylor-remainder input whose sole field is that cubic bound: the exact place where Mathlib's multivariate Taylor theorem, or an IsBigO fallback, is meant to connect.
A flat configuration is a background edge-length assignment against which the second variation and remainder are expanded. Incidence consistency ensures the triangulation supports well-defined hinges and deficit angles.
proof idea
One-line wrapper. It applies the existing bound constructor, feeding the Taylor hypothesis (already a local cubic remainder bound) together with the triangulation, incidence proof, and flat configuration into the named remainder-input structure. No new estimate is proved; the definition only makes the packaging explicit so the audit trail does not hide analytic assumptions inside a constructor.
why it matters
Downstream, the Hessian-plus-Taylor assembler uses this packaging so that, once the nonlinear Hessian is identified and the cubic Taylor theorem is available, the canonical nonlinear remainder is controlled by $O(|\xi|^3)$. A second consumer builds the combined local Hessian-Taylor input bundle from an eventually-zero edge stencil and the same Taylor hypothesis.
In the Recognition geometry stack this is the thin interface between the analytic Taylor fact and the second-variation calculus for discrete gravity. It does not itself touch the forcing chain (T0-T8), the Recognition Composition Law, or the phi-ladder mass formula; it only supplies the cubic remainder slot those continuum-limit arguments need once the Regge action is expanded about a flat background.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.