The Bargmann invariant on complex projective space

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

The (three-point) Bargmann invariant of rays p, q, r in a complex inner-product space is the normalised triple product

`Δ(p,q,r) = ⟪u,v⟫ ⟪v,w⟫ ⟪w,u⟫ / (‖u‖² ‖v‖² ‖w‖²)`

on representatives u, v, w. Each vector appears once in a conjugate-linear slot and once in a linear slot, so rescaling any representative by c ≠ 0 multiplies the numerator and denominator by the same ‖c‖²: the invariant is well defined on rays. Its modulus is a function of pairwise transition probabilities, but its PHASE is not: Δ is preserved by unitaries and CONJUGATED by the antiunitary conjProj. It is the minimal ray invariant separating the two Wigner branches, which is exactly what the CSD dynamics spine consumes.

Main results

• bargmannVec, bargmann : the vector-level and ray-level invariants, with the well-definedness rewriter bargmann_mk.
• bargmann_smul_unitary : unitaries preserve the invariant.
• bargmann_conjProj : the concrete antiunitary conjProj conjugates it.
• bargmannVec_probe / bargmann_probe : the concrete probe triple (e_i, e_i + e_j, e_i + I·e_j) (for i ≠ j) has Δ = (1 + I)/4, so Im Δ = 1/4 ≠ 0 — the unitary and antiunitary branches are genuinely separated in dimension ≥ 2.
• exists_bargmann_im_ne_zero : for 2 ≤ N there is a probe triple with Im Δ ≠ 0.

Provenance. Needed by the CSD dynamics spine W3 clopen-datum closure (CsdLean4/LF4/BargmannSelection.lean): the sign of Im Δ along the projected flow is a continuous discriminator between the unitary and antiunitary Wigner branches, turning the staged clopen hypothesis into a scalar continuity hypothesis.

Tags

projectivization, Bargmann invariant, Wigner theorem, antiunitary, phase

Vector level

noncomputable def Projectivization.bargmannVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (u v w : E) : ℂ

The vector-level Bargmann triple product, normalised by the squared norms. Each argument appears once as a bra and once as a ket, so the value is invariant under nonzero rescaling of each argument separately (bargmannVec_smul_left etc.), hence descends to rays.

Equations

• Projectivization.bargmannVec u v w = inner ℂ u v * inner ℂ v w * inner ℂ w u / ↑(‖u‖ ^ 2 * ‖v‖ ^ 2 * ‖w‖ ^ 2)

theorem Projectivization.bargmannVec_smul_left {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {c : ℂ} (hc : c ≠ 0) (u v w : E) : bargmannVec (c • u) v w = bargmannVec u v w

Rescaling the first argument by c ≠ 0 leaves bargmannVec unchanged: the numerator picks up conj c * c = ‖c‖² (once from the conjugate-linear slot of ⟪u,v⟫, once from the linear slot of ⟪w,u⟫), cancelling the ‖c‖² in the denominator.

theorem Projectivization.bargmannVec_smul_middle {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {c : ℂ} (hc : c ≠ 0) (u v w : E) : bargmannVec u (c • v) w = bargmannVec u v w

Rescaling the middle argument by c ≠ 0 leaves bargmannVec unchanged.

theorem Projectivization.bargmannVec_smul_right {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {c : ℂ} (hc : c ≠ 0) (u v w : E) : bargmannVec u v (c • w) = bargmannVec u v w

Rescaling the last argument by c ≠ 0 leaves bargmannVec unchanged.

Ray level

noncomputable def Projectivization.bargmann {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] (p q r : Projectivization ℂ E) : ℂ

The Bargmann invariant of three projective points, defined on their canonical representatives. Well-definedness across representative choice is bargmann_mk.

Equations

• p.bargmann q r = Projectivization.bargmannVec p.rep q.rep r.rep

theorem Projectivization.rep_mk_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {v : E} (hv : v ≠ 0) : ∃ (a : ℂˣ), (mk ℂ v hv).rep = a • v

A canonical representative of mk v hv is a nonzero scalar multiple of v. (Local copy of the TransitionProbability helper, which is private.)

theorem Projectivization.bargmann_mk {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] {u v w : E} (hu : u ≠ 0) (hv : v ≠ 0) (hw : w ≠ 0) : (mk ℂ u hu).bargmann (mk ℂ v hv) (mk ℂ w hw) = bargmannVec u v w

Well-definedness rewriter. For arbitrary nonzero representatives, the ray-level Bargmann invariant equals the vector-level triple product.

Transformation laws under the Wigner branches

theorem Projectivization.bargmannVec_toEuclideanLin_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (u v w : EuclideanSpace ℂ (Fin N)) : bargmannVec ((Matrix.toEuclideanLin ↑U) u) ((Matrix.toEuclideanLin ↑U) v) ((Matrix.toEuclideanLin ↑U) w) = bargmannVec u v w

Unitaries preserve the vector-level Bargmann triple product: the inner products are preserved (inner_toEuclideanLin_unitary) and so are the norms.

theorem Projectivization.bargmann_smul_unitary {N : ℕ} (U : ↥(Matrix.unitaryGroup (Fin N) ℂ)) (p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : (U • p).bargmann (U • q) (U • r) = p.bargmann q r

Unitaries preserve the Bargmann invariant.

theorem Projectivization.bargmannVec_conjVec {N : ℕ} (u v w : EuclideanSpace ℂ (Fin N)) : bargmannVec (conjVec u) (conjVec v) (conjVec w) = (starRingEnd ℂ) (bargmannVec u v w)

Coordinatewise conjugation conjugates the vector-level triple product: each inner product is conjugated (conjVec_inner), the norms are fixed (conjVec_norm), and the denominator is real.

theorem Projectivization.bargmann_conjProj {N : ℕ} (p q r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) : p.conjProj.bargmann q.conjProj r.conjProj = (starRingEnd ℂ) (p.bargmann q r)

The antiunitary conjProj conjugates the Bargmann invariant. This is the phase-sensitivity that no function of pairwise transition probabilities can see: it separates the two Wigner branches.

The non-degenerate probe triple

theorem Projectivization.probe_fst_ne_zero {N : ℕ} (i : Fin N) : EuclideanSpace.single i 1 ≠ 0

First probe: the basis ray representative e_i is nonzero.

theorem Projectivization.probe_snd_ne_zero {N : ℕ} {i j : Fin N} (hij : i ≠ j) : EuclideanSpace.single i 1 + EuclideanSpace.single j 1 ≠ 0

Second probe: e_i + e_j is nonzero for i ≠ j (its inner product with e_i is 1).

theorem Projectivization.probe_trd_ne_zero {N : ℕ} {i j : Fin N} (hij : i ≠ j) : EuclideanSpace.single i 1 + Complex.I • EuclideanSpace.single j 1 ≠ 0

Third probe: e_i + I·e_j is nonzero for i ≠ j.

theorem Projectivization.bargmannVec_probe {N : ℕ} {i j : Fin N} (hij : i ≠ j) : bargmannVec (EuclideanSpace.single i 1) (EuclideanSpace.single i 1 + EuclideanSpace.single j 1) (EuclideanSpace.single i 1 + Complex.I • EuclideanSpace.single j 1) = (1 + Complex.I) / 4

The probe value. On the triple (e_i, e_i + e_j, e_i + I·e_j) with i ≠ j, the vector-level Bargmann triple product is (1 + I)/4: the inner products are 1, 1 + I, 1 and the squared norms 1, 2, 2.

theorem Projectivization.bargmann_probe {N : ℕ} {i j : Fin N} (hij : i ≠ j) : (mk ℂ (EuclideanSpace.single i 1) ⋯).bargmann (mk ℂ (EuclideanSpace.single i 1 + EuclideanSpace.single j 1) ⋯) (mk ℂ (EuclideanSpace.single i 1 + Complex.I • EuclideanSpace.single j 1) ⋯) = (1 + Complex.I) / 4

The probe triple separates the branches. The ray-level Bargmann invariant of the probe triple is (1 + I)/4, with imaginary part 1/4 ≠ 0.

theorem Projectivization.exists_bargmann_im_ne_zero {N : ℕ} (hN : 2 ≤ N) : ∃ (p : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (q : Projectivization ℂ (EuclideanSpace ℂ (Fin N))) (r : Projectivization ℂ (EuclideanSpace ℂ (Fin N))), (p.bargmann q r).im ≠ 0

For 2 ≤ N there is a probe triple whose Bargmann invariant has nonzero imaginary part: the two Wigner branches are genuinely separated in dimension at least 2.