Lean: positive normal functional = tr(. rho), rho >= 0, via Hilbert-Schmidt amplification

To upgrade phi = tr(. T) on a von Neumann algebra M (T trace class, not positive) to a positive density matrix, use the Hilbert-Schmidt space S2(H) as the amplification H (x) l2: B(H) acts by left multiplication (a StarAlgHom, adjoint from hsInner = trace(A^dagger B)). Factor T = (V sqrt|T|) sqrt|T| so tr(aT) = <X, aY>_HS; positivity gives phi(a*a) = re<aX, aY> <= ||a (X+Y)/2||^2, then a Radon-Nikodym lemma gives phi = <Z, aZ>_HS = tr(a Z Z*). For the Radon-Nikodym lemma, Mathlib's PositiveLinearMap.GNS (GelfandNaimarkSegal.lean) plus LinearMap.extendOfNorm (Operator/Extend.lean) do most of the work: extend a S -> GNS, a zeta -> [a] from the dense range to the closure U, compose with U.orthogonalProjectionOnto, and take h = V^dagger V; commutation with pi(S) follows from P pi(c) = pi(c) P and a two-variable closure argument (Set.EqOn.closure + closure_prod_eq). Apply it to a Hahn-Banach positive extension of phi to B(H), since GNS needs a positive map on the whole C*-algebra.