dot_e
plain-language theorem explainer
The weighted inner product of any coordinate vector α against the standard basis indicator at index i₀ recovers exactly the component α(i₀). Anyone working the general-n block reduction of the projector P_λ cites this as the elementary extraction identity for the indicator direction e_{i₀}. The proof unfolds the sum definitions and collapses the Finset sum to the single matching index.
Claim. For every ambient dimension $n$, every coordinate vector $\alpha\in\mathbb{R}^n$, and every index $i_0\in\{0,\ldots,n-1\}$, if $e_{i_0}$ denotes the standard basis indicator ($1$ at $i_0$ and $0$ elsewhere), then $\sum_{i}\alpha_i\,(e_{i_0})_i=\alpha_{i_0}$.
background
The ambient setting is the general-$n$ block reduction of the projector $P_\lambda$. Vectors are coordinate maps $\mathrm{Vec},n:=\mathrm{Fin},n\to\mathbb{R}$. The weighted product $\mathrm{dot},\alpha,t:=\sum_i\alpha_i t_i$ is the logarithmic aggregate used throughout the $N$-dimensional cost calculus. The indicator $e_{i_0}$ is the coordinate basis vector that is $1$ at $i_0$ and $0$ elsewhere; evaluating the projector on this direction isolates the $(i_0,i_0)$ entry needed for the reduction.
Module context: ScalarCertificates already treats the genuine $2$D slice. This module lifts non-parallelism of $P_\lambda$ relative to the flat connection $D$ to arbitrary ambient $n$, for any $\alpha$ supported on two coordinates (a $2$-sparse vector). The inverse undeformed metric $D^{-1}(t)=\mathrm{diag}(\cosh(t_i)^{-1})$ and the sharp map (raising a covector by the inverse-metric kernel) appear later in the same reduction chain; the present identity is the pure linear-algebra extraction step that feeds those arguments.
proof idea
Unfold the definitions of the weighted product and of the indicator $e_{i_0}$. Rewrite the resulting finite sum by Finset.sum_eq_single at the index $i_0$. The matching term simplifies to $\alpha_{i_0}\cdot 1$. Off-diagonal terms vanish because the indicator is zero there. The membership side-condition is discharged by the fact that every Fin n index lies in the universe set, so the excluded-index case is absurd.
why it matters
This is a @[simp] extraction lemma inside the general-$n$ architecture that realizes Theorem 1a beyond the $2$D slice. Its sole recorded consumer is the block-reduction identity PApply_e_eq_P00Gen: for $2$-sparse $\alpha$, $\lambda\neq 0$, and background $t$ with $t_{i_1}=0$, the $(i_0,i_0)$ entry of the abstract $n$-dimensional projector $P_\lambda=P\mathrm{Apply},\lambda,(D^{-1}t),\alpha$ applied to $e_{i_0}$ equals exactly the closed $2$D form $P_{00}\mathrm{Gen}(\alpha_{i_0},\alpha_{i_1},t_{i_0})$. Without component extraction against $e_{i_0}$, that algebraic collapse cannot even be stated. Downstream, agreement of the two sides as functions of the free coordinate lets the already-proved $2$D non-vanishing derivative transport to PApply_not_parallel_gen, closing the general-$n$ non-parallelism claim for the cost projector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.