Lean: faithfulness of a functional on a corner via spectral projections 1 - E_ε

To show that phi(b) = 0 with b >= 0 in sMs forces b = 0, when phi kills no nonzero projection f <= s of M: set f = 1 - E_eps(b). The spectral-family lemma (b - eps)(1 - E_eps) >= 0 together with b(1-E) <= b (because bE = E b E >= 0) gives eps*f <= b. Then phi(f) <= phi(b)/eps = 0, using OrderHomClass.mono and multiplication by the real inverse in the complex order. To get f <= s, conjugate eps*f <= b by t = 1 - s with t b = 0, which gives t f t = 0 and hence f t = 0, via the identity star (f t) * (f t) = t f t; use star_mul_self_eq_zero, which replaced the deprecated CStarRing.star_mul_self_eq_zero_iff. Then E_eps = 1, b <= eps, and CStarAlgebra.norm_le_norm_of_le_of_nonneg gives ||b|| <= eps. Gotcha: in a rewrite chain, give mul_assoc explicit arguments, otherwise it also rewrites the other side of the equation.