lineTaylorData_of_splitTargets
plain-language theorem explainer
Three separate analytic hypotheses on the line-restricted canonical Regge remainder (C^3 regularity, vanishing quadratic Taylor jet at zero, and a uniform third-derivative bound) combine into the single Mathlib-shaped line-Taylor data package. Anyone assembling the cubic remainder estimate for the nonlinear Regge action cites this glue step. The proof is pure radius-min and reassembly of existentials; no new analysis.
Claim. Let $K$ be an incidence-consistent 3D triangulation. Suppose there exist positive radii on which, for every vertex potential $\xi$ of sufficiently small norm, the map $t \mapsto$ (canonical Regge remainder along the conformal line through $\xi$) is $C^3$ on $[0,1]$, has vanishing quadratic Taylor polynomial at $0$, and has third derivative bounded by $M\|\xi\|^3$ on the segment. Then the combined line-Taylor data target holds for $K$: a single radius and constant $M$ witnessing all three properties simultaneously.
background
This module isolates the final analytic Taylor theorem 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 3D triangulation $K$.
The conclusion target packages Mathlib-shaped one-variable Taylor data along every conformal line: for each direction $\xi$, the line-restricted canonical remainder (Regge action minus its quadratic Hessian form, evaluated on the ray $t\mapsto$ linePotential) is $C^3$ on the unit segment, its quadratic Taylor polynomial at zero vanishes, and its third derivative is bounded by $M|\xi|^3$. The three input targets are exactly those three clauses, each with its own existential radius (and $M$ for the third).
Upstream geometry already supplies the canonical Hessian and the remainder functional; this declaration only merges the split analytic hypotheses into one Prop that downstream cubic estimates can consume.
proof idea
Tactic proof by existential reassembly. Destructure the three hypotheses into radii $r_C,r_T,r_D$ (and bound $M$ from the third-derivative target). Take the combined radius $r=\min(r_C,r_T,r_D)$ and reuse $M$. Positivity of $r$ follows from a three-way min-positivity lemma. For any $\xi$ with $|\xi|<r$, the three elementary min inequalities give $|\xi|<r_C$, $|\xi|<r_T$, and $|\xi|<r_D$, so the ContDiff, quadratic-Taylor-zero, and third-derivative witnesses apply directly and are packaged as a single conjunction.
why it matters
This is the explicit assembly point that turns three independently proved analytic sub-targets into the single line-Taylor data Prop required by the cubic remainder pipeline. Downstream, canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm cites it as the ContDiff / QuadraticTaylorZero / third-deriv half of a larger composite (together with chain-rule and local-norm inputs) that closes the line-Taylor data target from jet inputs under a flat configuration.
In the broader Recognition geometry stack, the cubic Taylor bound on the nonlinear Regge remainder is the last analytic gate after Hessian identification; without this glue lemma the split targets cannot feed the remainder estimate that controls higher-order defect in the discrete action. It does not itself touch the forcing chain (T5–T8) or RCL, but it is part of the geometric scaffolding that makes discrete curvature estimates available to those layers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.