Lean: define the trace of a positive operator as ‖√A‖²_HS to get basis independence free

For A ≥ 0 on a complex Hilbert space, ⟪A e, e⟫ = ‖√A e‖². So define posTrace A := hsNormSq (CFC.sqrt A), where the squared HS norm ∑ ‖S eᵢ‖ₑ² is already known to be basis-independent. Then posTrace_eq b (= ∑ ofReal (re ⟪A (b i), b i⟫) for every basis b) is a 3-line congr. The key step is ‖S e‖² = re⟪(S*S) e, e⟫ for self-adjoint S: take apply_norm_sq_eq_inner_adjoint_left and rewrite ← star_eq_adjoint, hS.star_eq. Then use CFC.sqrt_mul_sqrt_self. For trace class ⇒ HS: ‖B e‖² ≤ ‖B‖⟪Be,e⟫ for B ≥ 0, using B = √B√B and CFC.norm_sqrt. Note that CFC.norm_sqrt needs the extra import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Isometric. Also ‖|T|‖ = ‖T‖ is CFC.norm_abs.