Phase invariance of rank-1 outer products and wrappers

Category: 3-Local (pre-LF4 plan Phase 1 — phase invariance of outerProduct, rankOneEffect, and rankOneDensity under unit-modulus scalar action).

For a unit-modulus scalar c, the rank-1 outer product |c·φ⟩⟨c·φ| equals |φ⟩⟨φ|. The rank-1 projector through a unit vector depends only on the projective ray of the vector, not on its specific unit-vector representative.

Used downstream by the volume-ratio effect function effectProjFn (pre-LF4 plan Phase 2) to justify well-definedness under a caller- supplied phase-arbitrary rep : P → EuclideanSpace ℂ (Fin N) map.

theorem CSD.LF2.outerProduct_phase_invariant {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (c : ℂ) (hc : ‖c‖ = 1) : outerProduct (c • φ) = outerProduct φ

Phase invariance of outerProduct. For a unit-modulus scalar c and any vector φ, the outer product of c • φ equals the outer product of φ. Algebraic content: (c • φ) ⊗ (c • φ)* = c · c̄ · (φ ⊗ φ*) = ‖c‖² · (φ ⊗ φ*) = φ ⊗ φ*.

theorem CSD.LF2.rankOneEffect_phase_invariant {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (c : ℂ) (hc : ‖c‖ = 1) (hφ : ‖φ‖ = 1) (hcφ : ‖c • φ‖ = 1) : rankOneEffect (c • φ) hcφ = rankOneEffect φ hφ

Phase invariance of rankOneEffect. For a unit-modulus scalar c, rankOneEffect (c • φ) = rankOneEffect φ under matching unit-norm hypotheses. The rank-1 effect depends only on the projective ray of φ.

theorem CSD.LF2.rankOneDensity_phase_invariant {N : ℕ} (φ : EuclideanSpace ℂ (Fin N)) (c : ℂ) (hc : ‖c‖ = 1) (hφ : ‖φ‖ = 1) (hcφ : ‖c • φ‖ = 1) : rankOneDensity (c • φ) hcφ = rankOneDensity φ hφ

Phase invariance of rankOneDensity. For a unit-modulus scalar c, rankOneDensity (c • φ) = rankOneDensity φ under matching unit-norm hypotheses. The rank-1 density depends only on the projective ray of φ.