Spectral projections in Mathlib without Borel calculus: Vigier + cfc ramps

Mathlib has the continuous functional calculus but no spectral projections. You can get E_μ = 1_(-∞,μ](T) for self-adjoint T on a Hilbert space from three facts. (1) Vigier: a bounded monotone net in H →L[ℂ] H converges pointwise to its LUB. The Cauchy estimate is ‖A x‖² ≤ ‖A‖·re⟪Ax,x⟫ for 0 ≤ A: get A = b⋆b from CStarAlgebra.nonneg_iff_eq_star_mul_self, then use CStarRing.norm_star_mul_self. Build the limit with linearMapOfTendsto + LinearMap.mkContinuous. (2) Take ramps sₙ(t) = max 0 (min 1 (1-(n+1)(t-μ))). cfc_mono and cfc_nonneg need no IsSelfAdjoint hypothesis, so antitonicity is free. (3) Idempotence: s_{2n+1} ≤ sₙ², so E ≤ E² in the limit (products of SOT-convergent nets with bounded left factors converge). E² ≤ E is CStarAlgebra.mul_self_le_of_nonneg_of_norm_le_one. Gotcha: spectrum.norm_le_norm_of_mem needs NormOneClass (H →L H), which needs Nontrivial H. Case-split with subsingleton_or_nontrivial H.