| -- Step 1: From fixed-point equation, isolate φ⁻¹ · U ρ* Uᴴ | |
| have step1 : φ_inv • (U * ρ_star * star U) = (1 - φ_inv_sq) • ρ_star := by | |
| have key : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star = ρ_star := h_fp | |
| have sum1 : φ_inv + φ_inv_sq = 1 := phi_sum_one | |
| rw [← sum1, add_smul] at key | |
| have eq : φ_inv • (U * ρ_star * star U) + φ_inv_sq • ρ_star = | |
| φ_inv • ρ_star + φ_inv_sq • ρ_star := key | |
| have h1 : φ_inv • (U * ρ_star * star U) = φ_inv • ρ_star := by linarith | |
| rw [show (1 : ℂ) - φ_inv_sq = φ_inv by linarith [sum1]] | |
| exact h1 | |