CanonicalRemainderCubicTaylorFromJetInputsTarget
plain-language theorem explainer
Packages the last analytic obligation for the nonlinear Regge remainder: vanishing first and second variations at a flat configuration imply the local cubic remainder bound. Geometry and discrete-gravity workers cite it as the exact finite-dimensional Taylor step left after smoothness and jet vanishing. It is a pure Prop abbreviation chaining two named input structures to the cubic theorem, with no proof content.
Claim. For an incidence-consistent 3D triangulation $K$ and a flat configuration on $K$, the named proposition asserts: if the first variation of the canonical Regge remainder (relative to the graph-Laplacian Hessian) vanishes at the zero potential, and the second variation of that remainder also vanishes, then the local cubic remainder bound holds.
background
The module isolates the final analytic Taylor step for the nonlinear Regge remainder after the Hessian has been identified. The setting is finite-dimensional: vertex potentials on a 3D triangulation $K$ that is incidence-consistent, expanded about a flat configuration (zero deficit angles).
The canonical Regge Hessian is the graph-Laplacian built from incidence dual weights. The remainder is the nonlinear part of the Regge action after the quadratic Hessian term is subtracted. Two upstream input structures record the jet data still needed: first-variation input asserts that the Fréchet derivative of the remainder at the zero potential is zero (for a given Hessian $H$); second-variation input asserts that the canonical remainder's second variation vanishes.
NonlinearReggeCubicTaylorTheorem is itself an alias for the local cubic remainder bound: the remainder is $O(|\xi|^3)$ near zero in the vertex-potential norm. Smoothness of the canonical remainder at the flat point and vanishing of its value are already available upstream; what remains is the pure Taylor implication from jet vanishing to the cubic estimate.
proof idea
Definitional packaging only: the body is the implication
first-variation input (for the canonical Hessian) $\to$ second-variation input $\to$ cubic Taylor theorem.
No tactics, no lemmas applied. The flat-configuration hypothesis is carried as an unused binder so downstream consumers can thread the same configuration context.
why it matters
Closes the interface gap between jet-vanishing lemmas and the cubic bound without inserting an axiom. Downstream, nonlinearReggeCubicTaylorTheorem_of_remainderJetInputs consumes this target together with concrete first- and second-variation witnesses to discharge the cubic theorem. A second consumer builds the full local Hessian–Taylor input package from an eventually-zero edge stencil plus this jet target.
In the broader Recognition geometry stack this is the last pure-analysis hinge before discrete curvature expansions can feed continuum limits and forcing-chain geometry (spatial dimension and octave structure sit upstream of the triangulation model). It does not itself touch $J$-cost, $\varphi$, or the RCL; it only certifies the cubic remainder estimate those continuum arguments rely on.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.