lineCLM
plain-language theorem explainer
Packages the ray t ↦ t • ξ through a fixed vertex conformal potential as a continuous linear map ℝ →L[ℝ] VertexPotential K. Downstream cubic-Taylor and chain-rule arguments on the line-restricted Regge remainder cite it to apply CLM composition lemmas. The body is the standard smulRight construction on the identity map of ℝ.
Claim. For a finite 3D Regge triangulation $K$ and a vertex conformal potential $\xi \in \mathbb{R}^{n_V(K)}$, let $\mathrm{lineCLM}(K,\xi)$ be the continuous $\mathbb{R}$-linear map $\mathbb{R}\to\mathrm{VertexPotential}(K)$ given by $t\mapsto t\cdot\xi$.
background
The module isolates the final analytic cubic Taylor bound on the nonlinear Regge remainder after the Hessian has been identified. The ambient configuration space is the finite-dimensional space of vertex conformal potentials on a triangulation $K$.
A Triangulation3D carries finite vertex/edge/tetrahedron counts with incidence data and nondegenerate squared-edge lengths on each tet. VertexPotential K is the Euclidean space $\mathrm{Fin},n_V\to\mathbb{R}$ of real values at vertices (conformal factors). The zero potential is the flat reference point for the remainder analysis.
Line restrictions $t\mapsto t\cdot\xi$ are the standard device for reducing multivariable Fréchet Taylor estimates to one-variable calculus along rays from the flat configuration.
proof idea
One-line definition: ContinuousLinearMap.smulRight applied to the identity map $\mathrm{id}:\mathbb{R}\to\mathbb{R}$ and the fixed vector $\xi$. By construction this is the continuous linear map sending $t$ to $t\cdot\xi$ in VertexPotential K. No further lemmas are invoked.
why it matters
This is the CLM packaging of the ray through $\xi$, needed so Mathlib chain-rule and iterated-derivative lemmas apply to the line-restricted canonical remainder. Downstream, canonicalRemainder_line_eq_comp identifies the scalar remainder along the ray with $R\circ\mathrm{lineCLM}(K,\xi)$; lineCLM_apply and lineCLM_eq_linePotential are the simp bridges to the ordinary scalar multiple and to linePotential.
Those identities feed the localized closures canonicalRemainderLineChainRuleBound_of_flatConfiguration and canonicalRemainder_iteratedFDeriv3_local_bound_of_flatConfiguration, and the quadratic-Taylor-vanishing statement along rays under a flat configuration. In the broader RS geometry stack this is scaffolding for the cubic remainder bound that closes the nonlinear Regge Hessian analysis in 3D (the $D=3$ landmark of the forcing chain).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.