Berry's phase for a spin-½ around a cone: minus half the solid angle

Category: 3-Local (QM-validity). BACKLOG #10, brick BP-2 of specs/berry-phase-scoping.md.

The state ψ(t) = (cos θ/2, e^{it} sin θ/2) of a spin-½ precesses once around a cone of half-angle θ on the Bloch sphere as t runs over [0, 2π]; its ray returns to itself with total phase 0. The general theory of Mathlib/Analysis/InnerProductSpace/GeometricPhase.lean gives:

• connectionForm_coneCurve — the connection form along the curve is the constant sin²(θ/2);
• coneCurve_cyclic — the curve is cyclic with total phase 0;
• ★★ geometricPhase_coneCurve — the geometric phase is −2π sin²(θ/2) = −π(1 − cos θ), minus half the solid angle 2π(1 − cos θ) of the cone (geometricPhase_coneCurve_solidAngle) — Berry's 1984 result for spin-½, the phase Tomita–Chiao measured with light in a coiled fibre.

Honest scope

⚠️ One curve, computed directly (its disc and the curvature formula are BerryPhaseCurvature.lean). The adiabatic setting — a spin in a slowly rotating field, where this curve is the instantaneous eigenvector and the phase is what the evolution actually accumulates — is BerryAdiabatic.lean (BP-5, BACKLOG #56, done 2026-09-28): fieldHam_mulVec_coneCurve identifies the loop, and norm_inner_state_sub_exp_le recovers −π(1 − cos θ) as the geometric part of the phase after one turn. The curve here is also the Schrödinger evolution generated by H = diag(0, −1), but that reading is not stated here.

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §5; A. Tomita, R. Chiao, PRL 57 (1986) 937; specs/berry-phase-scoping.md; specs/qm-empirical-tests.md ER3.

noncomputable def CSD.Empirical.QM.BerryPhase.coneCurve (θ t : ℝ) : EuclideanSpace ℂ (Fin 2)

The spin-½ state precessing around a cone of half-angle θ: (cos θ/2, e^{it} sin θ/2).

Equations

• CSD.Empirical.QM.BerryPhase.coneCurve θ t = !₂[↑(Real.cos (θ / 2)), Complex.exp (↑t * Complex.I) * ↑(Real.sin (θ / 2))]

noncomputable def CSD.Empirical.QM.BerryPhase.solidAngle (θ : ℝ) : ℝ

The solid angle of the cone of half-angle θ: 2π(1 − cos θ).

Equations

• CSD.Empirical.QM.BerryPhase.solidAngle θ = 2 * Real.pi * (1 - Real.cos θ)

theorem CSD.Empirical.QM.BerryPhase.hasDerivAt_coneCurve (θ t : ℝ) : HasDerivAt (coneCurve θ) !₂[0, Complex.I * Complex.exp (↑t * Complex.I) * ↑(Real.sin (θ / 2))] t

The derivative of the cone curve: (0, i e^{it} sin θ/2).

theorem CSD.Empirical.QM.BerryPhase.norm_coneCurve (θ t : ℝ) : ‖coneCurve θ t‖ = 1

theorem CSD.Empirical.QM.BerryPhase.contDiff_coneCurve (θ : ℝ) : ContDiff ℝ 1 (coneCurve θ)

theorem CSD.Empirical.QM.BerryPhase.connectionForm_coneCurve (θ t : ℝ) : GeometricPhase.connectionForm (coneCurve θ) t = Real.sin (θ / 2) ^ 2

The connection form along the cone curve is the constant sin²(θ/2).

theorem CSD.Empirical.QM.BerryPhase.coneCurve_cyclic (θ : ℝ) : coneCurve θ (2 * Real.pi) = Complex.exp (↑0 * Complex.I) • coneCurve θ 0

The cone curve is cyclic over [0, 2π] with total phase 0.

theorem CSD.Empirical.QM.BerryPhase.geometricPhase_coneCurve (θ : ℝ) : GeometricPhase.geometricPhase (coneCurve θ) (2 * Real.pi) 0 = -Real.pi * (1 - Real.cos θ)

★★ Berry's phase for the spin-½ cone: −2π sin²(θ/2) = −π(1 − cos θ).

theorem CSD.Empirical.QM.BerryPhase.geometricPhase_coneCurve_solidAngle (θ : ℝ) : GeometricPhase.geometricPhase (coneCurve θ) (2 * Real.pi) 0 = -(solidAngle θ / 2)

★★ The geometric phase is minus half the solid angle of the cone.