continuousLinearMap_apply_eq_sum_single
plain-language theorem explainer
A continuous linear functional on six real coordinates equals the sum of each coordinate times the functional on the corresponding standard basis vector. Anyone assembling a directional derivative of a dihedral angle from six edge-length partials cites this identity. The proof expands the input in the coordinate basis, pushes the map through the finite sum, and factors scalars via homogeneity.
Claim. For every continuous $\mathbb{R}$-linear map $L:(\mathbb{R}^6)\to\mathbb{R}$ and every $v\in\mathbb{R}^6$, $L(v)=\sum_{k} v_k\, L(e_k)$, where $e_k$ is the $k$-th standard basis vector in the six squared-edge coordinates of a tetrahedron.
background
The module targets the vanishing of the first variation of the full nonlinear Regge action at a flat conformal potential. The geometric engine is Schläfli cancellation plus zero deficit; the analytic work is to justify differentiating local dihedral data with respect to the six squared edge lengths of each tetrahedron.
Here the ambient space is $\mathrm{Fin},6\to\mathbb{R}$: one real coordinate per edge of a tetrahedron. Continuous linear maps $L:(\mathrm{Fin},6\to\mathbb{R})\to_L\mathbb{R}$ arise as Fréchet derivatives of smooth angle functionals of those six lengths. The standard basis pieces are the pointwise single-support vectors $\mathrm{Pi.single},k,1$, so evaluating $L$ on them recovers the six coordinate partials.
The supplied dependency edges into Recognition ledgers are name collisions on the binder $L$; the argument uses only finite-dimensional linearity from Mathlib.
proof idea
Reconstruct $v$ as the finite sum of its coordinate spikes via $\mathrm{Finset.univ_sum_single}$. Rewrite $L(v)$ as $L$ of that sum, then apply $\mathrm{map_sum}$ to pass $L$ inside. Termwise, identify $\mathrm{Pi.single},k,(v_k)$ with the scalar multiple $v_k\bullet\mathrm{Pi.single},k,1$ by a pointwise case split on the index, push the scalar through $L$ by $\mathrm{map_smul}$, and simplify the scalar action to ordinary multiplication. The result is the claimed weighted sum of the six basis evaluations.
why it matters
This is the linear-algebra glue that turns six proved coordinate partials into a directional derivative along an arbitrary edge-length velocity. Downstream, $\mathrm{hasDerivAt_flatAngle_directional}$ quotes exactly that assembly: along $t\mapsto a+t\cdot v$ through the flat tuple, the $f$-th dihedral angle has derivative $\sum_k v_k\cdot\mathrm{flatAngleJacobian},f,k$ at $t=0$, built from the $C^1$ Fréchet derivative plus this identity. The same pattern appears in the non-flat generalization $\mathrm{hasDerivAt_angle_directional}$ and in the local chain-rule packages that feed the first-variation and Hessian analyses of the nonlinear Regge action.
In the broader Recognition geometry stack, those derivative gates are the analytic input to Schläfli cancellation at flat configurations, the step that forces the first variation of the Regge action to vanish before second-variation and TT-gauge work begins.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.