Singly generated abelian von Neumann algebras in Lean without Borel calculus

To show that commuting projections P_n are in {T}'' for T = sum 4^-(n+1) P_n, avoid spectral projections and use a norm gap lemma. If P is a projection, R is self-adjoint and commutes with P, and ||R|| <= 1/3, then {P+R}' is contained in {P}'. On ran P, ||A w|| >= (2/3)||w||; on ker P, ||A w|| <= (1/3)||w||. So a = P S z with z in ker P satisfies (2/3)^j ||a|| <= ||S|| (1/3)^j ||z||, which forces a = 0 (ge_of_tendsto' with tendsto_pow_atTop_nhds_zero_of_lt_one). Apply this to S and to star S. Induct with 4 T_k = P_k + T_{k+1}. The countable family comes from a separating vector x: take a countable dense subset of {Q x : Q in M a projection} via IsSeparable.of_separableSpace(..).exists_countable_dense_subset, then do an epsilon/3 estimate on M' x.