Step (1) of the Wigner / Fubini–Study rigidity converse

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

Glossary: https://glossary.constraintsurfacedynamics.com/wigner-rigidity/ Plain-language, CSD-role and formal statements of Wigner rigidity, with this module as its Lean anchor. Kept symmetric by scripts/check-glossary.sh. On upstreaming: this is a Category 1 file. Strip this Glossary block before any Mathlib or Physlib PR; a personal project link has no place in a canonical header.

This file builds STEP (1) of the Wigner / Fubini–Study rigidity converse on top of the transition-probability foundation (Mathlib/LinearAlgebra/Projectivization/TransitionProbability.lean). It delivers:

• TransProbPreserving f — the predicate that a self-map f : ℙ ℂ E → ℙ ℂ E preserves the transition probability transProb;
• TransProbPreserving.injective — such a map is injective (a transition probability 1 forces coincidence, via transProb_self and transProb_eq_one_iff);
• transProbPreserving_unitary — the realisability inclusion: every unitary in Matrix.unitaryGroup (Fin N) ℂ, acting on ℂℙ^{N-1}, is TransProbPreserving. This is the U(N) → TransProbPreserving map whose surjectivity-up-to-phase is the deferred Wigner statement;
• TransProbPreserving.orthogonal / .inner_rep_eq_zero_iff — preservation of orthogonality, both as a transProb = 0 face and an inner = 0 face;
• TransProbPreserving.pairwise_orthogonal and orthonormalBasis_pairwise_orthogonal — the "orthonormal frame ↦ pairwise orthogonal family" content: an orthonormal basis induces a pairwise-orthogonal projective family, and a TransProbPreserving map sends it to one.

Steps (2a) and (2b) (proved here): image frame and candidate unitary

• (2a) The image orthonormal frame. imageVec is the unit-normalised canonical representative of the image ray f (mk (b i)); imageVec_norm, imageVec_ne_zero, and imageVec_orthonormal (off-diagonals transported from the source frame through TransProbPreserving.inner_rep_eq_zero_iff) make it an orthonormal family, packaged as imageOrthonormalBasis (an orthonormal family of cardinality N in EuclideanSpace ℂ (Fin N), finrank = N, spans). mk_imageOrthonormalBasis records that the i-th image ONB vector spans the image ray: mk (imageOrthonormalBasis i) = f (mk (b i)).
• (2b) The candidate unitary. candidateUnitary hf b is the OrthonormalBasis.equiv change of frame b ↦ imageOrthonormalBasis hf b along the identity reindexing of Fin N, a genuine ≃ₗᵢ[ℂ]. The headline candidateUnitary_agrees_on_basis is the agreement on the basis points: mk (candidateUnitary hf b (b i)) = f (mk (b i)) for every i.

Step (2c) frame reduction (proved here): the reduced map fixes the basis

• The projective image of an isometry equiv. projMap e is the Projectivization.map of a linear isometry equivalence e's underlying injective linear map. It preserves the transition probability (transProb_projMap, via the vector-level transProbVec_linearIsometryEquiv from e.inner_map_map and e.norm_map), hence is TransProbPreserving (projMap_transProbPreserving). TransProbPreserving.comp gives closure of the predicate under composition. (All general in E.)
• The frame-reduced map. reducedMap hf b := projMap (candidateUnitary hf b).symm ∘ f is TransProbPreserving (reducedMap_transProbPreserving) and fixes every source basis ray (reducedMap_fixes_basis): reducedMap hf b (mk (b i)) = mk (b i) for every i. The proof rewrites f (mk (b i)) backward via candidateUnitary_agrees_on_basis, pushes the inverse candidate unitary's projective map through projMap_mk, and applies LinearIsometryEquiv.symm_apply_apply.

This reduces the open converse to the Wigner normal-form problem for the reduced map, addressed in Stages 1–3 below.

Stage 1 (proved here): moduli preservation

• TransProbPreserving.transProb_of_fixed — a preserving map fixing a point q preserves the transition probability from every point to q.
• transProb_srcPoint — the transition probability to the i-th basis ray is the normalised squared modulus of the i-th coordinate b.repr ψ i.
• reducedMap_coord_modulus — Stage 1 headline: writing reducedMap hf b (mk ψ) = mk φ, the modulus profile ‖b.repr φ i‖² / ‖φ‖² = ‖b.repr ψ i‖² / ‖ψ‖² is preserved coordinate-by-coordinate.

Stage 2 (proved here): the two-level phase normal form

• add_basis_ne_zero, repr_eq_pair_of_support, mk_eq_two_level_of_profile — support and reconstruction infrastructure.
• reducedMap_two_level_normal_form — Stage 2 headline: for distinct i₀ ≠ i, reducedMap hf b (mk (b i₀ + b i)) = mk (b i₀ + ε • b i) for a unimodular ε. The image ray is pinned up to the single phase ε.

Both stages are derived from TransProbPreserving alone; no ℂ-linearity is assumed anywhere.

The antiunitary witness (proved here): conjProj

conjProj is coordinatewise complex conjugation as a ray map (conjVec on representatives), a concrete TransProbPreserving inhabitant (conjProj_transProbPreserving) of the antiunitary class: conjVec is conjugate-linear (conjVec_smul : conjVec (c • ψ) = conj c • conjVec ψ), not the underlying map of any ≃ₗᵢ[ℂ]. This makes the eventual dichotomy non-vacuous on the antiunitary side. Built on the conjugation inner/norm identities conjVec_inner : ⟪conjVec u, conjVec v⟫ = conj ⟪u, v⟫ and conjVec_norm : ‖conjVec ψ‖ = ‖ψ‖.

Stage 3 piece 1 (proved here): the diagonal-phase reduction

diagUnitary b ε hε is the diagonal-in-b isometry with unit-modulus phases ε (via the ε-scaled orthonormal basis, scaledBasis); twoLevelPhase extracts the Stage-2 phases anchored at ε i₀ := 1; and diagReducedMap hf b i₀ := projMap D⁻¹ ∘ reducedMap hf b (with D built from those phases) is TransProbPreserving (diagReducedMap_transProbPreserving), fixes every basis ray (diagReducedMap_fixes_basis), and fixes the two-level rays mk (b i₀ + b i) for every i ≠ i₀ (diagReducedMap_fixes_two_level). This is the setup the cocycle step (pieces 2–3) consumes. D is constructed from the extracted phases, not posited of f: no ℂ-linearity is assumed.

Stage 3 piece 2 (proved here): the cocycle coboundary structure

On the diagonally reduced map g := diagReducedMap hf b i₀ the coordinate overlap algebra pins the pairwise relative phases up to sign:

• diagReducedMap_coord_modulus — Stage-1 moduli transported to g.
• diagReducedMap_two_level_relphase — the anchored real-part relation Re(d̄_{i₀} d_i)/‖φ‖² = Re(c̄_{i₀} c_i)/‖ψ‖².
• diagReducedMap_fixes_three_level (W4) — the equal triple ray mk (b i₀ + b i + b j) is fixed, via moduli + saturation (norm_eq_re_imp_eq, eq_of_re_conj_mul_eq) + repr_eq_triple_of_support.
• diagReducedMap_fixes_two_level_general (W4) — the non-anchored ray mk (b i + b j) (i, j ≠ i₀) is fixed, using the triple as a probe.
• diagReducedMap_pairwise_relphase (W4) — the unconditional pairwise real-part relation for all i, j ≠ i₀, the full coboundary structure.

Every probe is real-coordinate, so the fixings are consistent with both the unitary and antiunitary branches: piece 2 establishes the coboundary structure, not the global sign (that is piece 3). No ℂ-linearity is assumed.

Stage 3 piece 3 (W5, proved here): complex probe, reconstruction, dichotomy

The converse of the realisability inclusion transProbPreserving_unitary is the Wigner / Fubini–Study rigidity theorem:

theorem (informal): TransProbPreserving f → (∃ U : Matrix.unitaryGroup (Fin N) ℂ, f = fun p => U • p) ∨ (∃ antiunitary A, f = A-ray-action)

equivalently, the isometry group of ℂℙⁿ with the Fubini–Study metric is the projective semi-unitary group. It is not stated here as an axiom or a sorry.

Scope note (CL-024 audit, 2026-08-06; updated same day). This module proves the EXISTENCE clause of the Wigner/Bargmann theorem. The up-to-phase uniqueness clause is formalized in companion modules: matrix vocabulary in PhaseRigidity.lean (exists_unit_smul_of_smul_eq_smul, the U(N) → PU(N) circle kernel — predating the audit, which missed it) and this theorem's own projMap/conjProj vocabulary in WignerUniqueness.lean (exists_unit_smul_of_projMap_eq, exists_unit_smul_of_projMap_conjProj_eq, via the involution conjProj_conjProj). The branch-EXCLUSIVITY facts (a map cannot be both unitary- and antiunitary-induced, 2 ≤ N) live downstream: Projectivization.conjProj_ne_projMap / smul_action_not_antiunitary (Empirical/CSD/Gates/WignerDischarge.lean) and the Bargmann-invariant discriminator (Projectivization/Bargmann.lean, LF4/BargmannSelection.lean). Cite those modules, not this one, for uniqueness/exclusivity claims. Piece 3 (W5) delivers the branch-distinguishing machinery:

• two_level_imrelphase_of_fixes / _flips — the complex I-probe pins the imaginary part of the relative phase, the datum the real probes of pieces 1–2 could not reach (fixed complex ray ⟹ Im preserved; flipped ⟹ Im negated).
• eq_id_of_fixes_all_two_level / eq_bconj_of_flips_complex — the two reconstruction directions: a map fixing all basis + real + complex two-level rays is the identity on rays; one that flips the complex rays is coordinatewise conjugation in b (bConjVec). ℂ-linearity is an OUTPUT.
• diagReducedMap_complex_probe — the complex probe ray mk (b i₀ + I • b i) is not conjugation-invariant, so the diagonally reduced map sends it to itself (+) or to mk (b i₀ − I • b i) (−): the per-pair ± I branch datum.
• diagReducedMap_dichotomy_of_complexSign — the assembly: given the global complex-sign closure (all complex two-level rays fixed, or all flipped), the reduced map is globally the identity, or globally bConjVec conjugation. Both branches genuine; the antiunitary branch is not dropped.

W6 (DONE). The unconditional wigner_rigidity is stated and proved here. The global-sign closure — the per-pair ± I datum is consistent across all pairs (fixes-all ∨ flips-all) — is discharged in diagReducedMap_complexSign_closure via the non-anchored per-pair dichotomy (diagReducedMap_complex_probe_general), the master witness masterVec, the abstract Gram-triple core sign_link_core, order swap by injectivity, and index linking; the unconditional diagReducedMap_dichotomy and the headline wigner_rigidity (unitary ∨ antiunitary, ℂ-linearity an output) follow, foundational-triple only. See the Stage 3 complete (W6) section at the end of this file. Scope of "piece 2 CLOSED" (load-bearing): piece 2 delivers the sign-free real-part relations — the full pairwise data Re(conj dᵢ·dⱼ)/‖φ‖² = Re(conj cᵢ·cⱼ)/‖ψ‖² (equivalently the pairwise cosines cos(βⱼ−βᵢ)=cos(αⱼ−αᵢ)) for every pair, which pin the phase configuration up to global rotation AND a single global reflection. The phrases "2-cocycle"/"coboundary structure" are narrative labels: no formal Complex.arg-based additive identity θ(i,j)=θ(i₀,j)−θ(i₀,i) or H² object is constructed, because extracting one presupposes choosing an arg branch — i.e. resolving the ± reflection — which is precisely piece 3. Critical honesty notes (load-bearing).

• reducedMap_fixes_basis does not make reducedMap the identity: the diagonal-phase freedom is genuine and is exactly the Stage-2 phase ε, pinned only by the Stage-3 cocycle. Do not read frame reduction as reducedMap = id nor as f = projMap (candidateUnitary hf b).
• Transition-probability preservation over ℂ admits both the unitary and the antiunitary classes; the holomorphic / Kähler complex structure selects the unitary one. Stage 3 must derive ℂ-linearity from the overlap data, not assume it: a smuggled linearity hypothesis would beg the question.

Provenance

Staged as upstream Mathlib material. All declarations live under namespace Projectivization with no CsdLean4-namespace prefix; the CsdLean4/Mathlib/... location is the only staging signal. Intended location: Mathlib/LinearAlgebra/Projectivization/WignerRigidity.lean.

Tags

projectivization, transition probability, Fubini-Study, Wigner theorem, unitary group, complex projective space, isometry, orthogonality

Diagonal value of the projective transition probability

theorem Projectivization.transProb_self {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p : Projectivization ℂ E) : p.transProb p = 1

The diagonal value of the projective transition probability is 1: any projective point coincides with itself. Reduces to transProbVec_self on the (nonzero) canonical representative via transProb_mk.

The transition-probability-preserving predicate

def Projectivization.TransProbPreserving {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (f : Projectivization ℂ E → Projectivization ℂ E) : Prop

A self-map of ℙ ℂ E is transition-probability preserving when it preserves transProb on every pair of projective points. The realisability direction transProbPreserving_unitary shows every unitary action is such a map; the converse (every such map is induced by a unitary) is the open Wigner target documented in the module header.

Equations

• Projectivization.TransProbPreserving f = ∀ (p q : Projectivization ℂ E), (f p).transProb (f q) = p.transProb q

Realisability inclusion: U(N) → TransProbPreserving

theorem Projectivization.TransProbPreserving.injective {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) : Function.Injective f

A transition-probability-preserving self-map of ℂℙ^{N-1} is injective: if f p = f q then transProb p q = transProb (f p) (f q) = transProb (f p) (f p) = 1, so p = q by transProb_eq_one_iff. (The coincidence characterisation transProb_eq_one_iff is the EuclideanSpace ℂ (Fin N) ingredient.)

theorem Projectivization.transProbPreserving_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : TransProbPreserving fun (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) => U • p

Realisability inclusion. Every unitary in Matrix.unitaryGroup (Fin N) ℂ, acting on ℂℙ^{N-1}, is transition-probability preserving. Immediate from transProb_smul_unitary. This is the U(N) → TransProbPreserving map; the surjectivity-up-to-phase of this map is the deferred Wigner statement.

The antiunitary witness conjProj

Over ℂ, transition-probability preservation admits a second class beyond the unitary one: the antiunitary class, realised by complex conjugation. This subsection builds it concretely. conjVec is coordinatewise complex conjugation on EuclideanSpace ℂ (Fin N), a conjugate-linear isometry (conjVec_smul shows the semilinear scaling law conjVec (c • ψ) = conj c • conjVec ψ, which is not the linear law of any ≃ₗᵢ[ℂ]). Its ray map conjProj is TransProbPreserving (conjProj_transProbPreserving), so the eventual Wigner dichotomy is not vacuous on the antiunitary side.

noncomputable def Projectivization.conjVec {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin N)

Coordinatewise complex conjugation on EuclideanSpace ℂ (Fin N): the conjugate-linear isometry ψ ↦ (fun i => conj (ψ i)).

Equations

• Projectivization.conjVec ψ = WithLp.toLp 2 fun (i : Fin N) => (starRingEnd ℂ) (ψ.ofLp i)

theorem Projectivization.conjVec_ofLp {N : ℕ} (ψ : EuclideanSpace ℂ (Fin N)) (i : Fin N) : (conjVec ψ).ofLp i = (starRingEnd ℂ) (ψ.ofLp i)

conjVec acts coordinatewise: (conjVec ψ) i = conj (ψ i) (definitional).

theorem Projectivization.conjVec_inner {N : ℕ} (u v : EuclideanSpace ℂ (Fin N)) : inner ℂ (conjVec u) (conjVec v) = (starRingEnd ℂ) (inner ℂ u v)

Conjugation inner identity. ⟪conjVec u, conjVec v⟫ = conj ⟪u, v⟫. Reduces via PiLp.inner_apply to the coordinatewise identity conj(conj (u i)) * conj (v i) = conj (conj (u i) * v i) (RCLike.inner_apply', map_mul, Complex.conj_conj).

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

Conjugation norm identity. ‖conjVec ψ‖ = ‖ψ‖. Both squared norms are the real part of the (conjugation-swapped) self inner product conjVec_inner; RCLike.conj_re drops the conjugation on the real part.

theorem Projectivization.conjVec_smul {N : ℕ} (c : ℂ) (ψ : EuclideanSpace ℂ (Fin N)) : conjVec (c • ψ) = (starRingEnd ℂ) c • conjVec ψ

Semilinearity of conjVec. conjVec (c • ψ) = conj c • conjVec ψ. This conjugate-linear scaling law witnesses that conjVec is genuinely antiunitary: it is not the linear scaling law satisfied by any ≃ₗᵢ[ℂ], so conjProj is not projMap of a complex-linear isometry equivalence.

theorem Projectivization.conjVec_ne_zero {N : ℕ} {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : conjVec ψ ≠ 0

conjVec preserves nonvanishing: ‖conjVec ψ‖ = ‖ψ‖ ≠ 0.

theorem Projectivization.conjVec_transProbVec {N : ℕ} (u v : EuclideanSpace ℂ (Fin N)) : transProbVec (conjVec u) (conjVec v) = transProbVec u v

Conjugation preserves the vector transition probability. transProbVec (conjVec u) (conjVec v) = transProbVec u v: the numerator is fixed since ‖conj ⟪u,v⟫‖ = ‖⟪u,v⟫‖ (conjVec_inner + RCLike.norm_conj), the denominator by conjVec_norm.

noncomputable def Projectivization.conjProj {N : ℕ} (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The antiunitary ray map: complex conjugation of the canonical representative. Total and well-defined (conjugation is norm-preserving and injective, so the image ray does not depend on representative choice up to the scaling conjVec_smul absorbs).

Equations

• p.conjProj = Projectivization.mk ℂ (Projectivization.conjVec p.rep) ⋯

theorem Projectivization.conjProj_transProbPreserving {N : ℕ} : TransProbPreserving conjProj

HEADLINE (antiunitary witness). conjProj is TransProbPreserving. Reduce both image rays to mk (conjVec ·.rep) via transProb_mk, then apply conjVec_transProbVec. This exhibits a concrete TransProbPreserving inhabitant of the antiunitary class: conjVec is conjugate-linear (conjVec_smul), not the underlying map of any ≃ₗᵢ[ℂ]; for 2 ≤ N the ray-level map conjProj is not projMap of any unitary (conjProj_ne_projMap, WignerDischarge — at N ≤ 1 the projective space has at most one point and the distinction vanishes). The eventual Wigner dichotomy is thus non-vacuous on the antiunitary side.

theorem Projectivization.conjProj_mk {N : ℕ} {v : EuclideanSpace ℂ (Fin N)} (hv : v ≠ 0) : (mk ℂ v hv).conjProj = mk ℂ (conjVec v) ⋯

Ray-map identity for conjProj on arbitrary representatives. conjProj (mk v hv) = mk (conjVec v). The canonical representative of mk v hv is a • v for some nonzero a; conjVec (a • v) = conj a • conjVec v (conjVec_smul), a nonzero rescaling, so both sides span the same ray. This is the representative-independent form of conjProj, needed for the eventual antiunitary assembly (Stage 3).

Orthogonality preservation

theorem Projectivization.transProb_mk_eq_zero_iff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {v w : E} (hv : v ≠ 0) (hw : w ≠ 0) : (mk ℂ v hv).transProb (mk ℂ w hw) = 0 ↔ inner ℂ v w = 0

mk-level orthogonality rewriter: for nonzero representatives v, w, the projective transition probability of mk v, mk w vanishes iff v ⟂ w. Routes through transProb_mk and the fact that the (positive) denominator of transProbVec is irrelevant to vanishing.

theorem Projectivization.TransProbPreserving.orthogonal {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {f : Projectivization ℂ E → Projectivization ℂ E} (hf : TransProbPreserving f) (p q : Projectivization ℂ E) : (f p).transProb (f q) = 0 ↔ p.transProb q = 0

Orthogonality preservation (transProb face). A transition-probability- preserving map preserves orthogonality of projective points (read as transProb = 0): the hypothesis rewrites the LHS to the RHS.

theorem Projectivization.TransProbPreserving.inner_rep_eq_zero_iff {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (p q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : inner ℂ (f p).rep (f q).rep = 0 ↔ inner ℂ p.rep q.rep = 0

Orthogonality preservation (inner-product face). A transition-probability- preserving self-map of ℂℙ^{N-1} preserves orthogonality of the canonical representatives. Combines .orthogonal with the orthogonality characterisation transProb_eq_zero_iff on both sides.

Orthogonal projective families and orthonormal frames

def Projectivization.Orthogonal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p q : Projectivization ℂ E) : Prop

Orthogonality of two projective points, read off the transition probability: Orthogonal p q means transProb p q = 0 (equivalently, the representatives are inner-product orthogonal).

Equations

• p.Orthogonal q = (p.transProb q = 0)

theorem Projectivization.TransProbPreserving.pairwise_orthogonal {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {f : Projectivization ℂ E → Projectivization ℂ E} (hf : TransProbPreserving f) {ι : Type u_3} {P : ι → Projectivization ℂ E} (h : Pairwise fun (i j : ι) => (P i).transProb (P j) = 0) : Pairwise fun (i j : ι) => (f (P i)).transProb (f (P j)) = 0

Orthogonal family preservation. A transition-probability-preserving map sends a pairwise-orthogonal projective family to a pairwise-orthogonal family. Pointwise consequence of .orthogonal.

theorem Projectivization.orthonormalBasis_pairwise_orthogonal {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : Pairwise fun (i j : Fin N) => (mk ℂ (b i) ⋯).transProb (mk ℂ (b j) ⋯) = 0

Orthonormal frame ↦ pairwise-orthogonal projective family. An orthonormal basis of EuclideanSpace ℂ (Fin N) induces a pairwise-orthogonal family of projective points (distinct basis rays are orthogonal). Uses b.orthonormal.2 (the off-diagonal vanishing of an Orthonormal family) and the mk-level rewriter transProb_mk_eq_zero_iff. Composing with TransProbPreserving.pairwise_orthogonal exhibits the "orthonormal frame ↦ pairwise-orthogonal family" content at the orthogonality level.

Step (2a): the image orthonormal frame

A TransProbPreserving map f together with a source orthonormal basis b produces an orthonormal family of image representatives, the unit-normalised canonical reps of the image rays f (mk (b i)). Pairwise orthogonality is transported from the source frame through inner_rep_eq_zero_iff; the diagonal is unit by construction. Indexed by Fin N in a space of finrank = N, the family is an orthonormal basis. Each image ONB vector spans the image ray: mk (imageOrthonormalBasis i) = f (mk (b i)).

noncomputable def Projectivization.srcPoint {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The i-th source basis projective point mk (b i). A definitional abbreviation kept folded inside the helper lemmas; the public headlines (mk_imageOrthonormalBasis, candidateUnitary_agrees_on_basis) restate it as the explicit mk ℂ (b i) (b.orthonormal.ne_zero i).

Equations

• Projectivization.srcPoint b i = Projectivization.mk ℂ (b i) ⋯

theorem Projectivization.srcPoint_eq {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : srcPoint b i = mk ℂ (b i) ⋯

srcPoint unfolds to the explicit mk of the basis vector.

noncomputable def Projectivization.imageVec {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (_hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : EuclideanSpace ℂ (Fin N)

The unit-normalised canonical representative of the image ray f (mk (b i)). Normalising the (nonzero) rep (f (srcPoint b i)).rep by the real reciprocal of its norm (cast to ℂ) gives a unit vector spanning the same ray.

Equations

• Projectivization.imageVec _hf b i = ↑‖(f (Projectivization.srcPoint b i)).rep‖⁻¹ • (f (Projectivization.srcPoint b i)).rep

theorem Projectivization.imageVec_scalar_ne_zero {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (_hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : ↑‖(f (srcPoint b i)).rep‖⁻¹ ≠ 0

The reciprocal-norm scalar in imageVec is nonzero (the rep is nonzero, so its norm is positive).

theorem Projectivization.imageVec_ne_zero {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : imageVec hf b i ≠ 0

imageVec is nonzero.

theorem Projectivization.imageVec_norm {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : ‖imageVec hf b i‖ = 1

imageVec has unit norm: the reciprocal-norm scaling normalises the rep.

theorem Projectivization.imageVec_orthonormal {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : Orthonormal ℂ (imageVec hf b)

The image family imageVec hf b is orthonormal. Off-diagonal: the source basis rays are orthogonal (orthonormalBasis_pairwise_orthogonal + transProb_eq_zero_iff on the canonical reps), inner_rep_eq_zero_iff hf transports this to the image reps, and the scalar normalisation factors pull out of inner leaving 0. Diagonal: imageVec_norm.

noncomputable def Projectivization.imageOrthonormalBasis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))

The image orthonormal family, packaged as an OrthonormalBasis (Fin N): an orthonormal family of cardinality N in EuclideanSpace ℂ (Fin N) (finrank = N) spans the whole space, so OrthonormalBasis.mk applies.

Equations

• Projectivization.imageOrthonormalBasis hf b = OrthonormalBasis.mk ⋯ ⋯

theorem Projectivization.imageOrthonormalBasis_apply {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : (imageOrthonormalBasis hf b) i = imageVec hf b i

imageOrthonormalBasis evaluates to imageVec (the OrthonormalBasis.mk apply lemma).

theorem Projectivization.mk_imageOrthonormalBasis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : mk ℂ ((imageOrthonormalBasis hf b) i) ⋯ = f (mk ℂ (b i) ⋯)

The image ONB vector's ray is the image ray. imageVec hf b i is a nonzero scalar multiple of (f (srcPoint b i)).rep, so mk (imageVec ..) equals mk ((f (srcPoint b i)).rep) = f (srcPoint b i) by the mk-scaling characterisation mk_eq_mk_iff' and mk_rep.

Step (2b): the candidate unitary

The candidate unitary is the OrthonormalBasis.equiv change-of-frame b ↦ imageOrthonormalBasis hf b along the identity reindexing. On the source basis vectors it reproduces the image ONB vectors, hence (via mk_imageOrthonormalBasis) agrees ray-by-ray with f on the basis points. This is the unitary candidate for the Wigner converse; the open content is extending the agreement off the basis (step (2c)) and ruling out the antiunitary branch (step (2d)).

noncomputable def Projectivization.candidateUnitary {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)

The candidate unitary: the linear isometry equivalence carrying the source orthonormal basis b to the image orthonormal basis along the identity reindexing of Fin N.

Equations

• Projectivization.candidateUnitary hf b = b.equiv (Projectivization.imageOrthonormalBasis hf b) (Equiv.refl (Fin N))

theorem Projectivization.candidateUnitary_apply_basis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : (candidateUnitary hf b) (b i) = (imageOrthonormalBasis hf b) i

The candidate unitary sends the i-th source basis vector to the i-th image ONB vector. From OrthonormalBasis.equiv_apply_basis and Equiv.refl_apply.

theorem Projectivization.candidateUnitary_agrees_on_basis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : mk ℂ ((candidateUnitary hf b) (b i)) ⋯ = f (mk ℂ (b i) ⋯)

Step (2b) headline. The candidate unitary agrees with f on the basis points: the ray spanned by candidateUnitary hf b (b i) is exactly the image ray f (mk (b i)). Composes candidateUnitary_apply_basis (the image ONB vector) with mk_imageOrthonormalBasis (its ray is the image ray).

Step (2c) frame reduction: projective image of an isometry equiv

The projective map projMap e of a linear isometry equivalence e preserves transProb (transProb_projMap), so it is TransProbPreserving (projMap_transProbPreserving). Composing f with the projective map of the inverse candidate unitary yields reducedMap, which is TransProbPreserving and fixes every basis ray (reducedMap_fixes_basis). This reduces the open converse step (2c) to the single Wigner normal-form lemma stated in the module header. These declarations are general in E wherever they do not consume the EuclideanSpace-specific candidateUnitary.

noncomputable def Projectivization.projMap {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) : Projectivization ℂ E → Projectivization ℂ E

The projective self-map induced by a linear isometry equivalence e: the Projectivization.map of e's underlying (injective) linear map.

Equations

• Projectivization.projMap e = Projectivization.map ↑e.toLinearEquiv ⋯

theorem Projectivization.projMap_mk {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) (v : E) (hv : v ≠ 0) : projMap e (mk ℂ v hv) = mk ℂ (e v) ⋯

projMap e sends mk v to mk (e v). The nonzero side is e v ≠ 0 from e.injective (an injective linear map is zero-preserving), packaged through Projectivization.map_mk.

@[simp]

theorem Projectivization.projMap_refl {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] : projMap (LinearIsometryEquiv.refl ℂ E) = id

projMap of the identity is the identity ray map.

theorem Projectivization.projMap_trans {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e₁ e₂ : E ≃ₗᵢ[ℂ] E) : projMap (e₁.trans e₂) = projMap e₂ ∘ projMap e₁

projMap is functorial: the ray map of a composite is the composite of the ray maps (trans composes left-to-right, so projMap e₂ applies second).

theorem Projectivization.transProbVec_linearIsometryEquiv {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) (u v : E) : transProbVec (e u) (e v) = transProbVec u v

Transition probability is invariant under a linear isometry equivalence (vector level). transProbVec (e u) (e v) = transProbVec u v: the numerator is fixed by e.inner_map_map, the denominator by e.norm_map.

theorem Projectivization.transProb_projMap {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) (p q : Projectivization ℂ E) : (projMap e p).transProb (projMap e q) = p.transProb q

projMap e preserves transProb (projective level). Reduce both points to mk of their canonical reps, push projMap through projMap_mk, collapse to transProbVec via transProb_mk, then apply transProbVec_linearIsometryEquiv.

theorem Projectivization.projMap_transProbPreserving {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) : TransProbPreserving (projMap e)

projMap e is TransProbPreserving. Immediate from transProb_projMap. General in E.

theorem Projectivization.TransProbPreserving.comp {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {g f : Projectivization ℂ E → Projectivization ℂ E} (hg : TransProbPreserving g) (hf : TransProbPreserving f) : TransProbPreserving fun (p : Projectivization ℂ E) => g (f p)

Composition of TransProbPreserving maps. g ∘ f preserves transProb when both g and f do. General in E.

Step (2c) frame reduction: the reduced map fixes every basis ray

reducedMap hf b := projMap (candidateUnitary hf b).symm ∘ f. It is TransProbPreserving and fixes every source basis ray, since on srcPoint b i the candidate unitary's projective map reproduces f's value (by candidateUnitary_agrees_on_basis) and its inverse returns to the basis ray.

noncomputable def Projectivization.reducedMap {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The frame-reduced map: post-compose f with the projective map of the inverse candidate unitary. Designed so that the basis rays become fixed points.

Equations

• Projectivization.reducedMap hf b p = Projectivization.projMap (Projectivization.candidateUnitary hf b).symm (f p)

theorem Projectivization.reducedMap_transProbPreserving {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : TransProbPreserving (reducedMap hf b)

reducedMap is TransProbPreserving. It is the composition projMap (candidateUnitary hf b).symm ∘ f; compose hf with projMap_transProbPreserving.

theorem Projectivization.reducedMap_fixes_basis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i : Fin N) : reducedMap hf b (mk ℂ (b i) ⋯) = mk ℂ (b i) ⋯

HEADLINE (frame reduction). The frame-reduced map fixes every source basis ray: reducedMap hf b (mk (b i)) = mk (b i).

Proof chain. Write U := candidateUnitary hf b. By definition reducedMap hf b (srcPoint b i) = projMap U.symm (f (srcPoint b i)). Rewrite f (srcPoint b i) backward via candidateUnitary_agrees_on_basis to mk (U (b i)); push projMap U.symm through projMap_mk to mk (U.symm (U (b i))); and U.symm (U (b i)) = b i by LinearIsometryEquiv.symm_apply_apply. mk is proof-irrelevant in its nonzero hypothesis, so the dependent nonzero proofs are immaterial.

Critical honesty note. Fixing the basis rays does not make reducedMap the identity: the diagonal-phase freedom is genuine and is exactly what the remaining normal-form lemma (step (2c)) must pin down. Do not read this as reducedMap = id or f = projMap (candidateUnitary hf b).

Stage 1: moduli preservation

A TransProbPreserving map fixing a projective point q preserves the transition probability from every point to q (TransProbPreserving.transProb_of_fixed). Applied to reducedMap hf b, which fixes every source basis ray, this shows the modulus profile of the coordinates in the basis b is preserved: writing reducedMap hf b (mk ψ) = mk φ, the normalised squared modulus ‖b.repr ψ i‖² / ‖ψ‖² of each coordinate is preserved (reducedMap_coord_modulus). This is the coordinate-free heart of the Wigner normal-form argument; it does not yet pin phases.

theorem Projectivization.TransProbPreserving.transProb_of_fixed {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {g : Projectivization ℂ E → Projectivization ℂ E} (hg : TransProbPreserving g) {q : Projectivization ℂ E} (hq : g q = q) (p : Projectivization ℂ E) : (g p).transProb q = p.transProb q

Moduli-preservation kernel. A transition-probability-preserving map fixing a projective point q preserves the transition probability from every point to q. General in E.

theorem Projectivization.transProb_srcPoint {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) (i : Fin N) : (mk ℂ ψ hψ).transProb (srcPoint b i) = ‖(b.repr ψ).ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

The transition probability from mk ψ to the i-th source basis ray srcPoint b i is the normalised squared modulus of the i-th coordinate b.repr ψ i. Uses norm_inner_symm and OrthonormalBasis.repr_apply_apply to identify ‖⟪ψ, b i⟫‖ = ‖b.repr ψ i‖, and Orthonormal.norm_eq_one to drop the unit basis norm from the denominator.

theorem Projectivization.reducedMap_coord_modulus {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) (i : Fin N) : ‖(b.repr (reducedMap hf b (mk ℂ ψ hψ)).rep).ofLp i‖ ^ 2 / ‖(reducedMap hf b (mk ℂ ψ hψ)).rep‖ ^ 2 = ‖(b.repr ψ).ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

Stage 1 (moduli preservation). Writing reducedMap hf b (mk ψ) = mk φ, the normalised squared modulus of every coordinate in the basis b is preserved: ‖b.repr φ i‖² / ‖φ‖² = ‖b.repr ψ i‖² / ‖ψ‖², where φ is the canonical representative of the image ray. Combines the moduli-preservation kernel TransProbPreserving.transProb_of_fixed (with q = srcPoint b i, fixed by reducedMap_fixes_basis) and the coordinate reading transProb_srcPoint.

Stage 2: the two-level phase normal form

For distinct indices i₀ ≠ i, the frame-reduced map sends the superposition ray mk (b i₀ + b i) to a ray mk (b i₀ + ε • b i) with ε unimodular (reducedMap_two_level_normal_form). Stage 1 forces the image rep to be supported on {i₀, i} with equal coordinate moduli there; normalising the ray so that the i₀-coordinate is 1 leaves a single unit phase ε := d_i / d_{i₀}. The genuine content is the support restriction plus the modulus equality; the phase ε is not yet pinned to 1 (that is Stage 3, the cocycle).

theorem Projectivization.add_basis_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i : Fin N} (hij : i₀ ≠ i) : b i₀ + b i ≠ 0

The sum of two distinct basis vectors is nonzero: its squared norm is 2 (Pythagoras via norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero, using the orthogonality b.orthonormal.2 hij and the unit norms).

theorem Projectivization.repr_eq_pair_of_support {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (φ : EuclideanSpace ℂ (Fin N)) {i₀ i : Fin N} (hij : i₀ ≠ i) (hsupp : ∀ (j : Fin N), j ≠ i₀ → j ≠ i → (b.repr φ).ofLp j = 0) : φ = (b.repr φ).ofLp i₀ • b i₀ + (b.repr φ).ofLp i • b i

Support reconstruction. A vector whose coordinates in the basis b vanish outside {i₀, i} is the pair sum of its two surviving coordinates. OrthonormalBasis.sum_repr expands φ, Finset.sum_subset drops the null coordinates, and Finset.sum_pair collapses the two-element sum.

theorem Projectivization.mk_eq_two_level_of_profile {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {φ : EuclideanSpace ℂ (Fin N)} (hφ : φ ≠ 0) {i₀ i : Fin N} (hij : i₀ ≠ i) (hsupp : ∀ (j : Fin N), j ≠ i₀ → j ≠ i → (b.repr φ).ofLp j = 0) (ha : (b.repr φ).ofLp i₀ ≠ 0) (hmod : ‖(b.repr φ).ofLp i‖ = ‖(b.repr φ).ofLp i₀‖) : ∃ (ε : ℂ) (hne : b i₀ + ε • b i ≠ 0), ‖ε‖ = 1 ∧ mk ℂ φ hφ = mk ℂ (b i₀ + ε • b i) hne

Profile ⇒ two-level normal form. A nonzero vector supported on {i₀, i} with equal coordinate moduli there (and nonzero i₀-coordinate) spans the ray mk (b i₀ + ε • b i) for the unit phase ε := (b.repr φ i) / (b.repr φ i₀). Factoring b.repr φ i₀ out of the pair reconstruction rescales the ray; the modulus equality gives ‖ε‖ = 1.

theorem Projectivization.reducedMap_two_level_normal_form {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i : Fin N} (hij : i₀ ≠ i) : ∃ (ε : ℂ) (hne : b i₀ + ε • b i ≠ 0), ‖ε‖ = 1 ∧ reducedMap hf b (mk ℂ (b i₀ + b i) ⋯) = mk ℂ (b i₀ + ε • b i) hne

Stage 2 (two-level phase normal form). For distinct i₀ ≠ i, the frame-reduced map sends the superposition ray mk (b i₀ + b i) to mk (b i₀ + ε • b i) for a unimodular ε. Stage 1 (reducedMap_coord_modulus) forces the image rep to be supported on {i₀, i} with equal moduli there; mk_eq_two_level_of_profile packages the ray normal form. This pins the image ray up to the single phase ε; pinning ε = 1 (globally coherently) is the Stage 3 cocycle, not proved here.

Stage 3 piece 1: the diagonal-phase reduction

The first piece of the Stage 3 residual, on the critical path to the dichotomy. It removes the Stage-2 two-level phases by post-composing the frame-reduced map g = reducedMap hf b with a diagonal isometry D⁻¹ in the basis b.

• The diagonal isometry. For a unit-modulus phase family ε : Fin N → ℂ (∀ i, ‖ε i‖ = 1), the scaled family fun i => ε i • b i is again an orthonormal basis (scaledBasis); diagUnitary b ε hε is the ≃ₗᵢ[ℂ] carrying b to it, so diagUnitary (b i) = ε i • b i (diagUnitary_apply_basis) and (diagUnitary).symm (b i) = (ε i)⁻¹ • b i (diagUnitary_symm_apply_basis). This is diagonal in the basis b, not in the standard basis, so it is built as an OrthonormalBasis.equiv, not a Matrix.diagonal.
• The extracted phases. twoLevelPhase hf b i₀ reads off, per index, the Stage-2 phase εᵢ from reducedMap_two_level_normal_form (anchored at ε i₀ := 1), with ‖twoLevelPhase hf b i₀ j‖ = 1 for every j (twoLevelPhase_norm).
• The diagonally-reduced map. diagReducedMap hf b i₀ := projMap (D).symm ∘ reducedMap hf b with D := diagUnitary b (twoLevelPhase hf b i₀) …. It is TransProbPreserving (diagReducedMap_transProbPreserving), still fixes every basis ray (diagReducedMap_fixes_basis), and additionally fixes the two-level rays mk (b i₀ + b i) for every i ≠ i₀ (diagReducedMap_fixes_two_level) — the setup the cocycle step (pieces 2–3) consumes. No ℂ-linearity is assumed: D is constructed from the extracted phases, not posited of f.

theorem Projectivization.scaled_orthonormal {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) : Orthonormal ℂ fun (i : Fin N) => ε i • b i

The scaled family fun i => ε i • b i is orthonormal when every phase is unit modulus (‖ε i‖ = 1): the off-diagonals inherit b's orthogonality, and the diagonal is conj (ε i) * ε i = ‖ε i‖² = 1 (RCLike.conj_mul).

theorem Projectivization.scaled_span {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) : ⊤ ≤ Submodule.span ℂ (Set.range fun (i : Fin N) => ε i • b i)

The ε-scaled family spans: cardinality N linearly independent vectors in finrank = N. Kept a separate Prop lemma so scaledBasis is a term-mode def (a tactic-mode data def would over-include ambient section variables).

noncomputable def Projectivization.scaledBasis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))

The ε-scaled orthonormal basis (an orthonormal family of cardinality N in finrank = N, so OrthonormalBasis.mk applies).

Equations

• Projectivization.scaledBasis b ε hε = OrthonormalBasis.mk ⋯ ⋯

theorem Projectivization.scaledBasis_apply {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) (i : Fin N) : (scaledBasis b ε hε) i = ε i • b i

scaledBasis evaluates to the scaled basis vector (OrthonormalBasis.mk apply).

noncomputable def Projectivization.diagUnitary {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)

The diagonal isometry in the basis b: the ≃ₗᵢ[ℂ] carrying b to the ε-scaled basis along the identity reindexing. Diagonal in b (diagUnitary (b i) = ε i • b i), unit modulus per coordinate.

Equations

• Projectivization.diagUnitary b ε hε = b.equiv (Projectivization.scaledBasis b ε hε) (Equiv.refl (Fin N))

theorem Projectivization.diagUnitary_apply_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) (i : Fin N) : (diagUnitary b ε hε) (b i) = ε i • b i

diagUnitary scales the i-th basis vector by ε i.

theorem Projectivization.diagUnitary_symm_apply_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ε : Fin N → ℂ) (hε : ∀ (i : Fin N), ‖ε i‖ = 1) (i : Fin N) : (diagUnitary b ε hε).symm (b i) = (ε i)⁻¹ • b i

The inverse diagUnitary scales the i-th basis vector by (ε i)⁻¹. diagUnitary ((ε i)⁻¹ • b i) = b i (since ε i ≠ 0), then symm_apply_apply.

noncomputable def Projectivization.twoLevelPhase {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ j : Fin N) : ℂ

The Stage-2 phase, extracted per index and anchored at ε i₀ := 1. For j ≠ i₀, twoLevelPhase hf b i₀ j is the unit phase εⱼ supplied by reducedMap_two_level_normal_form for the pair (i₀, j).

Equations

• Projectivization.twoLevelPhase hf b i₀ j = if h : j = i₀ then 1 else Classical.choose ⋯

theorem Projectivization.twoLevelPhase_self {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) : twoLevelPhase hf b i₀ i₀ = 1

The anchor phase is 1: twoLevelPhase hf b i₀ i₀ = 1.

theorem Projectivization.twoLevelPhase_norm {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ j : Fin N) : ‖twoLevelPhase hf b i₀ j‖ = 1

Every extracted phase is unit modulus: ‖twoLevelPhase hf b i₀ j‖ = 1 (anchor ‖1‖ = 1; off-anchor from the Stage-2 choose_spec).

noncomputable def Projectivization.diagReducedMap {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))

The diagonally-reduced map: projMap D⁻¹ ∘ reducedMap hf b, where D := diagUnitary b (twoLevelPhase hf b i₀) … is the diagonal isometry built from the extracted phases.

Equations

• Projectivization.diagReducedMap hf b i₀ p = Projectivization.projMap (Projectivization.diagUnitary b (Projectivization.twoLevelPhase hf b i₀) ⋯).symm (Projectivization.reducedMap hf b p)

theorem Projectivization.diagReducedMap_transProbPreserving {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) : TransProbPreserving (diagReducedMap hf b i₀)

diagReducedMap is TransProbPreserving. Composition of the preserving projMap D⁻¹ and the preserving reducedMap hf b.

theorem Projectivization.diagReducedMap_fixes_basis {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ i : Fin N) : diagReducedMap hf b i₀ (mk ℂ (b i) ⋯) = mk ℂ (b i) ⋯

diagReducedMap still fixes every basis ray. reducedMap fixes mk (b i), then projMap D⁻¹ sends it to mk ((ε i)⁻¹ • b i) = mk (b i) (scaling invariance).

theorem Projectivization.diagReducedMap_fixes_two_level {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i : Fin N} (hij : i₀ ≠ i) : diagReducedMap hf b i₀ (mk ℂ (b i₀ + b i) ⋯) = mk ℂ (b i₀ + b i) ⋯

HEADLINE (diagonal-phase reduction). The diagonally-reduced map fixes the two-level superposition ray mk (b i₀ + b i) for every i ≠ i₀.

Proof. Stage 2 (reducedMap_two_level_normal_form, extracted through twoLevelPhase) gives reducedMap hf b (mk (b i₀ + b i)) = mk (b i₀ + c • b i) with c := twoLevelPhase hf b i₀ i unit modulus. Applying D⁻¹: D⁻¹ (b i₀) = (ε i₀)⁻¹ • b i₀ = b i₀ (anchor ε i₀ = 1) and D⁻¹ (b i) = c⁻¹ • b i, so D⁻¹ (b i₀ + c • b i) = b i₀ + (c c⁻¹) • b i = b i₀ + b i. Hence the ray is fixed. This is the setup consumed by the cocycle step (pieces 2–3): a TransProbPreserving map fixing every basis ray and every two-level ray mk (b i₀ + b i). No ℂ-linearity assumed.

Stage 3 piece 2: coordinate moduli, the two-level relative phase, cocycle datum

Piece 2 of the Stage-3 residual, the derivation-heavy core, built on the diagonally reduced map h := diagReducedMap hf b i₀ (TransProbPreserving, fixing every basis ray and every anchored two-level ray mk (b i₀ + b i)). Writing h (mk ψ) = mk φ, cⱼ := b.repr ψ j, dⱼ := b.repr φ j:

• Moduli (coord_modulus_of_fixes_basis, diagReducedMap_coord_modulus): ‖dⱼ‖² / ‖φ‖² = ‖cⱼ‖² / ‖ψ‖², for any TransProbPreserving map fixing the basis rays.
• Two-level relative phase (two_level_relphase_of_fixes, diagReducedMap_two_level_relphase) — the heart of piece 2: Re(d̄_{i₀} d_i) / ‖φ‖² = Re(c̄_{i₀} c_i) / ‖ψ‖², i.e. arg(d_i / d_{i₀}) = ± arg(c_i / c_{i₀}). The overlap fixes only the real part; the sign of the imaginary part — the cocycle's ℤ/2 datum — stays free.
• Conditional pairwise relation (diagReducedMap_pairwise_relphase_of_fixed): for any pair (i, j) whose two-level ray is fixed by h, the analogous relation Re(d̄_i d_j) / ‖φ‖² = Re(c̄_i c_j) / ‖ψ‖² holds.

No ℂ-linearity of f/h is used anywhere below: every relation comes from the transProb/transProbVec overlap algebra, the fixed-point content of diagReducedMap, and the moduli. The precise residual is documented after the lemmas and in the Stage 3 (residual) section.

theorem Projectivization.cnorm_add_sq (A B : ℂ) : ‖A + B‖ ^ 2 = ‖A‖ ^ 2 + ‖B‖ ^ 2 + 2 * ((starRingEnd ℂ) A * B).re

Complex parallelogram expansion. For A B : ℂ, ‖A + B‖² = ‖A‖² + ‖B‖² + 2·Re(conj A · B). Via Complex.normSq_add and Complex.normSq_eq_norm_sq; (A · conj B).re = (conj A · B).re since re is conjugation-invariant.

theorem Projectivization.inner_eq_conj_repr {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (j : Fin N) : inner ℂ ψ (b j) = (starRingEnd ℂ) ((b.repr ψ).ofLp j)

The inner product of ψ with a basis vector is the conjugate of the corresponding coordinate: ⟪ψ, b j⟫ = conj (b.repr ψ j). From OrthonormalBasis.repr_apply_apply (b.repr ψ j = ⟪b j, ψ⟫) and inner_conj_symm.

theorem Projectivization.inner_add_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (i₀ i : Fin N) : inner ℂ ψ (b i₀ + b i) = (starRingEnd ℂ) ((b.repr ψ).ofLp i₀ + (b.repr ψ).ofLp i)

The inner product of ψ with a two-level basis sum unfolds to the conjugate of the coordinate sum: ⟪ψ, b i₀ + b i⟫ = conj (b.repr ψ i₀ + b.repr ψ i).

theorem Projectivization.add_basis_norm_sq {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i : Fin N} (hij : i₀ ≠ i) : ‖b i₀ + b i‖ ^ 2 = 2

The squared norm of a two-level basis sum is 2 (Pythagoras via norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero and the unit norms).

theorem Projectivization.transProb_two_level {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) {i₀ i : Fin N} (hij : i₀ ≠ i) : (mk ℂ ψ hψ).transProb (mk ℂ (b i₀ + b i) ⋯) = ‖(b.repr ψ).ofLp i₀ + (b.repr ψ).ofLp i‖ ^ 2 / (‖ψ‖ ^ 2 * 2)

Two-level overlap in coordinates. The transition probability from mk ψ to the two-level ray mk (b i₀ + b i) is ‖b.repr ψ i₀ + b.repr ψ i‖² / (‖ψ‖² · 2). Combines transProb_mk, inner_add_basis (the numerator), RCLike.norm_conj, and add_basis_norm_sq (the denominator's ‖b i₀ + b i‖² = 2).

theorem Projectivization.coord_modulus_of_fixes_basis {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (j : Fin N), g (srcPoint b j) = srcPoint b j) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) (i : Fin N) : ‖(b.repr (g (mk ℂ ψ hψ)).rep).ofLp i‖ ^ 2 / ‖(g (mk ℂ ψ hψ)).rep‖ ^ 2 = ‖(b.repr ψ).ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

Moduli preservation for a basis-fixing preserver. Any TransProbPreserving map g that fixes every source basis ray preserves the normalised squared modulus of every coordinate: ‖b.repr (g (mk ψ)).rep i‖² / ‖(g (mk ψ)).rep‖² = ‖b.repr ψ i‖² / ‖ψ‖². Generalises reducedMap_coord_modulus off reducedMap to an abstract g; the proof is the same transProb_of_fixed + transProb_srcPoint composition.

theorem Projectivization.two_level_relphase_of_fixes {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (j : Fin N), g (srcPoint b j) = srcPoint b j) {i₀ i : Fin N} (hij : i₀ ≠ i) (hfix2 : g (mk ℂ (b i₀ + b i) ⋯) = mk ℂ (b i₀ + b i) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (g (mk ℂ ψ hψ)).rep).ofLp i₀) * (b.repr (g (mk ℂ ψ hψ)).rep).ofLp i).re / ‖(g (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i₀) * (b.repr ψ).ofLp i).re / ‖ψ‖ ^ 2

Two-level relative-phase constraint (general). Let g be TransProbPreserving, fixing every basis ray and the two-level ray mk (b i₀ + b i). Writing g (mk ψ) = mk φ, the real part of the relative phase between the i₀- and i-coordinates is preserved: Re(conj d_{i₀} · d_i) / ‖φ‖² = Re(conj c_{i₀} · c_i) / ‖ψ‖², with cⱼ = b.repr ψ j, dⱼ = b.repr φ j.

Proof. The two-level overlap transProb (g (mk ψ)) (mk (b i₀ + b i)) equals transProb (mk ψ) (mk (b i₀ + b i)) because g fixes the two-level ray (transProb_of_fixed); transProb_two_level reads both as ‖·₀ + ·ᵢ‖² / (‖·‖² · 2). Cross-multiplying and expanding the numerators with cnorm_add_sq leaves, after cancelling the modulus terms via coord_modulus_of_fixes_basis, exactly the real-part relation.

No linearity is used: this is pure overlap algebra. The imaginary part of conj d_{i₀} · d_i — the sign of the relative phase, the cocycle's ℤ/2 datum — is not pinned, and the result holds for both the unitary (d = c) and antiunitary (d = conj c) branches.

theorem Projectivization.diagReducedMap_coord_modulus {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) (i : Fin N) : ‖(b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i‖ ^ 2 / ‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2 = ‖(b.repr ψ).ofLp i‖ ^ 2 / ‖ψ‖ ^ 2

Moduli preservation for the diagonally reduced map. Instance of coord_modulus_of_fixes_basis for diagReducedMap hf b i₀.

theorem Projectivization.diagReducedMap_two_level_relphase {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i : Fin N} (hij : i₀ ≠ i) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i₀) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i).re / ‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i₀) * (b.repr ψ).ofLp i).re / ‖ψ‖ ^ 2

HEADLINE (two-level relative phase, the heart of piece 2). The diagonally reduced map diagReducedMap hf b i₀ preserves the real part of the relative phase between the anchor coordinate i₀ and any coordinate i ≠ i₀: Re(conj d_{i₀} · d_i) / ‖φ‖² = Re(conj c_{i₀} · c_i) / ‖ψ‖², i.e. arg(d_i / d_{i₀}) = ± arg(c_i / c_{i₀}). Instance of two_level_relphase_of_fixes with the basis fixing (diagReducedMap_fixes_basis) and the anchored two-level fixing (diagReducedMap_fixes_two_level). The ± sign is genuinely free (only the real part is pinned) and no ℂ-linearity is assumed.

theorem Projectivization.diagReducedMap_pairwise_relphase_of_fixed {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) (hfix : diagReducedMap hf b i₀ (mk ℂ (b i + b j) ⋯) = mk ℂ (b i + b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp j).re / ‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j).re / ‖ψ‖ ^ 2

Conditional pairwise relative phase (the (i, j) leg of the 2-cocycle). For a pair (i, j) whose two-level ray mk (b i + b j) is fixed by diagReducedMap hf b i₀, the relative-phase relation Re(conj d_i · d_j) / ‖φ‖² = Re(conj c_i · c_j) / ‖ψ‖² holds. Immediate instance of two_level_relphase_of_fixes for the pair (i, j). The fixing hypothesis hfix is the only residual input: the anchored diagonal reduction supplies it for i = i₀ (diagReducedMap_fixes_two_level) but not for general non-anchored pairs (see the residual note).

Stage 3 piece 2 (W4): triple-support probe and the non-anchored two-level fixing

The non-anchored two-level fixing g (mk (b i + b j)) = mk (b i + b j) for i, j ≠ i₀ — the missing input that upgrades the pairwise relative-phase relation to unconditional — is derived here through a triple-support probe. The equal triple ray mk (b i₀ + b i + b j) is first shown fixed (diagReducedMap_fixes_three_level), then used as a probe carrying both i and j to fix the non-anchored two-level ray (diagReducedMap_fixes_two_level_general), whence the conditional pairwise leg becomes unconditional (diagReducedMap_pairwise_relphase).

Critical honesty (audit). Every probe here is a real-coordinate superposition (all surviving source coordinates = 1), so its ray is fixed by the identity and by coordinatewise conjugation alike: fixing it is consistent with both the unitary (d = c) and antiunitary (d = conj c) branches, and does not collapse the global unitary/antiunitary choice. What is established is the coboundary structure of the phase cocycle (the pairwise real-part relations), not the global sign (piece 3). No ℂ-linearity is assumed: every alignment comes from moduli preservation, a single fixed-probe overlap, and the saturation lemma.

theorem Projectivization.norm_eq_re_imp_eq {z : ℂ} (h : ‖z‖ = z.re) : z = ↑z.re

Saturation. A complex number whose real part equals its modulus is that real part: ‖z‖ = z.re → z = z.re. Squaring, z.re² = ‖z‖² = z.re² + z.im² forces z.im = 0.

theorem Projectivization.eq_of_re_conj_mul_eq {a c : ℂ} (ha : a ≠ 0) (hmod : ‖c‖ = ‖a‖) (hre : ((starRingEnd ℂ) a * c).re = ‖a‖ ^ 2) : c = a

Phase alignment from a saturated overlap. If two complex numbers have equal modulus ‖c‖ = ‖a‖, with a ≠ 0, and the real part of conj a · c saturates the modulus product Re(conj a · c) = ‖a‖², then c = a. Route: ‖conj a · c‖ = ‖a‖‖c‖ = ‖a‖², so Re = ‖·‖; norm_eq_re_imp_eq makes conj a · c real and equal to ‖a‖² = conj a · a; cancel conj a ≠ 0. This is the neutral alignment step; applied to a real-coordinate probe it aligns d = a on both the unitary and antiunitary branches, so it does not collapse the sign.

theorem Projectivization.repr_eq_triple_of_support {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (φ : EuclideanSpace ℂ (Fin N)) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) (hsupp : ∀ (k : Fin N), k ≠ i₀ → k ≠ i → k ≠ j → (b.repr φ).ofLp k = 0) : φ = (b.repr φ).ofLp i₀ • b i₀ + (b.repr φ).ofLp i • b i + (b.repr φ).ofLp j • b j

Triple-support reconstruction. A vector whose coordinates in the basis b vanish outside {i₀, i, j} (distinct) is the triple sum of its three surviving coordinates. OrthonormalBasis.sum_repr expands φ, Finset.sum_subset drops the null coordinates, and the three-element Finset.sum collapses. The 3-support analogue of repr_eq_pair_of_support.

theorem Projectivization.add3_basis_norm_sq {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) : ‖b i₀ + b i + b j‖ ^ 2 = 3

The squared norm of a triple basis sum is 3 (Pythagoras: b i₀ + b i ⟂ b j and ‖b i₀ + b i‖² = 2, ‖b j‖² = 1).

theorem Projectivization.add3_basis_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) : b i₀ + b i + b j ≠ 0

A triple of distinct basis vectors sums to a nonzero vector (norm² = 3).

theorem Projectivization.inner_add3_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (i₀ i j : Fin N) : inner ℂ ψ (b i₀ + b i + b j) = (starRingEnd ℂ) ((b.repr ψ).ofLp i₀ + (b.repr ψ).ofLp i + (b.repr ψ).ofLp j)

The inner product of ψ with a triple basis sum unfolds to the conjugate of the coordinate sum: ⟪ψ, b i₀ + b i + b j⟫ = conj (c_{i₀} + c_i + c_j).

theorem Projectivization.cnorm_add3_sq (A B C : ℂ) : ‖A + B + C‖ ^ 2 = ‖A‖ ^ 2 + ‖B‖ ^ 2 + ‖C‖ ^ 2 + 2 * ((starRingEnd ℂ) A * B).re + 2 * ((starRingEnd ℂ) A * C).re + 2 * ((starRingEnd ℂ) B * C).re

Triple parallelogram expansion. `‖A + B + C‖² = ‖A‖² + ‖B‖² + ‖C‖²

• 2·Re(conj A · B) + 2·Re(conj A · C) + 2·Re(conj B · C). Two applications of cnorm_add_sqplusRe(conj (A+B) · C) = Re(conj A · C) + Re(conj B · C)`.

theorem Projectivization.transProb_three_level {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) : (mk ℂ ψ hψ).transProb (mk ℂ (b i₀ + b i + b j) ⋯) = ‖(b.repr ψ).ofLp i₀ + (b.repr ψ).ofLp i + (b.repr ψ).ofLp j‖ ^ 2 / (‖ψ‖ ^ 2 * 3)

Triple-level overlap in coordinates. The transition probability from mk ψ to the equal triple ray mk (b i₀ + b i + b j) is ‖c_{i₀} + c_i + c_j‖² / (‖ψ‖² · 3). Combines transProb_mk, inner_add3_basis (numerator), RCLike.norm_conj, and add3_basis_norm_sq (denominator).

Stage 3 piece 2 (W4): the triple and non-anchored two-level fixings

theorem Projectivization.diagReducedMap_fixes_three_level {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) : diagReducedMap hf b i₀ (mk ℂ (b i₀ + b i + b j) ⋯) = mk ℂ (b i₀ + b i + b j) ⋯

HEADLINE (triple-support fixing). The diagonally reduced map fixes the equal triple superposition ray mk (b i₀ + b i + b j) for distinct i₀, i, j.

Proof. Write g := diagReducedMap hf b i₀, φ := (g (mk w)).rep with w := b i₀ + b i + b j. Stage-1 moduli (coord_modulus_of_fixes_basis) restrict φ to support {i₀, i, j} with equal coordinate moduli ‖d_k‖² = ‖φ‖²/3. The two anchored two-level fixings (diagReducedMap_two_level_relphase at the probe w) pin Re(conj d_{i₀} · d_i) = ‖φ‖²/3 = ‖d_{i₀}‖² and likewise for j, which saturates the modulus product; eq_of_re_conj_mul_eq forces d_i = d_{i₀} and d_j = d_{i₀}, so φ = d_{i₀} · w and mk φ = mk w.

Audit note. The source coordinates c_{i₀} = c_i = c_j = 1 are real, so this fixing is consistent with both d = c (unitary) and d = conj c (antiunitary): it establishes cocycle coboundary structure, not the global sign. No ℂ-linearity is assumed.

theorem Projectivization.diagReducedMap_fixes_two_level_general {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) : diagReducedMap hf b i₀ (mk ℂ (b i + b j) ⋯) = mk ℂ (b i + b j) ⋯

HEADLINE (non-anchored two-level fixing). The diagonally reduced map fixes every two-level superposition ray mk (b i + b j) with i, j ≠ i₀, i ≠ j — not only the anchored ones. This upgrades the pairwise relative-phase leg to unconditional.

Proof. Write g := diagReducedMap hf b i₀, φ := (g (mk w')).rep, w' := b i + b j. Stage-1 moduli restrict φ to support {i, j} (d_{i₀} = 0) with ‖d_i‖² = ‖d_j‖² = ‖φ‖²/2. The fixed triple ray mk (b i₀ + b i + b j) (diagReducedMap_fixes_three_level) — a probe carrying both i and j — used through transProb_of_fixed gives the overlap identity ‖d_i + d_j‖² / (‖φ‖²·3) = ‖1 + 1‖² / (2·3), whence Re(conj d_i · d_j) = ‖φ‖²/2 = ‖d_i‖², saturating the modulus product; eq_of_re_conj_mul_eq forces d_j = d_i, so φ = d_i · w' and mk φ = mk w'.

Audit note. The probe b i₀ + b i + b j and the source b i + b j are real-coordinate: consistent with both branches. Coboundary structure, not global sign. No ℂ-linearity assumed.

theorem Projectivization.diagReducedMap_pairwise_relphase {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (h0i : i₀ ≠ i) (h0j : i₀ ≠ j) (hij : i ≠ j) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp j).re / ‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j).re / ‖ψ‖ ^ 2

HEADLINE (unconditional pairwise relative phase, the 2-cocycle coboundary). For any distinct i, j ≠ i₀, the diagonally reduced map preserves the real part of the relative phase between coordinates i and j: Re(conj d_i · d_j) / ‖φ‖² = Re(conj c_i · c_j) / ‖ψ‖², for every source ray mk ψ. Discharges the hfix hypothesis of diagReducedMap_pairwise_relphase_of_fixed via the non-anchored two-level fixing diagReducedMap_fixes_two_level_general.

Together with diagReducedMap_two_level_relphase (the anchored legs (i₀, k)), the pairwise legs (i, j) here give the full coboundary structure of the phase 2-cocycle — the real-part relations Re(c̄_i d_j) = Re(c̄_i c_j)·‖φ‖²/‖ψ‖² for all pairs — with the ± sign of the imaginary parts still free (the ℤ/2 datum resolved only by piece 3). No ℂ-linearity is assumed.

Stage 3 piece 3 (W5): the complex probe, the global sign, and the dichotomy

Piece 3 is the finish. Pieces 1–2 established the phase-cocycle coboundary structure through real-coordinate probes, which cannot see the global unitary/antiunitary sign (they are fixed by the identity and by coordinatewise conjugation alike). Piece 3 introduces the complex probe mk (b i₀ + I • b i), whose ray is not conjugation-invariant, so it distinguishes the two branches, and assembles the global dichotomy.

The layout:

• Imaginary relative phase. The I-probe overlap (transProb_two_level_I, transProb_two_level_negI) pins the imaginary part of the relative phase, the datum invisible to piece 2: two_level_imrelphase_of_fixes (from a fixed complex ray) and two_level_imrelphase_of_flips (from a flipped one, the antiunitary reading).
• Reconstruction. Given a TransProbPreserving map fixing every basis ray, every real two-level ray mk (b i + b j), and every complex two-level ray mk (b i + I • b j), the full Gram datum conj dᵢ · dⱼ · ‖ψ‖² = conj cᵢ · cⱼ · ‖φ‖² is pinned, forcing φ = λ • ψ, i.e. the map is the identity on rays (eq_id_of_fixes_all_two_level). If instead the complex rays are flipped, the datum conjugates and the map is coordinatewise conjugation in the basis b (eq_bconj_of_flips_complex). ℂ-linearity is an output of this reconstruction, never an input.
• The complex probe local dichotomy. For each i ≠ i₀ the diagonally reduced map sends mk (b i₀ + I • b i) to mk (b i₀ + I • b i) (plus branch) or mk (b i₀ - I • b i) (minus branch): the anchored real-part relation forces the image phase to have zero real part, and unit modulus leaves exactly ± I (diagReducedMap_complex_probe).

No ℂ-linearity is assumed anywhere below.

theorem Projectivization.re_mul_I_eq_im (x y : ℂ) : (x * Complex.I * (starRingEnd ℂ) y).re = ((starRingEnd ℂ) x * y).im

The imaginary-part conversion (x · I · conj y).re = (conj x · y).im, a coordinate identity in ℂ.

theorem Projectivization.cnorm_sub_I_sq (A B : ℂ) : ‖A - Complex.I * B‖ ^ 2 = ‖A‖ ^ 2 + ‖B‖ ^ 2 + 2 * ((starRingEnd ℂ) A * B).im

Complex "difference" parallelogram. `‖A - I·B‖² = ‖A‖² + ‖B‖²

• 2·(conj A · B).im. Pure real-coordinate algebra via Complex.normSq`.

theorem Projectivization.cnorm_add_I_sq (A B : ℂ) : ‖A + Complex.I * B‖ ^ 2 = ‖A‖ ^ 2 + ‖B‖ ^ 2 - 2 * ((starRingEnd ℂ) A * B).im

Complex "sum" parallelogram with I. `‖A + I·B‖² = ‖A‖² + ‖B‖²

• 2·(conj A · B).im. Pure real-coordinate algebra via Complex.normSq`.

The I-probe b i + I • b j

theorem Projectivization.Iadd_basis_norm_sq {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i j : Fin N} (hij : i ≠ j) : ‖b i + Complex.I • b j‖ ^ 2 = 2

Squared norm of the I-probe: ‖b i + I • b j‖² = 2 (Pythagoras, ‖I • b j‖ = ‖b j‖ = 1).

theorem Projectivization.Iadd_basis_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i j : Fin N} (hij : i ≠ j) : b i + Complex.I • b j ≠ 0

The I-probe is nonzero (norm² = 2).

theorem Projectivization.inner_Iadd_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (i j : Fin N) : inner ℂ ψ (b i + Complex.I • b j) = (starRingEnd ℂ) ((b.repr ψ).ofLp i) + Complex.I * (starRingEnd ℂ) ((b.repr ψ).ofLp j)

Inner product of ψ with the I-probe: ⟪ψ, b i + I • b j⟫ = conj cᵢ + I · conj cⱼ.

theorem Projectivization.transProb_two_level_I {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) {i j : Fin N} (hij : i ≠ j) : (mk ℂ ψ hψ).transProb (mk ℂ (b i + Complex.I • b j) ⋯) = ‖(b.repr ψ).ofLp i - Complex.I * (b.repr ψ).ofLp j‖ ^ 2 / (‖ψ‖ ^ 2 * 2)

I-probe overlap. transProb (mk ψ) (mk (b i + I • b j)) = ‖cᵢ - I · cⱼ‖² / (‖ψ‖² · 2). The numerator conjugate identity conj cᵢ + I · conj cⱼ = conj (cᵢ - I · cⱼ) plus RCLike.norm_conj puts it in the c-coordinate form.

theorem Projectivization.two_level_imrelphase_of_fixes {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (k : Fin N), g (srcPoint b k) = srcPoint b k) {i j : Fin N} (hij : i ≠ j) (hfixI : g (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (g (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (g (mk ℂ ψ hψ)).rep).ofLp j).im / ‖(g (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j).im / ‖ψ‖ ^ 2

Imaginary relative-phase constraint (fixed complex ray). Let g be TransProbPreserving, fixing every basis ray and the complex two-level ray mk (b i + I • b j). Writing g (mk ψ) = mk φ, the imaginary part of the relative phase is preserved: Im(conj dᵢ · dⱼ) / ‖φ‖² = Im(conj cᵢ · cⱼ) / ‖ψ‖². The I-probe is not conjugation-invariant, so this is the datum piece 2 could not reach. Pure overlap algebra; no ℂ-linearity.

The -I-probe b i - I • b j (the flipped complex ray)

theorem Projectivization.subI_basis_norm_sq {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i j : Fin N} (hij : i ≠ j) : ‖b i - Complex.I • b j‖ ^ 2 = 2

Squared norm of the -I-probe: ‖b i - I • b j‖² = 2.

theorem Projectivization.subI_basis_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i j : Fin N} (hij : i ≠ j) : b i - Complex.I • b j ≠ 0

The -I-probe is nonzero (norm² = 2).

theorem Projectivization.inner_subI_basis {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (i j : Fin N) : inner ℂ ψ (b i - Complex.I • b j) = (starRingEnd ℂ) ((b.repr ψ).ofLp i) - Complex.I * (starRingEnd ℂ) ((b.repr ψ).ofLp j)

Inner product of ψ with the -I-probe: ⟪ψ, b i - I • b j⟫ = conj cᵢ - I · conj cⱼ.

theorem Projectivization.transProb_two_level_negI {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) {i j : Fin N} (hij : i ≠ j) : (mk ℂ ψ hψ).transProb (mk ℂ (b i - Complex.I • b j) ⋯) = ‖(b.repr ψ).ofLp i + Complex.I * (b.repr ψ).ofLp j‖ ^ 2 / (‖ψ‖ ^ 2 * 2)

-I-probe overlap. transProb (mk ψ) (mk (b i - I • b j)) = ‖cᵢ + I · cⱼ‖² / (‖ψ‖² · 2).

theorem Projectivization.two_level_imrelphase_of_flips {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (k : Fin N), g (srcPoint b k) = srcPoint b k) {i j : Fin N} (hij : i ≠ j) (hflipI : g (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (g (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (g (mk ℂ ψ hψ)).rep).ofLp j).im / ‖(g (mk ℂ ψ hψ)).rep‖ ^ 2 = -((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j).im / ‖ψ‖ ^ 2

Imaginary relative-phase constraint (flipped complex ray). If g TransProbPreserving fixes every basis ray and flips the complex two-level ray, g (mk (b i + I • b j)) = mk (b i - I • b j), then the imaginary part of the relative phase is negated: Im(conj dᵢ · dⱼ) / ‖φ‖² = -Im(conj cᵢ · cⱼ) / ‖ψ‖². This is the antiunitary reading. No ℂ-linearity.

Reconstruction: from the Gram datum to the identity / conjugation

theorem Projectivization.mul_ofReal_re (z : ℂ) (r : ℝ) : (z * ↑r).re = z.re * r

Real part of a product with a real scalar on the right: (z · r).re = z.re · r.

theorem Projectivization.mul_ofReal_im (z : ℂ) (r : ℝ) : (z * ↑r).im = z.im * r

Imaginary part of a product with a real scalar on the right: (z · r).im = z.im · r.

theorem Projectivization.eq_id_of_fixes_all_two_level {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (k : Fin N), g (srcPoint b k) = srcPoint b k) (hR : ∀ (i j : Fin N) (hij : i ≠ j), g (mk ℂ (b i + b j) ⋯) = mk ℂ (b i + b j) ⋯) (hI : ∀ (i j : Fin N) (hij : i ≠ j), g (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : g (mk ℂ ψ hψ) = mk ℂ ψ hψ

Reconstruction (unitary branch). A TransProbPreserving map g fixing every basis ray, every real two-level ray mk (b i + b j), and every complex two-level ray mk (b i + I • b j) is the identity on rays: g (mk ψ) = mk ψ for every ψ ≠ 0.

The real relations (two_level_relphase_of_fixes) and the imaginary relations (two_level_imrelphase_of_fixes) together pin the full Gram datum conj dᵢ · dⱼ · ‖ψ‖² = conj cᵢ · cⱼ · ‖φ‖² for every pair; taking a reference index i₁ with c_{i₁} ≠ 0 gives dⱼ = λ · cⱼ with λ fixed, so φ = λ • ψ. ℂ-linearity is an output here, not an input.

noncomputable def Projectivization.bConjVec {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) : EuclideanSpace ℂ (Fin N)

Coordinatewise complex conjugation in the basis b: bConjVec b ψ = ∑ⱼ conj(b.repr ψ j) • b j. Its k-th coordinate is conj(b.repr ψ k) (repr_bConjVec). For the standard basis this is conjVec.

Equations

• Projectivization.bConjVec b ψ = ∑ j : Fin N, (starRingEnd ℂ) ((b.repr ψ).ofLp j) • b j

theorem Projectivization.repr_bConjVec {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (ψ : EuclideanSpace ℂ (Fin N)) (k : Fin N) : (b.repr (bConjVec b ψ)).ofLp k = (starRingEnd ℂ) ((b.repr ψ).ofLp k)

The k-th coordinate of bConjVec b ψ is conj (b.repr ψ k).

theorem Projectivization.bConjVec_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : bConjVec b ψ ≠ 0

bConjVec b ψ is nonzero when ψ is (some conjugate coordinate is nonzero).

theorem Projectivization.unit_re_zero_eq_I_or_negI {ε : ℂ} (h1 : ‖ε‖ = 1) (h2 : ε.re = 0) : ε = Complex.I ∨ ε = -Complex.I

A unit-modulus complex number with zero real part is ± I. Squaring the norm, ε.im² = 1, so ε.im = ±1 and ε = ⟨0, ±1⟩.

theorem Projectivization.eq_bconj_of_flips_complex {N : ℕ} {g : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hg : TransProbPreserving g) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (hfixb : ∀ (k : Fin N), g (srcPoint b k) = srcPoint b k) (hR : ∀ (i j : Fin N) (hij : i ≠ j), g (mk ℂ (b i + b j) ⋯) = mk ℂ (b i + b j) ⋯) (hflip : ∀ (i j : Fin N) (hij : i ≠ j), g (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : g (mk ℂ ψ hψ) = mk ℂ (bConjVec b ψ) ⋯

Reconstruction (antiunitary branch). A TransProbPreserving map g fixing every basis ray, every real two-level ray mk (b i + b j), and flipping every complex two-level ray, g (mk (b i + I • b j)) = mk (b i - I • b j), is coordinatewise conjugation in the basis b: g (mk ψ) = mk (bConjVec b ψ) for every ψ ≠ 0.

The real relations survive, but the imaginary relations are negated (two_level_imrelphase_of_flips), conjugating the Gram datum to conj dᵢ · dⱼ · ‖ψ‖² = cᵢ · conj cⱼ · ‖φ‖², so dⱼ = μ · conj cⱼ and φ = μ • bConjVec b ψ. No ℂ-linearity is assumed; this is the genuine antiunitary branch of the Wigner disjunction.

The complex probe: the branch-distinguishing local dichotomy

theorem Projectivization.diagReducedMap_complex_probe {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i₀ i : Fin N} (hii : i₀ ≠ i) : diagReducedMap hf b i₀ (mk ℂ (b i₀ + Complex.I • b i) ⋯) = mk ℂ (b i₀ + Complex.I • b i) ⋯ ∨ diagReducedMap hf b i₀ (mk ℂ (b i₀ + Complex.I • b i) ⋯) = mk ℂ (b i₀ - Complex.I • b i) ⋯

HEADLINE (the complex probe). For i ≠ i₀ the diagonally reduced map sends the complex probe ray mk (b i₀ + I • b i) to either itself (plus branch) or mk (b i₀ - I • b i) (minus branch).

Unlike the real probes of pieces 1–2, the complex probe ray is not invariant under coordinatewise conjugation (conjVec (b i₀ + I • b i) = b i₀ - I • b i), so it distinguishes the unitary branch (+) from the antiunitary branch (-).

Proof. Stage-1 moduli restrict the image φ to support {i₀, i} with equal coordinate moduli. The anchored real relation (diagReducedMap_two_level_relphase) at the source coordinates c_{i₀} = 1, c_i = I gives Re(conj d_{i₀} · d_i) = 0, so the ratio ε := d_i / d_{i₀} has zero real part and unit modulus, hence ε = ± I (unit_re_zero_eq_I_or_negI). The two signs are the two branches. No ℂ-linearity is assumed.

The reduced-map dichotomy (conditional on the global complex sign)

theorem Projectivization.diagReducedMap_fixes_real_all {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ i j : Fin N) (hij : i ≠ j) : diagReducedMap hf b i₀ (mk ℂ (b i + b j) ⋯) = mk ℂ (b i + b j) ⋯

The diagonally reduced map fixes every real two-level ray mk (b i + b j), i ≠ j (anchored via diagReducedMap_fixes_two_level, non-anchored via diagReducedMap_fixes_two_level_general, with an add_comm swap for the j = i₀ case). Discharges the hR hypothesis of the reconstruction lemmas for the concrete diagonally reduced map.

theorem Projectivization.diagReducedMap_dichotomy_of_complexSign {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) (hsign : (∀ (i j : Fin N) (hij : i ≠ j), diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯) ∨ ∀ (i j : Fin N) (hij : i ≠ j), diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯) : (∀ (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0), diagReducedMap hf b i₀ (mk ℂ ψ hψ) = mk ℂ ψ hψ) ∨ ∀ (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0), diagReducedMap hf b i₀ (mk ℂ ψ hψ) = mk ℂ (bConjVec b ψ) ⋯

The reduced-map Wigner dichotomy (conditional on the global sign). Given the global complex-sign closure hsign — either the diagonally reduced map g := diagReducedMap hf b i₀ fixes every complex two-level ray mk (b i + I • b j), or it flips every one to mk (b i - I • b j) — the map is globally the identity on rays, or globally coordinatewise conjugation in the basis b:

• fixes-all branch ⟹ g (mk ψ) = mk ψ for all ψ (the unitary class);
• flips-all branch ⟹ g (mk ψ) = mk (bConjVec b ψ) for all ψ (the antiunitary class).

The real fixings are discharged internally (diagReducedMap_fixes_real_all); the two disjuncts feed the two reconstruction lemmas. The antiunitary branch is genuinely present and ℂ-linearity is an output, never assumed. The single residual to an unconditional Wigner converse is hsign, for which diagReducedMap_complex_probe supplies the per-pair ± I datum; see the Stage 3 (residual) note.

theorem Projectivization.diagReducedMap_relphase_all {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : ((starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp j).re / ‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2 = ((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j).re / ‖ψ‖ ^ 2

theorem Projectivization.diagReducedMap_complex_probe_general {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) : diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯ ∨ diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯

theorem Projectivization.diagReducedMap_gram_of_fixed {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) (hfixI : diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : (starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp j * ↑(‖ψ‖ ^ 2) = (starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j * ↑(‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2)

Gram datum for a fixed complex ray.

theorem Projectivization.diagReducedMap_gram_of_flips {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) (hflipI : diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : (starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp j * ↑(‖ψ‖ ^ 2) = (starRingEnd ℂ) ((starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp j) * ↑(‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2)

Gram datum for a flipped complex ray.

theorem Projectivization.diagReducedMap_gram_diag {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ i : Fin N) {ψ : EuclideanSpace ℂ (Fin N)} (hψ : ψ ≠ 0) : (starRingEnd ℂ) ((b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i) * (b.repr (diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep).ofLp i * ↑(‖ψ‖ ^ 2) = (starRingEnd ℂ) ((b.repr ψ).ofLp i) * (b.repr ψ).ofLp i * ↑(‖(diagReducedMap hf b i₀ (mk ℂ ψ hψ)).rep‖ ^ 2)

Gram datum on the diagonal (moduli).

Master witness and the global-sign closure

noncomputable def Projectivization.masterVec {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) : EuclideanSpace ℂ (Fin N)

Master witness vector: ∑ a, (1 + I·a) • b a. All coordinates nonzero and all pairwise imaginary relative phases nonzero.

Equations

• Projectivization.masterVec b = ∑ a : Fin N, (1 + Complex.I * ↑↑a) • b a

theorem Projectivization.masterVec_repr {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (k : Fin N) : (b.repr (masterVec b)).ofLp k = 1 + Complex.I * ↑↑k

theorem Projectivization.masterVec_coord_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (k : Fin N) : (b.repr (masterVec b)).ofLp k ≠ 0

theorem Projectivization.masterVec_ne_zero {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (k : Fin N) : masterVec b ≠ 0

theorem Projectivization.masterVec_im_ne {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {a c : Fin N} (hac : a ≠ c) : ((starRingEnd ℂ) ((b.repr (masterVec b)).ofLp a) * (b.repr (masterVec b)).ofLp c).im ≠ 0

theorem Projectivization.Iprobe_ne_negIprobe {N : ℕ} (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) {i j : Fin N} (hij : i ≠ j) : mk ℂ (b i + Complex.I • b j) ⋯ ≠ mk ℂ (b i - Complex.I • b j) ⋯

The complex probe mk (b i + I • b j) and its conjugate mk (b i - I • b j) are distinct projective points (their reps are orthogonal).

theorem Projectivization.sign_link_core {cA cB cC dA dB dC : ℂ} {S F : ℝ} (hFpos : 0 < F) (hcA : cA ≠ 0) (hcB : cB ≠ 0) (hcC : cC ≠ 0) (hImAB : ((starRingEnd ℂ) cA * cB).im ≠ 0) (hImBC : ((starRingEnd ℂ) cB * cC).im ≠ 0) {Γab Γbc Γac : ℂ} (Eab : (starRingEnd ℂ) dA * dB * ↑S = Γab * ↑F) (Ebc : (starRingEnd ℂ) dB * dC * ↑S = Γbc * ↑F) (Eac : (starRingEnd ℂ) dA * dC * ↑S = Γac * ↑F) (Ebb : (starRingEnd ℂ) dB * dB * ↑S = (starRingEnd ℂ) cB * cB * ↑F) (hAB : Γab = (starRingEnd ℂ) cA * cB ∨ Γab = (starRingEnd ℂ) ((starRingEnd ℂ) cA * cB)) (hBC : Γbc = (starRingEnd ℂ) cB * cC ∨ Γbc = (starRingEnd ℂ) ((starRingEnd ℂ) cB * cC)) (hAC : Γac = (starRingEnd ℂ) cA * cC ∨ Γac = (starRingEnd ℂ) ((starRingEnd ℂ) cA * cC)) : Γab = (starRingEnd ℂ) cA * cB ↔ Γbc = (starRingEnd ℂ) cB * cC

Abstract algebraic core of the global-sign linking: given the Gram equations for three coordinates and the master genericity (imaginary relative phases nonzero), the fixed/flipped sign of the pair (a,b) matches that of (b,c).

def Projectivization.CFixed {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) : Prop

Abbreviation: the diagonally reduced map fixes the complex two-level ray (i,j).

Equations

• Projectivization.CFixed hf b i₀ hij = (Projectivization.diagReducedMap hf b i₀ (Projectivization.mk ℂ (b i + Complex.I • b j) ⋯) = Projectivization.mk ℂ (b i + Complex.I • b j) ⋯)

theorem Projectivization.diagReducedMap_complexSign_link {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {a bx c : Fin N} (hab : a ≠ bx) (hbc : bx ≠ c) (hac : a ≠ c) : CFixed hf b i₀ hab ↔ CFixed hf b i₀ hbc

Middle-index linking: the complex sign of (a,bx) matches that of (bx,c).

theorem Projectivization.diagReducedMap_complexSign_swap {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) : CFixed hf b i₀ hij → CFixed hf b i₀ ⋯

Order swap: the complex sign of (i,j) matches that of (j,i) (by injectivity).

theorem Projectivization.diagReducedMap_complexSign_swapIff {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) : CFixed hf b i₀ hij ↔ CFixed hf b i₀ ⋯

Order swap as an iff.

theorem Projectivization.diagReducedMap_complexSign_link' {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {a bx c : Fin N} (hab : a ≠ bx) (hac : a ≠ c) (hbc : bx ≠ c) : CFixed hf b i₀ hab ↔ CFixed hf b i₀ hac

Shared-first-index linking: the complex sign of (a,bx) matches that of (a,c).

theorem Projectivization.diagReducedMap_complexSign_all {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) {i j : Fin N} (hij : i ≠ j) {k l : Fin N} (hkl : k ≠ l) : CFixed hf b i₀ hij ↔ CFixed hf b i₀ hkl

Global constancy: the complex sign is the same for every pair.

theorem Projectivization.diagReducedMap_complexSign_closure {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) : (∀ (i j : Fin N) (hij : i ≠ j), diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i + Complex.I • b j) ⋯) ∨ ∀ (i j : Fin N) (hij : i ≠ j), diagReducedMap hf b i₀ (mk ℂ (b i + Complex.I • b j) ⋯) = mk ℂ (b i - Complex.I • b j) ⋯

HEADLINE (global-sign closure). The per-pair ± I complex-probe datum is globally consistent: either every complex two-level ray is fixed, or every one is flipped. Discharges the hsign hypothesis of diagReducedMap_dichotomy_of_complexSign from transition-probability preservation alone.

theorem Projectivization.diagReducedMap_dichotomy {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) (b : OrthonormalBasis (Fin N) ℂ (EuclideanSpace ℂ (Fin N))) (i₀ : Fin N) : (∀ (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0), diagReducedMap hf b i₀ (mk ℂ ψ hψ) = mk ℂ ψ hψ) ∨ ∀ (ψ : EuclideanSpace ℂ (Fin N)) (hψ : ψ ≠ 0), diagReducedMap hf b i₀ (mk ℂ ψ hψ) = mk ℂ (bConjVec b ψ) ⋯

HEADLINE (unconditional reduced-map dichotomy). The diagonally reduced map is globally the identity on rays, or globally coordinatewise conjugation in b. The global-sign residual is discharged (diagReducedMap_complexSign_closure); both branches are genuine and no ℂ-linearity is assumed.

STEP 2: assembly of the Wigner rigidity theorem

theorem Projectivization.projMap_comp {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e₁ e₂ : E ≃ₗᵢ[ℂ] E) (p : Projectivization ℂ E) : projMap e₁ (projMap e₂ p) = projMap (e₂.trans e₁) p

projMap functoriality: composition of projective isometry maps.

theorem Projectivization.projMap_symm_projMap {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (e : E ≃ₗᵢ[ℂ] E) (p : Projectivization ℂ E) : projMap e (projMap e.symm p) = p

projMap e and projMap e.symm are inverse.

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

Coordinatewise conjugation in the standard basis is conjVec.

theorem Projectivization.wigner_rigidity {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) : (∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = projMap e p) ∨ ∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = projMap e p.conjProj

HEADLINE (Wigner / Fubini-Study rigidity converse). Every transition-probability-preserving self-map of ℂℙ^{N-1} is induced by a unitary (projMap e for a ≃ₗᵢ[ℂ] e) or by an antiunitary (projMap e ∘ conjProj). ℂ-linearity of e is an OUTPUT of the construction (the reduced map lands on the identity), never assumed; the antiunitary branch is genuinely present (conjProj); the global unitary/antiunitary sign is forced from transition-probability preservation alone. Foundational-triple only.

Stage 3 complete (W6): the Wigner / Fubini-Study rigidity converse

Stages 1-3 are proved with no linearity assumed on f, only TransProbPreserving. Stage 3 piece 3 (W5) delivered the complex probe, both reconstruction directions, and the reduced-map dichotomy conditional on the global complex-sign closure. W6 discharges that closure (diagReducedMap_complexSign_closure) from transition-probability preservation alone: the per-pair ± I datum is globally consistent (all complex two-level rays fixed, or all flipped). The route is (a) the non-anchored per-pair ± I dichotomy (diagReducedMap_complex_probe_general); (b) the master witness masterVec with every pairwise imaginary relative phase nonzero (masterVec_im_ne); (c) the abstract Gram-triple core sign_link_core, ruling out mixed signs via the rank-1 identity g_ab g_bc = g_ac ‖d_b‖² and the imaginary relative phases; (d) order swap by injectivity (diagReducedMap_complexSign_swap, distinct rays mk (b i + I b j) and mk (b i - I b j)) plus index linking (..._link / ..._link' / ..._all). Neither Complex.arg nor any linearity is used; both ± branches stay alive until the probes resolve them.

The unconditional diagReducedMap_dichotomy follows, and the headline wigner_rigidity inverts the frame reductions (f = projMap (candidateUnitary hf b) ∘ projMap D ∘ diagReducedMap, with b the standard basis so bConjVec b = conjVec) to conclude that every TransProbPreserving self-map of ℂℙ^{N-1} is projMap e for a ≃ₗᵢ[ℂ] e (unitary) or projMap e ∘ conjProj (antiunitary). The antiunitary branch is genuinely present (conjProj); ℂ-linearity of e is an OUTPUT of the dichotomy landing on the identity, never assumed; the global sign is forced, not posited. Foundational triple only (propext, Classical.choice, Quot.sound); no busch, no sorry, no native_decide.

The Matrix.unitaryGroup reformulation

wigner_rigidity produces a ≃ₗᵢ[ℂ] witness e and states f = projMap e (or = projMap e ∘ conjProj). This section restates the theorem in the classic ∃ U : Matrix.unitaryGroup (Fin N) ℂ, f = U • · form, where U • · is the exact projective action used by transProbPreserving_unitary / transProb_smul_unitary (the MulAction.compHom of Matrix.UnitaryGroup.toEuclideanLinearEquivHom). The bridge is the matrix of the isometry in the standard basis: unitaryOfIsometry e := toEuclideanLin.symm e, whose columns are e (basisFun j), hence star M * M = 1 by the isometry property e.inner_map_map and orthonormality of basisFun. The antiunitary branch is kept genuinely present as U • conjProj p.

noncomputable def Projectivization.unitaryOfIsometry {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) : Matrix (Fin N) (Fin N) ℂ

The matrix of a linear isometry equivalence in the standard basis of EuclideanSpace ℂ (Fin N), i.e. the inverse image under the linear equivalence Matrix.toEuclideanLin. Its toEuclideanLin is e by construction (unitaryOfIsometry_toEuclideanLin); it lies in unitaryGroup (unitaryOfIsometry_mem).

Equations

• Projectivization.unitaryOfIsometry e = Matrix.toEuclideanLin.symm ↑↑↑e

theorem Projectivization.unitaryOfIsometry_toEuclideanLin {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) : Matrix.toEuclideanLin (unitaryOfIsometry e) = ↑↑↑e

toEuclideanLin (unitaryOfIsometry e) = e: the matrix realises the isometry's linear map. Immediate from LinearEquiv.apply_symm_apply.

theorem Projectivization.unitaryOfIsometry_apply {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) (i j : Fin N) : unitaryOfIsometry e i j = (e ((EuclideanSpace.basisFun (Fin N) ℂ) j)).ofLp i

Column formula: the (i, j) entry of unitaryOfIsometry e is the i-th coordinate of e (basisFun j). Evaluate toEuclideanLin (unitaryOfIsometry e) at the standard basis vector basisFun j (= Pi.single j 1 after ofLp) and use unitaryOfIsometry_toEuclideanLin.

theorem Projectivization.unitaryOfIsometry_mem {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) : unitaryOfIsometry e ∈ Matrix.unitaryGroup (Fin N) ℂ

unitaryOfIsometry e is a unitary matrix: star M * M = 1, because the (j, k) entry of star M * M is ⟪e (basisFun j), e (basisFun k)⟫ = ⟪basisFun j, basisFun k⟫ = δ_{jk} via e.inner_map_map and orthonormality of basisFun.

noncomputable def Projectivization.unitaryGroupOfIsometry {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) : ↥(Matrix.unitaryGroup (Fin N) ℂ)

The unitaryGroup element attached to a linear isometry equivalence.

Equations

• Projectivization.unitaryGroupOfIsometry e = ⟨Projectivization.unitaryOfIsometry e, ⋯⟩

theorem Projectivization.projMap_eq_smul_unitary {N : ℕ} (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : projMap e p = unitaryGroupOfIsometry e • p

The action bridge. projMap e agrees with the unitaryGroup ray action unitaryGroupOfIsometry e • · used by transProbPreserving_unitary. Reduce p to mk p.rep, push both sides through projMap_mk / smul_mk_eq_mk_toEuclideanLin, and note the underlying vectors agree since toEuclideanLin (unitaryOfIsometry e) = e.

theorem Projectivization.wigner_rigidity_unitaryGroup {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : TransProbPreserving f) : (∃ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = U • p) ∨ ∃ (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = U • p.conjProj

HEADLINE (Wigner rigidity, unitaryGroup form). The classic statement: every transition-probability-preserving self-map of ℂℙ^{N-1} is U • · for a U : Matrix.unitaryGroup (Fin N) ℂ (the unitary branch) or U • conjProj · (the antiunitary branch), with U • · the same MulAction used by transProbPreserving_unitary. Reformulation of wigner_rigidity through the isometry-to-matrix bridge projMap_eq_smul_unitary; no ℂ-linearity is assumed on f, the antiunitary branch is genuinely present, foundational-triple only.