nonlinearReggeCubicTaylorTheorem_of_identically_zero
plain-language theorem explainer
When the nonlinear Regge remainder vanishes for every vertex conformal potential, the cubic Taylor bound holds with zero cubic constant. Cited by the local J-cost correspondence under the same vanishing hypothesis. Proof is a direct term construction: radius one, constant zero, rewrite by vanishing.
Claim. Let $K$ be a finite 3D triangulation with consistent incidence. If the Regge action remainder relative to the canonical graph-Laplacian Hessian vanishes for every vertex conformal potential $\xi$, then the local cubic remainder bound for the nonlinear Regge action holds on $K$.
background
This module isolates the final analytic Taylor theorem needed after the nonlinear Hessian of the discrete Regge action is identified. The heavy content is a local third-order bound on the finite-dimensional space of vertex conformal potentials (real assignments to the vertices of a 3D triangulation $K$).
The Regge action remainder is the full Regge action minus its value at the zero potential minus one-half the quadratic form of a candidate Hessian. The canonical Hessian is the graph Laplacian induced by incidence dual weights. Incidence consistency of $K$ makes those weights and the Hessian well-defined.
The target proposition is exactly that finite-dimensional local cubic remainder bound, specialized to the canonical remainder: a radius and a constant that control cubic growth of the remainder near the origin in potential space.
proof idea
Term-mode construction of the local cubic bound package. Supply radius $1$ and cubic constant $0$; discharge the numeric side conditions by norm_num and le_rfl. For an arbitrary potential in the unit ball, rewrite the remainder by the global vanishing hypothesis, then simplify: both sides of the cubic estimate are zero.
why it matters
Closes the identically-vanishing special case of the cubic Taylor interface on the geometry side of Recognition Science. Downstream, the nonlinear Regge–J-cost local correspondence under remainder vanishing applies this lemma to obtain the local correspondence between the nonlinear Regge action and the J-cost. The declaration doc is explicit that the genuine nonlinear theorem will replace this strong hypothesis by a finite-dimensional third-order estimate; the present result is the bridge for that upgrade. It sits after Hessian identification and before continuum-curvature recovery on 3D triangulations (aligned with the forcing-chain conclusion $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.