lineCLM_one
plain-language theorem explainer
Evaluating the line continuous-linear map of a vertex potential at parameter 1 recovers that potential. Anyone restricting the Regge remainder along rays in vertex-potential space cites this endpoint identity. The proof is a one-line simplification of the line-map definition (scalar multiplication).
Claim. For any 3D triangulation $K$ and any vertex potential $\xi$ on $K$, the continuous linear map sending a scalar $t$ to the scaled potential $t\cdot\xi$ satisfies evaluation at $1$: the image is exactly $\xi$.
background
The module isolates the final analytic cubic Taylor theorem for the nonlinear Regge remainder after the Hessian has been identified. The setting is finite-dimensional: vertex potentials on a 3D triangulation, with the flat (zero) configuration as the expansion point.
To get a one-variable cubic bound, one restricts the canonical remainder along the ray from zero toward a fixed potential $\xi$. That restriction is implemented by a continuous linear map (the line map) that sends the scalar parameter $t$ to $t\cdot\xi$. Sibling facts record the same scaling for the ordinary line potential and norm control for $t\in[0,1]$.
This identity is the $t=1$ endpoint of that ray: the line map lands back on $\xi$ itself, so chain-rule and composition statements at the free endpoint match the unrestricted remainder at $\xi$.
proof idea
One-line wrapper. The tactic simp unfolds the definition of the line continuous-linear map, which is scalar multiplication of $\xi$ by the real parameter; at parameter $1$ this is definitionally $\xi$.
why it matters
Feeds the localized closure theorem canonicalRemainderLineChainRuleBound_of_flatConfiguration, which discharges CanonicalRemainderLineChainRuleBoundTarget. That parent result needs the line map to stay inside a small ball about the flat point for $t\in[0,1]$ and to apply the within-set chain rule for iterated Fréchet derivatives of the canonical remainder composed with the line map.
Without the $t=1$ identity, the composed derivatives at the free endpoint would not match the unrestricted remainder jet at $\xi$. The surrounding cubic Taylor infrastructure is the last analytic step after the nonlinear Hessian identification in the Regge-action geometry stack (spatial dimension $D=3$ as forced in the Recognition chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.