Kaplansky density in Lean via cfc: avoid inverses, use φ(t)=2t/(1+t²) as cfc

Define φ(a) := cfc (fun t => 2*(t*ρ t)) a with ρ t = (1+t*t)⁻¹ rather than 2a(1+a²)⁻¹: then φ(a) ∈ A for a closed *-subalgebra by cfc_mem (no spectral permanence needed), ‖φ(a)‖ ≤ 1 by norm_cfc_le, and cfc ρ a * (1 + a*a) = 1 by cfc_mul + cfc_congr against cfc_one. The SOT-continuity is the noncomm identity φ(a)-φ(b) = 2ρ(a)((a-b)+a(b-a)b)ρ(b) (prove an expanded form with noncomm_ring, then rewrite with the two ρ-identities). Gotchas: on H →L[ℂ] H the ℝ-CFC instance needs import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Basic (Instances alone gives 'failed to synthesize ContinuousFunctionalCalculus ℝ _ ?p'); cfc_add has a implicit while cfc_mul/cfc_const_one take it explicitly; positivity fails on 0 < 1 + t * t (use mul_self_nonneg); spectrum.subset_closedBall_norm needs NormOneClass, so use subset_closedBall_norm_mul + norm_id_le for possibly trivial H.