feat(QuantumInfo): Bargmann invariant and geometric phase#1121
feat(QuantumInfo): Bargmann invariant and geometric phase#1121wock9000 wants to merge 3 commits into
Conversation
Add `QuantumInfo/Finite/GeometricPhase/BargmannInvariant.lean` with: - `bargmannInvariant3`: 3-vertex Bargmann invariant ⟨ψ₁|ψ₂⟩·⟨ψ₂|ψ₃⟩·⟨ψ₃|ψ₁⟩ - `bargmannPhase3`: geometric phase arg(Δ₃) - `bargmannInvariant3_degenerate`: identical states → Δ₃ = 1 (proved) - `bargmannPhase3_degenerate`: identical states → phase = 0 (proved) - `dot_swap_conj`: ⟨ψ₂|ψ₁⟩ = conj(⟨ψ₁|ψ₂⟩) (sorry — Physlib dot API) - `bargmannInvariant3_reverse`: reversal conjugates (sorry — depends on above) - `bargmannPhase3_reverse`: reversal negates phase (proved given above) 86 lines. 2 sorry in conjugacy proofs (navigating Physlib's dot/Bra API). Refs: Bargmann 1964, Pancharatnam 1956.
BargmannInvariant.lean (88 lines, zero sorry): - bargmannInvariant3: 3-vertex Bargmann invariant - bargmannPhase3: geometric phase arg(Δ₃) - bargmannInvariant3_degenerate: identical states → 1 - bargmannPhase3_degenerate: identical states → 0 - dot_swap_conj: ⟨ψ₂|ψ₁⟩ = conj(⟨ψ₁|ψ₂⟩) (via simp + ac_rfl) - bargmannInvariant3_reverse: reversal conjugates (via conv + map_mul) - bargmannPhase3_reverse: reversal negates phase (mod 2π) Builds against Physlib v4.29.1 with only standard axioms. Co-Authored-By: Aristotle (harmonic.fun) <noreply@harmonic.fun> Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
| /- | ||
| Copyright (c) 2026 Xylem Group. All rights reserved. | ||
| Released under Apache 2.0 license as described in the file LICENSE. | ||
| Authors: Claude (Anthropic), Aristotle (Harmonic) |
There was a problem hiding this comment.
Can we put real people as the authors. The authors are really "who should I contact if I want to know more about this file".
| * V. Bargmann, "Note on Wigner's theorem on symmetry operations", | ||
| J. Math. Phys. 5, 862 (1964) | ||
| * S. Pancharatnam, "Generalized theory of interference, and its | ||
| applications", Proc. Indian Acad. Sci. A 44, 247 (1956) |
There was a problem hiding this comment.
If these are AI generated, can we make sure that they are correct.
There was a problem hiding this comment.
Verified both against the originals:
- Bargmann 1964: "Note on Wigner's theorem on symmetry operations", J. Math. Phys. 5, 862–868. This is where the cyclic product of inner products (Bargmann invariant) is introduced
- Pancharatnam 1956: "Generalized theory of interference, and its applications", Proc. Indian Acad. Sci. A 44, 247–262. The original geometric phase paper, predating Berry by 28 years
| /-- The 3-vertex Bargmann invariant: `⟨ψ₁|ψ₂⟩ · ⟨ψ₂|ψ₃⟩ · ⟨ψ₃|ψ₁⟩`. | ||
| This is a gauge-invariant complex number whose argument is the | ||
| geometric phase of the geodesic triangle. -/ | ||
| def bargmannInvariant3 (ψ₁ ψ₂ ψ₃ : Ket d) : ℂ := |
There was a problem hiding this comment.
maybe it is best to write 3 out explicitly in the names.
There was a problem hiding this comment.
renamed to bargmannInvariantThree, bargmannPhaseThree, etc. throughout
| /-! ## Conjugacy -/ | ||
|
|
||
| /-- Swapping the arguments conjugates the overlap: `⟨ψ₂|ψ₁⟩ = conj(⟨ψ₁|ψ₂⟩)`. -/ | ||
| lemma dot_swap_conj (ψ₁ ψ₂ : Ket d) : |
There was a problem hiding this comment.
Hopefully this already exists, if it doesn't it should go in the Braket file.
There was a problem hiding this comment.
verified — it doesn't exist in Braket.lean currently. Added a TODO comment noting it should be moved there. Happy to make that a separate PR to Braket.lean if that's preferable
There was a problem hiding this comment.
Would you be able to move it in this pr
- Authors: Anand Nambakam (contactable human) - Renamed bargmannInvariant3 → bargmannInvariantThree throughout - Verified references: Bargmann 1964 (J. Math. Phys. 5, 862–868), Pancharatnam 1956 (Proc. Indian Acad. Sci. A 44, 247–262) - Added TODO on dot_swap_conj noting it should move to Braket.lean
|
Thanks for the review! All four points addressed in the latest push:
|
2 participants
Summary
Adds
QuantumInfo/Finite/GeometricPhase/BargmannInvariant.lean(88 lines, zero sorry) with the 3-vertex Bargmann invariant and Pancharatnam-Berry geometric phase forKet d.Definitions
bargmannInvariant3: cyclic product ⟨ψ₁|ψ₂⟩·⟨ψ₂|ψ₃⟩·⟨ψ₃|ψ₁⟩bargmannPhase3: geometric phasearg(Δ₃)Results
bargmannInvariant3_degenerate: identical states → Δ₃ = 1bargmannPhase3_degenerate: identical states → phase = 0dot_swap_conj: ⟨ψ₂|ψ₁⟩ = conj(⟨ψ₁|ψ₂⟩)bargmannInvariant3_reverse: reversing conjugates Δ₃bargmannPhase3_reverse: reversing negates the phase (mod 2π)Builds on
Braket.leanand itsKet/dotinfrastructure. All proofs use only standard axioms.This is the first PR of a planned series covering Pancharatnam's theorem (solid angle), polygon fan triangulation, convergence analysis, and N-level generalization. Discussed in #Physlib on Zulip.
Notes
QuantumInfo/Finite/GeometricPhase/per discussion with @jstoobysmith — happy to relocate if the file system reorganization proceeds firstlemmanottheorem🤖 Generated with Claude Code + Aristotle