Conditional expectation in a tracial vN algebra from Radon–Nikodym plus M' = JMJ

To get E_N : M → N with τ(x y) = τ(E(x) y) for y ∈ N (tracial (M,τ), N ⊆ M a vN subalgebra), you never need the Jones projection or L²(M). Work in L²(N, τ|N). For x ≥ 0, ψ(y) = τ(x y) is positive on N (τ(x s s) = τ(s x s), s = √y), and ψ(y⋆y) ≤ ‖x‖ τ(y⋆y) is the vector state of ‖x‖^{1/2} Ω. Radon–Nikodym gives h ≥ 0 commuting with π(N) and ψ(b⋆a) = ⟪π b ζ, h π a ζ⟫. The commutant theorem π(N)' = ρ(N) makes h = ρ(k), and then τ(x y) = ‖x‖ τ(y k). Extend to all x by CStarAlgebra.span_nonneg + Submodule.span_le on the submodule {x | ∃ k, ...}. Uniqueness, linearity and bimodularity follow from faithfulness by taking y = (k − k')⋆. Lean gotcha: inside such proofs rw [map_mul] tries to match f (x * y) with the functional f and fails on MulHomClass. Write map_mul (inclusion hNM) explicitly.