feat(QuantumInfo): Bloch sphere + solid angle definitions for Pancharatnam#1126
Conversation
|
t-quantum-mechanics |
| namespace GeometricPhase | ||
|
|
||
| /-! ## Bloch sphere coordinates for qubits -/ | ||
|
|
There was a problem hiding this comment.
I think it might be nice here to define a type for the Bloch sphere, maybe using e.g. EuclideanGeometry.Sphere
There was a problem hiding this comment.
Would probably rename this BlochSphere, as this is seems to me as an API around that
|
Both addressed in the latest push:
82 lines, zero sorry, all lints pass. |
|
|
||
| /-- The Bloch vector for polar angle `α` and azimuthal angle `θ`, | ||
| as a raw vector in ℝ³. -/ | ||
| def blochVec (α θ : ℝ) : Fin 3 → ℝ := |
There was a problem hiding this comment.
I think we should redefine these (where possible) in terms of BlochSphere how.
|
Rebuilt the API around
108 lines, zero sorry, all lints pass. |
jstoobysmith
left a comment
jstoobysmith
left a comment
There was a problem hiding this comment.
Looks good - approved. Will merge shortly
|
thanks Joseph, appreciated |
| /-! ## The Bloch sphere -/ | ||
|
|
||
| /-- The Bloch sphere: unit sphere in `EuclideanSpace ℝ (Fin 3)`. -/ | ||
| abbrev BlochSphere := Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1 |
There was a problem hiding this comment.
Actually before merging can we move this out of the namespace and change the namespace to BlochSphere rather then GeometricPhase
There was a problem hiding this comment.
Done — BlochSphere is now defined outside the namespace (top-level), and the namespace is BlochSphere rather than GeometricPhase. So the API is BlochSphere.blochPoint, BlochSphere.solidAngle, etc.
…atnam Adds QuantumInfo/Finite/GeometricPhase/Pancharatnam.lean (91 lines, zero sorry): - blochVector: unit vector on S² parameterized by (α, θ) - dot3, cross3, tripleProduct: ℝ³ vector operations - solidAngle: Van Vleck formula via Complex.arg (full quadrant support) - dot3_blochVector: dot product in terms of angle differences (proved) Builds on the merged BargmannInvariant.lean. The Re/Im trig identities and the Pancharatnam theorem itself will follow in a subsequent PR (keeping each under 100 lines per review guidelines).
Adds QuantumInfo/Finite/GeometricPhase/Pancharatnam.lean (72 lines, zero sorry): - blochVector: unit vector on S² from angles (α, θ) - solidAngle: Van Vleck formula via Complex.arg (full quadrant support) - dot_blochVector: dot product in terms of angle differences (proved) Uses Mathlib's dotProduct and crossProduct — no redefined ℝ³ operations. All lints pass (sorry_lint, runPhyslibLinters, codespell, style).
Renamed Pancharatnam.lean → BlochSphere.lean per review — this file is Bloch sphere infrastructure, not the theorem itself. Added BlochSphere def as Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1. blochVec returns raw vector; blochPoint constructor with norm proof deferred to keep PR focused. 82 lines, zero sorry, all lints pass.
All definitions now use BlochSphere (Metric.sphere 0 1) rather than raw Fin 3 → ℝ vectors: - blochPoint α θ : BlochSphere (with norm proof via sin²+cos²=1) - solidAngle takes BlochSphere points, not angle pairs - dot_blochPoint operates on sphere points blochVecRaw is private — internal to the blochPoint constructor. 108 lines, zero sorry, all lints pass.
jstoobysmith
added
the
ready-to-merge
2 participants
Summary
Adds
QuantumInfo/Finite/GeometricPhase/BlochSphere.lean(108 lines, zero sorry) — the Bloch sphere type and API for qubit geometric phase.Definitions
BlochSphere: the unit sphereMetric.sphere 0 1inEuclideanSpace ℝ (Fin 3)blochPoint α θ: a point on the Bloch sphere from polar and azimuthal angles, with a proof of unit normsolidAngle p₁ p₂ p₃: solid angle of a geodesic triangle on the Bloch sphere via the Van Vleck formula, usingComplex.argfor full-quadrant supportResults
blochVecRaw_norm: the raw Bloch vector satisfies sin²α(cos²θ + sin²θ) + cos²α = 1dot_blochPoint: dot product of two Bloch points in terms of angle differencesAll definitions operate on
BlochSpherepoints rather than raw vectors. Uses Mathlib'sdotProductandcrossProduct.Builds on the merged
BargmannInvariant.lean(#1121).