lineCLM_apply
plain-language theorem explainer
Applying the continuous linear map that scales a fixed vertex potential along the real line recovers ordinary scalar multiplication. Anyone working the cubic Taylor remainder for the nonlinear Regge action on a 3D triangulation cites this as the evaluation identity for that line map. The proof is a one-line simp unfolding the smulRight construction.
Claim. For any finite 3D triangulation $K$, any vertex conformal potential $\xi$ on $K$, and any real scalar $t$, the continuous linear map $s\mapsto s\cdot\xi$ from $\mathbb{R}$ into the vertex-potential space evaluates at $t$ to $t\cdot\xi$.
background
This module isolates the final analytic Taylor theorem needed after the nonlinear Hessian of the Regge action has been identified: a local third-order bound on the remainder in the finite-dimensional space of vertex conformal potentials.
A Triangulation3D is a finite 3D Regge complex with incidence data and nondegenerate squared-edge lengths on every tetrahedron. The vertex-potential space is the Euclidean space $\mathbb{R}^{n_V}$ of real values at the vertices (conformal factors). The auxiliary map in view is the continuous linear map $\mathbb{R}\to L(\mathrm{VertexPotential})$ that sends a scalar $t$ to the scaled potential $t\cdot\xi$, built as smulRight of the identity on $\mathbb{R}$.
That line map is the path along which the cubic remainder of the nonlinear Regge action is restricted when proving chain-rule and Taylor estimates near a flat configuration.
proof idea
One-line wrapper. Unfold the definition of the line map (continuous linear map given by smulRight of the identity against the fixed potential $\xi$) and apply the standard evaluation lemma for smulRight; simp closes the goal.
why it matters
This evaluation identity is the first simp fact for the line map. Immediately downstream it feeds the equality of the continuous-linear-map path with the ordinary scalar path linePotential, and it is used inside the localized closure of the canonical remainder line chain-rule bound: within a small ball about the flat point, points $t\cdot\xi$ for $t\in[0,1]$ stay in the ContDiff neighborhood so the within-set iterated Fréchet chain rule applies to the cubic remainder.
In the broader Recognition geometry stack this is scaffolding for the cubic Taylor control of the nonlinear Regge remainder after the Hessian identification, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.