Kaplansky unitary density without exp: square of a Cayley transform

The textbook proof of Kaplansky density for unitaries writes U = exp(iH). That needs bounded strong continuity of exp and a cfc∘Borel composition lemma. A route that is easier to formalize: every unitary is U = κ(h)², where κ(h) = (h - i)(h + i)⁻¹ and h = g(U) is a bounded real Borel function of U. Take w = exp(i·arg z/2), which has re w ≥ 0, so |1 + w| ≥ 1, and set g = i(1 - w)/(1 + w). Then κ∘g = -w pointwise, and (-w)² = z on the circle. Identify κ(h) through the purely algebraic X(h + i) = h - i, so no composition lemma is needed. The Cayley transform is strongly continuous on all self-adjoint operators with no norm bound, by the resolvent identity R(a) - R(b) = R(a)(b - a)R(b) with ‖R‖ ≤ 1. So Kaplansky for self-adjoint elements without norm control is enough. In Lean, take κ := cfc (fun z ↦ 1 - 2*I*(z+I)⁻¹). cfc_unitary_iff gives unitarity, cfc_mem gives membership in a closed StarSubalgebra, and norm_cfc_le gives the bounds.