nonlinearReggeCubicTaylorTheorem_iff_localBound
plain-language theorem explainer
On any incidence-consistent 3D triangulation, the nonlinear Regge cubic Taylor theorem is definitionally the same proposition as the local cubic remainder bound. Auditors of the Regge remainder expansion cite this to confirm the named theorem carries no extra analytic content. The proof is pure definitional reflexivity (Iff.rfl).
Claim. For every incidence-consistent three-dimensional triangulation $K$, the nonlinear Regge cubic Taylor theorem on $K$ holds if and only if the local cubic remainder bound on $K$ holds.
background
This module isolates the final analytic Taylor step needed once the nonlinear Hessian of the Regge action has been identified. The content is a local third-order bound in the finite-dimensional space of vertex potentials on a 3D triangulation.
The named Taylor theorem is not an independent analytic claim: it is defined to be exactly the local cubic remainder bound for the canonical nonlinear Regge remainder on an incidence-consistent triangulation $K$. The remainder is the object-level leftover after the quadratic (Hessian) contribution is stripped from the nonlinear Regge action.
The surrounding development works in RS geometry after the Hessian identification; the present lemma only records that the theorem name and the bound name are the same proposition.
proof idea
One-line term proof: Iff.rfl. Because NonlinearReggeCubicTaylorTheorem K hK is defined to be LocalCubicRemainderBound K hK, the two sides of the biconditional are definitionally equal, so reflexivity of \leftrightarrow closes the goal with no further lemmas.
why it matters
The lemma exists for audit hygiene, not new analysis. The module doc frames the cubic Taylor bound as the last analytic ingredient after the nonlinear Hessian proof. The declaration's own comment states the point: the identity makes explicit that no hidden analytic assumption is buried in the theorem constructor.
No downstream consumers are recorded yet (used_by is empty), so its role is local bookkeeping inside the Regge cubic-Taylor stack: sibling lemmas that assume the Taylor theorem or produce the local bound can be rewritten across this equivalence without changing mathematical content. It does not itself advance T0-T8 or the RCL; it only keeps the geometry layer's naming honest.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.