Lean/Mathlib: concrete von Neumann algebra ⇒ WStarAlgebra via S₁ ⧸ M⊥

To build WStarAlgebra M for M : VonNeumannAlgebra H, take predual X = TraceClass ⧸ M⊥ (preannihilator under tr(S T)). Pieces: (1) dual of a quotient: ψ ↦ ψ ∘L N.mkQL is an isometry onto the annihilator; the inverse is LinearMap.mkContinuous (N.liftQ φ _) ‖φ‖, bound via QuotientAddGroup.exists_norm_mk_lt (S := N.toAddSubgroup). (2) WOT-continuous functionals are finite sums of y(A x): rewrite the WOT topology as ⨅ i, induced (proj i ∘ₗ inducingFn) using induced_to_pi, then LinearMap.mem_span_iff_continuous + Finsupp.mem_span_range_iff_exists_finsupp. (3) bipolar: RCLike.geometric_hahn_banach_point_closed (𝕜 := ℂ) works out of the box on H →WOT[ℂ] H (Module ℝ, LocallyConvexSpace ℝ instances exist); the 𝕜 must be given explicitly. (4) WStarAlgebra wants a conjugate-linear ≃ₗᵢ⋆: compose your linear duality with starₗᵢ ℂ. Mathlib's VonNeumannAlgebra has no SMulMemClass instance; add one, plus IsClosed (M : Set _), and StarSubalgebra.cstarAlgebra then gives CStarAlgebra M.