W3 clopen-datum closure: the Bargmann discriminator

Category: 3-Programme (CSD dynamics spine, the W3 staged residual).

W3 (UnitarySelection.lean) selected the unitary Wigner branch STAGED on a clopen datum: IsClopen {t | ProjUnitary d t}, the Lean image of (i) continuity of t ↦ projectedFlow t and (ii) the disconnectedness of the antiunitary component of the Fubini–Study isometry group. This module closes that datum:

• (ii) is PROVED. The Bargmann invariant (the normalised triple product Δ, Bargmann.lean) is preserved by the unitary branch and CONJUGATED by the antiunitary branch. On a probe triple with Im Δ ≠ 0 (exists for N ≥ 2) the two branches therefore sit at the two DISTINCT values Δ and conj Δ of one scalar observable: they are separated, and the Wigner disjunction is EXCLUSIVE (not_projUnitary_and_projAntiunitary).
• (i) is REDUCED to a scalar continuity datum. If the Bargmann observable t ↦ Δ(Φ_t p, Φ_t q, Φ_t r) of the flow is continuous, the unitary-time set is the preimage of the closed point {Δ₀} and its complement the preimage of {conj Δ₀} — both closed, so the set is CLOPEN (projUnitary_isClopen_of_bargmann_continuous), and the W3 selection fires unconditionally (projectedFlow_unitary_of_bargmann_continuous).

The degenerate dimensions need no datum at all: for N ≤ 1 every transformation of the (at most one-point) projective space is trivially the projective unitary 1 (projUnitary_of_dim_le_one), so together the clopen datum is closed at EVERY N — unconditionally for N ≤ 1, on the scalar continuity datum for N ≥ 2.

Honest posture (load-bearing)

The remaining hypothesis is hcont : Continuous (bargmannObservable d p q r) — continuity IN t of ONE ℂ-valued observable of the flow at THREE fixed probe rays. This is a strictly weaker posit than the compact-open continuity of t ↦ projectedFlow t that (i) named: it follows from it (composing with the continuity of Δ on ℙ³, a true statement whose formalisation needs local sections of mk not present in the corpus — the named follow-on), and it is the exact regularity the selection consumes. A genuine one-parameter physical flow has continuous observables; the posit is physical, not a placeholder for missing mathematics about the isometry group. Nothing here derives continuity from the KahlerOnticSetup fields — measure-preservation does not imply continuity (measure ≠ topology, the same discipline as measure ≠ metric in W3).

Non-vacuity

On trivialKahlerOnticSetup the Bargmann observable is constant, hence continuous; with the N ≥ 2 probe triple the full selection fires (trivialKahlerOnticSetup_bargmann_selection). Genuine, not vacuous.

Provenance

Foundational-triple only (propext, Classical.choice, Quot.sound); no busch, no sorry, no native_decide, no new axioms. Consumes W3 (projectedFlow_unitary_or_antiunitary, projectedFlow_unitary_of_clopen) and the Bargmann layer; Wigner is not re-proved.

The Bargmann observable of the projected flow

noncomputable def CSD.LF4.bargmannObservable {N : ℕ} (d : KahlerOnticSetup N) (p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (t : ℝ) : ℂ

The Bargmann observable of the projected flow along a fixed probe triple: t ↦ Δ(Φ_t p, Φ_t q, Φ_t r). One scalar function of time whose value discriminates the Wigner branches.

Equations

• CSD.LF4.bargmannObservable d p q r t = (d.projectedFlow t p).bargmann (d.projectedFlow t q) (d.projectedFlow t r)

theorem CSD.LF4.bargmannObservable_of_projUnitary {N : ℕ} {d : KahlerOnticSetup N} {t : ℝ} (h : ProjUnitary d t) (p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : bargmannObservable d p q r t = p.bargmann q r

On the unitary branch the Bargmann observable takes the reference value Δ(p,q,r).

theorem CSD.LF4.bargmannObservable_of_projAntiunitary {N : ℕ} {d : KahlerOnticSetup N} {t : ℝ} (h : ProjAntiunitary d t) (p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : bargmannObservable d p q r t = (starRingEnd ℂ) (p.bargmann q r)

On the antiunitary branch the Bargmann observable takes the CONJUGATE reference value conj Δ(p,q,r).

theorem CSD.LF4.not_projUnitary_and_projAntiunitary {N : ℕ} {d : KahlerOnticSetup N} {t : ℝ} {p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (him : (p.bargmann q r).im ≠ 0) (h1 : ProjUnitary d t) (h2 : ProjAntiunitary d t) : False

The Wigner disjunction is exclusive wherever a probe triple with Im Δ ≠ 0 exists: no time-t map is both projectively unitary and projectively antiunitary. (In dimension ≤ 1 both branches DO coincide; Im Δ ≠ 0 is exactly the non-degeneracy that separates them.)

The clopen datum, derived

theorem CSD.LF4.projUnitary_isClopen_of_bargmann_continuous {N : ℕ} (d : KahlerOnticSetup N) (hTPP : ∀ (t : ℝ), Projectivization.TransProbPreserving (d.projectedFlow t)) {p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (him : (p.bargmann q r).im ≠ 0) (hcont : Continuous (bargmannObservable d p q r)) : IsClopen {t : ℝ | ProjUnitary d t}

The W3 clopen datum, DERIVED. For a transition-probability-preserving projected flow whose Bargmann observable along a non-degenerate probe triple is continuous in t, the unitary-time set is clopen: it is the preimage of the closed singleton {Δ₀} and its complement the preimage of {conj Δ₀}, Δ₀ ≠ conj Δ₀ since Im Δ₀ ≠ 0.

The complement step is the load-bearing one, and it is not formal: it needs the two values to be exhaustive. That is supplied by the Wigner dichotomy projectedFlow_unitary_or_antiunitary (from hTPP), together with bargmannObservable_of_projUnitary and bargmannObservable_of_projAntiunitary pinning the observable's value on each branch. This discharges (ii) — the branch separation — outright, and reduces (i) to the scalar continuity hypothesis hcont.

theorem CSD.LF4.projectedFlow_unitary_of_bargmann_continuous {N : ℕ} (d : KahlerOnticSetup N) (hTPP : ∀ (t : ℝ), Projectivization.TransProbPreserving (d.projectedFlow t)) (h0 : ProjUnitary d 0) {p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))} (him : (p.bargmann q r).im ≠ 0) (hcont : Continuous (bargmannObservable d p q r)) (t : ℝ) : ProjUnitary d t

The W3 unitary selection, on the Bargmann continuity datum. For a transition-probability-preserving projected flow that is unitary at t = 0 and whose Bargmann observable along a non-degenerate probe triple is continuous, EVERY time-t map is on the unitary branch. The staged clopen hypothesis of projectedFlow_unitary_of_clopen is now derived, not posited.

The degenerate dimensions (N ≤ 1): no datum needed

theorem CSD.LF4.projectivization_subsingleton {N : ℕ} (hN : N ≤ 1) (p q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : p = q

For N ≤ 1 the projective space has at most one point.

theorem CSD.LF4.projUnitary_of_dim_le_one {N : ℕ} (hN : N ≤ 1) (d : KahlerOnticSetup N) (t : ℝ) : ProjUnitary d t

The degenerate case needs no datum: for N ≤ 1 every self-map of the (at most one-point) projective space — in particular every time-t projected flow map — is realised by the projective unitary 1. Together with the Bargmann route for N ≥ 2, the W3 clopen datum is closed at every N.

Non-vacuity on the trivialKahlerOnticSetup witness

theorem CSD.LF4.trivialKahlerOnticSetup_bargmann_selection {N : ℕ} (hN : 2 ≤ N) (p₀ : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (t : ℝ) : ProjUnitary (trivialKahlerOnticSetup N p₀) t

The Bargmann selection FIRES on the inhabitation witness (N ≥ 2): the identity flow's Bargmann observable is constant (hence continuous), the probe triple exists, t = 0 is unitary, and the conclusion — unitary at every time — is genuine. Confirms the hypotheses of projectedFlow_unitary_of_bargmann_continuous are jointly satisfiable.