canonicalRemainderLineQuadraticTaylorZero_of_jetInputs
plain-language theorem explainer
On a flat 3D triangulation, the degree-2 Taylor polynomial of the line-restricted canonical Regge remainder vanishes at t=1 for every vertex potential. Anyone assembling the cubic remainder bound or the analytic-closure certificate cites this. The proof expands the Taylor sum into three iterated derivatives and invokes vanishing lemmas for orders 0, 1, and 2.
Claim. Let $K$ be an incidence-consistent 3D triangulation that is flat, and suppose the canonical Regge remainder admits the stated first- and second-variation jet inputs at the canonical Hessian. Then there exists $r>0$ (in fact $r=1$ works) such that for every vertex potential $\xi$ with $\|\xi\|<r$, the degree-2 Taylor polynomial at $0$ of $t\mapsto$ (canonical remainder along the line potential of $\xi$) evaluates to $0$ at $t=1$.
background
This module isolates the final analytic Taylor step after the nonlinear Hessian of the Regge action has been identified. The ambient object is a finite-dimensional space of vertex potentials on a 3D triangulation $K$; the canonical remainder is the nonlinear Regge action minus its quadratic Hessian piece at the flat configuration.
The target proposition asserts existence of a radius $r>0$ so that, along every short line $t\mapsto$ linePotential$(K,\xi,t)$ in potential space, the degree-2 Taylor polynomial of the restricted remainder at $0$ evaluates to zero at the endpoint $t=1$. The radius is conventional: the identity holds for all $\xi$, so $r=1$ is enough.
Hypotheses package flatness of $K$ together with first- and second-variation jet inputs for the remainder at the canonical Hessian. Those inputs supply the vanishing of the constant, linear, and quadratic jets needed below; they sit upstream of the cubic remainder bound that is the module's end goal.
proof idea
Term-mode construction of the existential: take radius $r=1$ (positive by norm_num). For arbitrary $\xi$, rewrite taylorWithinEval of degree 2 via taylor_within_apply as a sum of three iteratedDerivWithin terms over $k\in{0,1,2}$.
Invoke three vanishing lemmas:
- order 0:
iteratedDerivWithin_zero_canonicalRemainderLine; - order 1:
iteratedDerivWithin_one_canonicalRemainderLine_of_jetInputs(uses flatness and the first-variation input); - order 2:
iteratedDerivWithin_two_canonicalRemainderLine_of_jetInputs(uses flatness and the second-variation input).
A short simp over Finset.sum_range_succ collapses the sum to zero.
why it matters
Closes the quadratic-Taylor-zero leg of the line-restricted remainder analysis. Downstream, canonicalRemainderAnalyticClosureCert wires this lemma in as line_quadratic_zero_from_jets. The sibling canonicalRemainderLineQuadraticTaylorZero_of_flat_first_and_directionalHessian re-packages the same target from flatness, first variation, and the directional Hessian theorem. The composite canonicalRemainderLineTaylorData_of_jetInputs_chainRule_and_localNorm assembles ContDiff, this quadratic zero, chain rule, and local-norm bound into full line-Taylor data.
In the Recognition geometry stack this is the analytic step that lets the nonlinear Regge remainder be controlled by a pure cubic estimate after the Hessian is fixed, feeding the continuum bridge from discrete ledger curvature to continuum action. It does not itself touch T5–T8 or the RCL; it is infrastructure for the Regge-side continuum limit.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.