Empirical/CSD/Gates: Wigner discharge of CSDUnitaryBundle.U_isometry (LF4-todo §13.2)

Category: 3-Local (CSD-side discharge of the §13.2 obligation).

What this file provides

The CSDUnitaryBundle.U_isometry field (∀ x y, ⟪U x, U y⟫ = ⟪x, y⟫) is discharged through Wigner from the intrinsic transition-probability-preserving condition on a projective self-map, rather than posited as a Hilbert isometry.

• Projectivization.transProbPreserving_isometry_dichotomy — the honest Wigner dichotomy at the Hilbert level: a TransProbPreserving self-map of ℂℙ^{N-1} is realised by a genuine ≃ₗᵢ[ℂ] e with ⟪e x, e y⟫ = ⟪x, y⟫ (unitary, giving U_isometry), OR by an antiunitary e ∘ conjVec with ⟪e (conjVec x), e (conjVec y)⟫ = conj ⟪x, y⟫ (time-reversal / anti-isometry; it does not satisfy U_isometry as stated). The antiunitary branch is not dropped: it is exposed with its conjugated inner-product law.
• CSDBridge.Gates.u_isometry_of_transProbPreserving — the constructor headline: from TransProbPreserving f plus a no-time-reversal selection (f is not the antiunitary branch), Wigner produces a ≃ₗᵢ[ℂ] e realising f and satisfying ⟪e x, e y⟫ = ⟪x, y⟫. Unitarity (hence U_isometry) is the OUTPUT of Wigner, not an input.
• CSDBridge.Gates.CSDUnitaryBundle.ofTransProbPreserving — the same content packaged as a CSDUnitaryBundle: U_isometry is a THEOREM.
• Projectivization.conjProj_ne_projMap / smul_action_not_antiunitary — the non-vacuity core: coordinatewise conjugation is not a unitary projective map (N ≥ 2), so the sector action g • · (a Matrix.unitaryGroup element, the posited-sector datum, SO-1) satisfies the no-time-reversal selection.
• cpSectorActionBundle — a concrete CSDUnitaryBundle on cpSectorData p₀ whose U_isometry is DERIVED (via the constructor, from the sector action's transition-probability preservation), not posited. Non-vacuous. Honest scope of this witness. Here f = g • · already carries isometry structure (that is exactly why transProbPreserving_unitary g and smul_action_not_antiunitary are provable), so for this concrete instance the Wigner step adds no content: an isometry realising f was in hand a priori. Read this as "U_isometry derived from the posited-sector action (SO-1) (which already carries the isometry)", NOT as "isometry derived from blind deterministic dynamics". The content-adding case — Wigner manufacturing an isometry from a map NOT presented as one — is the general constructor u_isometry_of_transProbPreserving; the general μL-flow ⟹ transProb lift is the open D1 gap.

Honest status of §13.2

Discharged MODULO the posited sector symmetry (SO-1). For projective dynamics that preserve the transition-probability structure, U_isometry is a theorem via Wigner, non-vacuously realised by the sector action on the concrete Kähler instance. The primitive moves from "posit the Hilbert unitary U with U_isometry" to "posit the projective dynamics preserves transition probabilities and is not time-reversal".

True residue (D1). The transition-probability preservation is FORCED by the sector symmetry — the sector group G acting by Fubini–Study isometries, which is the SO-1 sector datum (SectorData.(π, G)) — not by μL-measure-preservation. Measure-preservation is strictly weaker than metric preservation: a μFS-measure-preserving self-map of ℂℙ^{N-1} need not preserve the Fubini–Study metric / transition probability, so no lemma "measure-preserving f_Φ ⟹ TransProbPreserving f_Φ" is proved here (it is false). Deriving TransProbPreserving f_Φ from a general μL-flow for a non-symmetry flow is the open D1 gap. So §13.2 discharges exactly modulo the posited sector symmetry, correcting the earlier (false) "measure-preserving π-equivariant flow ⟹ isometry" reading of the obligation.

Foundational-triple only; no busch.

theorem Projectivization.conjProj_ne_projMap {N : ℕ} (hN : 2 ≤ N) (h : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)) : ¬∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), p.conjProj = projMap h p

Coordinatewise conjugation is not a unitary projective map (N ≥ 2). For any ≃ₗᵢ[ℂ] h, conjProj ≠ projMap h. Probe rays: the real rays fix the diagonal scalars h uᵢ = dᵢ • uᵢ, the real sum ray forces d₀ = d₁, and the complex ray mk (u₀ + I • u₁) — which conjProj sends to mk (u₀ − I • u₁) and projMap h to mk (u₀ + I • u₁) — forces I = −I, absurd. This is the crisp statement that the antiunitary class is genuinely distinct from the unitary class, and the non-vacuity core of the no-time-reversal selection below.

theorem Projectivization.transProbPreserving_isometry_dichotomy {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) ∧ ∀ (x y : EuclideanSpace ℂ (Fin N)), inner ℂ (e x) (e y) = inner ℂ x y) ∨ ∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), (∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = projMap e p.conjProj) ∧ ∀ (x y : EuclideanSpace ℂ (Fin N)), inner ℂ (e (conjVec x)) (e (conjVec y)) = (starRingEnd ℂ) (inner ℂ x y)

Honest Wigner dichotomy at the Hilbert level. A TransProbPreserving self-map of ℂℙ^{N-1} is realised either by a genuine ≃ₗᵢ[ℂ] e satisfying the isometry law ⟪e x, e y⟫ = ⟪x, y⟫ (the unitary branch, which discharges CSDUnitaryBundle.U_isometry), or by the antiunitary map e ∘ conjVec satisfying the conjugated law ⟪e (conjVec x), e (conjVec y)⟫ = conj ⟪x, y⟫ (the time-reversal branch, which does not satisfy U_isometry as stated). The antiunitary branch is not silently dropped: it is exposed with its anti-isometry law. ℂ-linearity of e is an OUTPUT of wigner_rigidity, not assumed.

theorem Projectivization.smul_action_not_antiunitary {N : ℕ} (hN : 2 ≤ N) (g : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : ¬∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), g • p = projMap e p.conjProj

The sector action g • · is not time-reversal (N ≥ 2). No ≃ₗᵢ[ℂ] e realises the unitary projective action g • · as the antiunitary e ∘ conjProj. Reduces to conjProj_ne_projMap: writing g • · = projMap eg with eg := (toEuclideanLinearEquiv g).isometryOfInner _ (isometry via inner_toEuclideanLin_unitary), an antiunitary factorisation would make conjProj = projMap (eg.trans e.symm), contradicting conjProj_ne_projMap.

theorem CSD.Empirical.CSDBridge.Gates.u_isometry_of_transProbPreserving {N : ℕ} {f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (hf : Projectivization.TransProbPreserving f) (hsel : ¬∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = Projectivization.projMap e p.conjProj) : ∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), (∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = Projectivization.projMap e p) ∧ ∀ (x y : EuclideanSpace ℂ (Fin N)), inner ℂ (e x) (e y) = inner ℂ x y

Constructor headline: U_isometry derived via Wigner. From TransProbPreserving f (the intrinsic transition-probability condition on a projective self-map) plus a no-time-reversal selection (f is not the antiunitary branch), Wigner produces a ≃ₗᵢ[ℂ] e realising f and satisfying the isometry law ⟪e x, e y⟫ = ⟪x, y⟫. Unitarity — hence CSDUnitaryBundle.U_isometry — is the OUTPUT of wigner_rigidity, never assumed. The primitive is thereby weakened from "posit the Hilbert isometry" to "posit the projective dynamics preserves transition probabilities and is not time-reversal". The no-time-reversal selection is a discrete ℤ/2 datum (the Kähler / ℂ-linearity orientation), not the isometry data.

noncomputable def CSD.Empirical.CSDBridge.Gates.CSDUnitaryBundle.ofTransProbPreserving {SigmaSpace : Type u_1} {P : Type u_2} {G : Type u_3} [MeasurableSpace SigmaSpace] [Nonempty SigmaSpace] [MeasurableSpace P] [Group G] [MulAction G SigmaSpace] [MulAction G P] [MulAction.IsPretransitive G P] {N : ℕ} {D : LF2.SectorData SigmaSpace P G} (ctx : Context D) (f : Projectivization ℂ (EuclideanSpace ℂ (Fin N)) → Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (hf : Projectivization.TransProbPreserving f) (hsel : ¬∃ (e : EuclideanSpace ℂ (Fin N) ≃ₗᵢ[ℂ] EuclideanSpace ℂ (Fin N)), ∀ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), f p = Projectivization.projMap e p.conjProj) : CSDUnitaryBundle D N (EuclideanSpace ℂ (Fin N))

CSDUnitaryBundle with U_isometry discharged through Wigner. Given a bridge context, a TransProbPreserving projective self-map f, and the no-time-reversal selection, produces a CSDUnitaryBundle whose carried U is the Wigner-output isometry and whose U_isometry field is a THEOREM (e.inner_map_map), not a posit. This is the §13.2 discharge on the Hilbert space EuclideanSpace ℂ (Fin N).

Equations

• CSD.Empirical.CSDBridge.Gates.CSDUnitaryBundle.ofTransProbPreserving ctx f hf hsel = { toContext := ctx, U := ⇑⋯.choose, U_isometry := ⋯ }

noncomputable def CSD.LF4.cpBridgeData {N : ℕ} [NeZero N] (p₀ : CPN N) : LF2.MeasureBridgeData (cpSectorData p₀) (Matrix.UnitaryGroup.fubiniStudyMeasure p₀)

Measure-bridge data for cpSectorData (c = 1, π = id), built axiom-free from fubiniStudyMeasure_smul_invariant and Measure.map_id.

Equations

• CSD.LF4.cpBridgeData p₀ = { is_inv := ⋯, c := 1, bridge_eq := ⋯ }

noncomputable def CSD.LF4.cpContext {N : ℕ} [NeZero N] (p₀ : CPN N) : Empirical.CSDBridge.Context (cpSectorData p₀)

The bridge context for the concrete ℂℙ^{N-1} / U(N) instance.

Equations

• CSD.LF4.cpContext p₀ = { μFS := Matrix.UnitaryGroup.fubiniStudyMeasure p₀, hμFS_prob := ⋯, bridge := CSD.LF4.cpBridgeData p₀ }

noncomputable def CSD.LF4.cpSectorActionBundle {N : ℕ} [NeZero N] (hN : 2 ≤ N) (p₀ : CPN N) (g : ↥(Matrix.unitaryGroup (Fin N) ℂ)) : Empirical.CSDBridge.Gates.CSDUnitaryBundle (cpSectorData p₀) N (EuclideanSpace ℂ (Fin N))

Non-vacuous §13.2 discharge on the concrete Kähler instance. A concrete CSDUnitaryBundle on cpSectorData p₀ whose U_isometry is DERIVED (via CSDUnitaryBundle.ofTransProbPreserving, from the sector action's transition-probability preservation transProbPreserving_unitary g) rather than posited. The no-time-reversal selection is supplied by smul_action_not_antiunitary (N ≥ 2): the sector action g • · is a Matrix.unitaryGroup element acting — the posited-sector-symmetry datum (SO-1) — hence not time-reversal. Unitarity is the OUTPUT of Wigner.

Equations

• One or more equations did not get rendered due to their size.