nonlinearReggeCubicTaylorTheorem_of_lineTaylorData
plain-language theorem explainer
Given Mathlib-shaped one-variable cubic Taylor data along every conformal line in vertex-potential space, the nonlinear Regge remainder obeys the local third-order bound. Analysts closing the Regge cascade cite this to turn line-restricted jet hypotheses into the cubic Taylor theorem. The proof is a two-step term composition: line Taylor data yields a cubic estimate, which is then fed to the estimate-to-theorem bridge.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose that for the canonical Regge remainder there exist $r>0$ and $M\ge 0$ such that, for every vertex potential $\xi$ with $\|\xi\|<r$, the restriction of the remainder along the conformal line $t\mapsto t\xi$ is $C^3$ on $[0,1]$, its quadratic Taylor polynomial at $0$ vanishes, and its third derivative is bounded by $M\|\xi\|^3$ on that segment. Then the local cubic remainder bound holds for $K$: the canonical nonlinear remainder is $O(\|\xi\|^3)$ near the origin.
background
This module isolates the last analytic Taylor step after the nonlinear Hessian of the Regge action has already been identified. The setting is finite-dimensional: vertex potentials on an incidence-consistent 3D triangulation $K$, with the canonical Regge Hessian fixed and the remainder measured relative to that quadratic form.
The hypothesis packages Mathlib-shaped one-variable Taylor data along every conformal line. Concretely, for each direction $\xi$, the line-restricted canonical remainder is $C^3$ on the unit segment, its quadratic jet at zero vanishes, and the third derivative is controlled by $M|\xi|^3$. That is the precise analytic bridge left after geometric reductions.
The target proposition is the exact third-order Taylor estimate specialized to the canonical Regge remainder: a local cubic remainder bound in vertex-potential space. Once that bound is in hand, the remainder is controlled by $O(|\xi|^3)$.
proof idea
Term-mode two-step composition, not a fresh analytic argument. First apply the sibling that turns line Taylor data into a line cubic estimate (lineCubicEstimate_of_lineTaylorData). Then feed that estimate into the bridge theorem that promotes a line cubic estimate to the full nonlinear cubic Taylor theorem (nonlinearReggeCubicTaylorTheorem_of_lineCubicEstimate). No new estimates are proved here; the work is pure packaging of already-reduced one-variable data.
why it matters
Closes one packaging layer in the cubic Taylor cascade for the nonlinear Regge remainder. Downstream it is consumed by nonlinearReggeCubicTaylorTheorem_of_flat_and_remainderJets, the cascade-closure theorem that obtains the cubic Taylor theorem from a flat configuration plus first- and second-variation jet inputs. The module doc frames this as the final analytic Taylor theorem needed once the nonlinear Hessian is identified; the post-proof note records that the canonical nonlinear remainder is then controlled by $O(|\xi|^3)$. In the broader Recognition geometry stack this is the finite-dimensional analytic gate between Hessian identification and remainder control on triangulated 3-space, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.