TwoSparse
plain-language theorem explainer
A vector α in R^n is two-sparse on indices i0, i1 when every coordinate outside {i0, i1} vanishes. This is the general-n support hypothesis that lets n-dimensional projector algebra collapse to the 2D scalar certificates. Anyone proving block reduction of P_λ or μ_λ on a two-coordinate slice cites it. The body is a plain Prop: a universal quantifier forcing off-support coordinates to zero.
Claim. For $n \in \mathbb{N}$, a vector $\alpha \in \mathbb{R}^n$ and indices $i_0, i_1 \in \{0,\ldots,n-1\}$, $\alpha$ is two-sparse on $(i_0,i_1)$ when $\alpha_k = 0$ for every $k \neq i_0, i_1$.
background
The ambient objects are coordinate vectors Vec n := Fin n → ℝ. The module lifts the 2D non-parallelism and non-flatness results of ScalarCertificates to arbitrary ambient dimension n. The strategy is algebraic block reduction: instantiate the abstract projector PApply of Projector.lean at the inverse undeformed metric Dinv t and a covector α supported on exactly two indices, then evaluate on the indicator direction e i0.
Two-sparsity is the support hypothesis that makes every sum in AApply and mu collapse. Off-support coordinates of α vanish, so the n-dimensional sums reduce exactly (not up to isomorphism) to two-term closed forms matching the 2D setup α = (a, b). The module doc states the target identity: PApply lam (Dinv t) α (e i0) i0 = P00Gen (α i0) (α i1) (t i0) when t i1 = 0.
proof idea
Definition, not a proved theorem. The predicate is the universal statement that α k = 0 whenever k differs from both i0 and i1. No tactics or lemmas; it is the Prop that downstream theorems take as a named hypothesis and discharge by Finset support arguments (as in sum_twoSparse).
why it matters
This is the structural hypothesis behind the panel-greenlit general-n extension of Theorem 1a. Downstream, sum_twoSparse collapses weighted sums of α_i² to the two active indices; mu_Dinv_twoSparse reduces the projector scalar μ_λ to a two-term cosh formula; PApply_e_eq_P00Gen is the block-reduction identity equating the n-dimensional (i0,i0) projector entry to the 2D closed form P00Gen; PApply_not_parallel_gen then transports dP00Gen_ne_zero to every n ≥ 2.
CurvatureBridge reuses it for spectator vanishing of the third-derivative tensor β and for the restricted sharp product dot α (D⁻¹ α). Without two-sparsity the n-dimensional sums do not algebraically equal the 2D certificates, so the cost-side non-parallelism of P_λ w.r.t. the flat connection D would remain stuck at n = 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.