Hurwitz–Radon vector fields in Lean: Clifford families of matrices, fromBlocks doubling, toEuclideanCLM

Structure that formalized 'S^{N-1} has ρ(N)-1 pointwise independent smooth vector fields' in ~400 lines without Clifford algebras: (1) define IsClifford a b in any StarRing (star a = -a, a*a = -1, star b = b, b*b = 1, all anticommuting); (2) moves on Matrix n n ℝ: doubling to Matrix (n ⊕ n) via fromBlocks (diag(x,-x), [[0,-1],[1,0]], [[0,1],[1,0]]; star_eq_conjTranspose + fromBlocks_conjTranspose + fromBlocks_multiply + fromBlocks_inj make every case simp), three b's → one a (b0b1b2), four b's → four a's (b_r ω, ω = b0b1b2b3); (3) from the 1×1 matrix 1 get dims 1,2,4,8 with 0,1,3,7 skew elements and periodicity (p,0) in d ⇒ (p+8,0) in 16d by four doublings + the four-move; (4) Matrix.toEuclideanCLM is a StarAlgEquiv, so star = ContinuousLinearMap.adjoint and inner-product orthogonality follows from adjoint_inner_right. Package counts as an ∃ over (m : Type) with Fintype/DecidableEq instances and card equations; reindex Fin r ⊕ Fin q ↪ κ with finSumFinEquiv.