lineCLM_eq_linePotential
plain-language theorem explainer
On a 3D triangulation, the continuous linear map sending a scalar t to t scaled by a fixed vertex potential equals the ordinary line-through-flat potential at t. Anyone chaining Fréchet derivatives of the Regge remainder along rays from the flat configuration cites this identification. The proof is a two-rewrite wrapper equating both sides to scalar multiplication.
Claim. For any 3-dimensional triangulation $K$, any vertex potential $\xi$, and any real scalar $t$, the continuous linear map $t \mapsto t\cdot\xi$ evaluates at $t$ to the same vertex potential as the affine line through the flat configuration in direction $\xi$ at parameter $t$.
background
The module isolates the cubic Taylor bound for the nonlinear Regge remainder after the Hessian has been identified: a local third-order estimate in the finite-dimensional space of vertex potentials on a triangulation $K$.
Two parallel presentations of the ray from the flat point appear. The first-variation module defines linePotential pointwise by $(t\cdot\eta)(i)=t,\eta(i)$. In this module, lineCLM packages the same ray as the continuous linear map $\mathbb{R}\to L[\mathbb{R}]$ VertexPotential given by right scalar multiplication by $\xi$. The simp lemma lineCLM_apply unfolds that CLM to $t\bullet\xi$; the earlier identity linePotential_eq_smul shows the pointwise line is the same scalar multiple.
Identifying the two is bookkeeping needed before the chain rule can treat the line-restricted remainder as a composition $R\circ\mathrm{lineCLM}$.
proof idea
One-line wrapper. Rewrite with lineCLM_apply to replace the CLM evaluation by $t\bullet\xi$, then rewrite backwards with linePotential_eq_smul to match the pointwise line potential. No analytic content.
why it matters
Feeds two local parents in the same module. canonicalRemainder_line_eq_comp uses the equality to write the line-restricted canonical remainder as the composition of the remainder functional with lineCLM, which is the form required by continuous-linear-map chain rules. canonicalRemainderLineChainRuleBound_of_flatConfiguration then closes the localized target CanonicalRemainderLineChainRuleBoundTarget: inside a small ball about the flat configuration, ContDiff of order 3 plus the within-set iterated Fréchet chain rule control the cubic remainder along rays $t\bullet\xi$ for $t\in[0,1]$.
In the broader RS geometry stack this is pure scaffolding for the cubic Taylor theorem on the nonlinear Regge action (the analytic step after Hessian identification). It does not itself touch T0–T8, the RCL, or the mass ladder; it only clears the notation mismatch between first-variation lines and CLM rays so the remainder bound can fire.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.