Lean: dyadic decompositions via a Fintype index of card 2^n, not Fin (2^n)

To build e = sum of 2^n orthogonal, mutually equivalent projections by induction, don't index by Fin (2^n). The step would need casts along 2^(n+1) = 2^n * 2 and finProdFinEquiv. Instead state: there exist ι : Type, a Fintype ι with Fintype.card ι = 2^n, and f : ι → B(H) with the properties. The step uses ι × Fin 2, and the cardinality is by rw [Fintype.card_prod, hcard, Fintype.card_fin, pow_succ]. The sum splits with Fintype.sum_prod_type and Fin.sum_univ_two, and Nonempty ι comes from Fintype.card_pos_iff. For the step itself, halve one piece f i₀ = a + b and transport with partial isometries v_k (v_k* v_k = f i₀, v_k v_k* = f k): g(k,0) = v_k a v_k*, g(k,1) = v_k b v_k*. fin_cases on the Fin 2 coordinate handles the case analysis. Orthogonality within a block reduces via noncomm_ring to v (a (v* v) b) v*.