nonlinearReggeCubicTaylorTheorem_of_remainderJetInputs
plain-language theorem explainer
Given an incidence-consistent 3D triangulation with a flat background, plus the packaged jet-level Taylor implication and the first- and second-variation vanishing inputs for the canonical Regge remainder, the local cubic remainder bound holds. Discrete-gravity analysts cite this once the jet hypotheses are assembled, to discharge the third-order estimate on the nonlinear remainder. The proof is a one-line application of that packaged implication to the two variation inputs.
Claim. Let $K$ be an incidence-consistent 3-dimensional triangulation admitting a flat configuration. Suppose the canonical Regge remainder satisfies the finite-dimensional analytic claim that vanishing first and second variations imply a local cubic bound, and suppose the first variation of the remainder (relative to the canonical graph-Laplacian Hessian) vanishes at the zero potential and the second-variation input holds. Then the nonlinear Regge cubic Taylor theorem holds: the remainder obeys a local $O(\|\xi\|^3)$ bound near the flat point.
background
This module isolates the final analytic Taylor theorem needed after the nonlinear Hessian has been identified. The heavy content is a local third-order bound in the finite-dimensional vertex-potential space on a 3D triangulation.
In the discrete setting the Regge action splits into a quadratic piece given by the canonical Hessian (the graph Laplacian induced by incidence dual weights) plus a nonlinear remainder. A flat configuration is a background assignment with vanishing deficit angles. The remainder is already smooth at the flat point and vanishes there.
The first-variation input records that the Fréchet derivative of the remainder at the zero potential is zero (relative to that canonical Hessian). The second-variation input is the matching second-order jet condition. The jet-input target packages the pure analytic implication from those two vanishings to the local cubic remainder bound, without adding an axiom.
proof idea
One-line wrapper. The jet-input target is already an implication
first-variation input → second-variation input → cubic Taylor theorem.
The proof applies that implication to the supplied first- and second-variation hypotheses and returns the cubic bound. No further rewriting or analysis is performed here.
why it matters
After the nonlinear Hessian is identified and smoothness of the remainder at the flat point is secured, the remaining analytic step is the third-order Taylor estimate in vertex-potential space. This declaration is the discharge lemma for that step: it turns the packaged jet-input target plus the two variation inputs into the named cubic Taylor theorem (itself an alias of the local cubic remainder bound).
No downstream consumers are recorded yet. Intended use is error control when expanding the discrete action about flat space, feeding continuum-limit and curvature-recovery arguments on the Recognition geometry side. The result is pure finite-dimensional analysis; it does not invoke the forcing chain (T0–T8), the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.