canonicalRemainderLineThirdDerivBound_closed
plain-language theorem explainer
For any incidence-consistent 3D triangulation that admits a flat analytic configuration, the cubic Taylor remainder of the nonlinear Regge action along the segment from the flat base is controlled by a uniform third-derivative bound near the origin in vertex-potential space. Agents that need only this bound, without the full remainder-closure audit, cite this certificate. The proof is a one-line projection out of the analytic remainder closure package.
Claim. Let $K$ be an incidence-consistent three-dimensional triangulation admitting a flat analytic configuration. Then there exist radii $r>0$ and $M\ge 0$ such that for every vertex potential $\xi$ with $\|\xi\|<r$ and every $t\in[0,1]$, the absolute value of the third iterated derivative of the nonlinear Regge action along the line from the flat base point toward $\xi$ is at most $M$.
background
This module is the lane-local audit for Track 1B-REM on the analytic-remainder branch of the nonlinear Regge action. The broader progress audit pulls in finite-Freudenthal combinatorics, so this file isolates a buildable closure certificate for the smooth remainder analysis alone.
A flat analytic configuration packages three facts at the base point: the arccos endpoint is free (squared dihedral cosines avoid $\pm 1$), all deficits vanish, and the nonlinear action is smooth enough to invoke Taylor theory. The target proposition asserts existence of a neighborhood radius $r$ and a uniform bound $M$ on the third iterated derivative of the action along every line segment from that flat base into a ball of vertex potentials.
Upstream, the cubic-Taylor-bound module defines that target as an existential statement over $r$ and $M$; the smoothness module supplies the flat-configuration structure; the sibling analytic-closure record packages the full remainder package from which individual bounds are projected.
proof idea
One-line term proof. Instantiate the analytic remainder closure record at the given triangulation and incidence hypothesis, then apply its projection that extracts the line third-derivative bound from a flat configuration. No additional algebraic work occurs at this site; the heavy lifting lives in the closure package and the cubic Taylor infrastructure it re-exports.
why it matters
Gives agents a thin import path to the third-derivative control that underwrites the cubic Taylor theorem for the nonlinear Regge action, without forcing the broad remainder-progress audit or the finite-Freudenthal combinatorics stack. In the Recognition geometry lane this bound is the analytic half of Track 1B-REM: once the third derivative is controlled near a flat base, the cubic remainder is $O(|\xi|^3)$ and the local Hessian/J-cost correspondence can be stated cleanly.
Sibling closures in the same audit file cover the full cubic Taylor endpoint, local Hessian Taylor inputs, the J-cost local correspondence, and the strongest true Regge-to-J-cost replacement. No downstream consumers are wired yet; the declaration is an export surface for later geometry and forcing-chain work that needs only the third-derivative fact. It does not itself touch T5–T8 or the Recognition Composition Law, but it stabilizes the continuum side of the discrete-to-continuum bridge those landmarks eventually use.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.