Wigner uniqueness: the inducing (anti)unitary is unique up to phase

Category: 1-Mathlib (CSD-free Mathlib upstream candidate).

The uniqueness clause of the classical Wigner/Bargmann theorem, in the vocabulary of wigner_rigidity's own conclusion (projMap of a ≃ₗᵢ[ℂ], antiunitary branch through conjProj):

• Projectivization.exists_unit_smul_of_projMap_eq — two linear isometry equivalences with the same projective action differ by a global unit-modulus phase: e₂ = c • e₁ pointwise with ‖c‖ = 1 (any complex inner-product space, subsingleton case included).
• Projectivization.conjProj_conjProj — conjProj is an involution on ℂℙ^{N-1} (hence surjective).
• Projectivization.exists_unit_smul_of_projMap_conjProj_eq — the antiunitary twin: two inducers of the same antiunitary ray map (projMap e ∘ conjProj) differ by a global unit-modulus phase.

Together with wigner_rigidity (existence) and the branch-exclusivity facts (conjProj_ne_projMap / smul_action_not_antiunitary, Empirical/CSD/Gates/WignerDischarge.lean; Bargmann discriminator, Projectivization/Bargmann.lean), this completes the classical statement: every transition-probability-preserving map is induced by a unitary or antiunitary operator, unique up to a global phase within its branch.

The matrix-vocabulary sibling (two Matrix.unitaryGroup elements with the same ray action differ by a phase — the kernel of U(N) → PU(N) is the circle) predates this module: Projectivization.exists_unit_smul_of_smul_eq_smul (PhaseRigidity.lean, built for the W5-S1 phase lift). This module proves the ≃ₗᵢ-vocabulary form directly (same homothety engine, LinearMap.exists_eq_smul_id_of_forall_notLinearIndependent) rather than transporting through matrices, because projMap is what wigner_rigidity outputs and the isometry route needs no unitary star-algebra.

Provenance: CL-024 audit follow-up (2026-08-06) — the audit named up-to-phase uniqueness as the formalization gap against the reference; the matrix form turned out to already exist in PhaseRigidity.lean, and this module closes the remaining vocabulary gap. See specs/audit-sweep-plan.md (intake) and specs/BACKLOG.md G11.

Uniqueness up to phase, projMap vocabulary

theorem Projectivization.exists_unit_smul_of_projMap_eq {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e₁ e₂ : E ≃ₗᵢ[ℂ] E) (h : ∀ (p : Projectivization ℂ E), projMap e₁ p = projMap e₂ p) : ∃ (c : ℂ), ‖c‖ = 1 ∧ ∀ (v : E), e₂ v = c • e₁ v

Wigner uniqueness (unitary branch). Two linear isometry equivalences inducing the same projective self-map are equal up to a global unit-modulus phase: e₂ = c • e₁ pointwise with ‖c‖ = 1. Route: e₂ ∘ e₁⁻¹ fixes every ray, so every vector is an eigenvector of the composite; by the homothety lemma it is c • id, and the isometry property pins ‖c‖ = 1.

The antiunitary branch

theorem Projectivization.conjVec_conjVec {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) : conjVec (conjVec ψ) = ψ

conjVec is an involution: coordinatewise double conjugation is the identity.

theorem Projectivization.conjProj_conjProj {N : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : p.conjProj.conjProj = p

conjProj is an involution on ℂℙ^{N-1}: conjugating the ray twice returns the ray (hence conjProj is surjective — the fact the antiunitary uniqueness reduction needs).

theorem Projectivization.exists_unit_smul_of_projMap_conjProj_eq {N : ℕ} (e₁ e₂ : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) (h : ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), projMap e₁ p.conjProj = projMap e₂ p.conjProj) : ∃ (c : ℂ), ‖c‖ = 1 ∧ ∀ (v : EuclideanSpace ℂ (Fin N)), e₂ v = c • e₁ v

Wigner uniqueness (antiunitary branch). Two linear isometry equivalences inducing the same antiunitary ray map (projMap e ∘ conjProj, the shape of wigner_rigidity's second disjunct) are equal up to a global unit-modulus phase. Reduces to the unitary branch through the involutivity of conjProj.