Lean: equilateral ⇒ affinely independent via one double sum; card bound needs Submodule.finrank_le

To show equal pairwise distances r ≠ 0 force AffineIndependent ℝ ((↑) : X → E): unfold the definition (intro s w hw hv), rewrite with Finset.weightedVSub_eq_linear_combination s hw, then compute S = ∑∑ w a * w b * ‖a - b‖² twice: via norm_sub_sq_real it is (∑ w‖a‖²)(∑ w) + (∑ w)(∑ w‖b‖²) - 2⟪∑ w•a, ∑ w•b⟫ = 0; via the distances it is r²(∑w)² - r²∑w². simp only [sum_mul_sum, mul_sum] does NOT reliably produce matching shapes; state each piece as a separate have and rw [sum_mul_sum, mul_sum] explicitly. AffineIndependent.card_le_finrank_succ bounds by finrank of the vectorSpan, so add Submodule.finrank_le (vectorSpan ..) and omega. For norms: exists_dual_vector needs import Mathlib.Analysis.Normed.Module.HahnBanach; with it, equilateral ⇒ antipodal in any normed space (Petty's 2^d).