The curvature formula on the spin-½ cone: the disc integral is half the solid angle

Category: 3-Local (QM-validity). BACKLOG #54, brick BP-3 of specs/berry-phase-scoping.md, checked on Berry's example.

The cone curve ψ(t) = (cos θ/2, e^{it} sin θ/2) of BerryPhase.lean bounds the disc Ψ(s, t) = (cos(sθ/2), e^{it} sin(sθ/2)), s ∈ [0, 1], t ∈ [0, 2π]: at s = 0 the disc is the north pole, at s = 1 it is the cone curve, and the cut t = 0 ≡ 2π closes with no phase. The curvature 2 Im⟪∂_sΨ, ∂_tΨ⟫ is (θ/2) sin(sθ), and its integral over the disc is π(1 − cos θ), half the solid angle of the cone.

• coneSurface θ, coneSurface_one — the disc, whose outer edge is coneCurve θ; contDiff_coneSurface, norm_coneSurface, the two partial derivatives;
• ★ curvature_coneSurface — the curvature is (θ/2) sin(sθ);
• ★ integral_curvature_coneSurface — its integral over the disc is solidAngle θ / 2;
• ★★ geometricPhase_coneCurve_eq_neg_integral_curvature — the general curvature formula (GeometricPhase.geometricPhase_eq_neg_integral_curvature) applied to the cone;
• ★★ curvature_formula_consistent — the same equation proved the other way, from Berry's direct computation β = −Ω/2 (geometricPhase_coneCurve_solidAngle) and the disc integral: the two derivations agree.

The Fubini–Study reading (BACKLOG #65, 2026-09-28), through Mathlib/Geometry/Manifold/Instances/ProjectiveSpaceGeometricPhase.lean:

• ★ curvature_coneSurface_eq_neg_half_fsPullback — the curvature on this disc is −1/2 of the Fubini–Study form of ℂℙ¹ on the velocities of the projected disc;
• ★★ integral_fsPullback_coneSurface — the form integrates to −Ω over the cap in the dd^c normalisation of fsForm, so ★★ geometricPhase_coneCurve_eq_half_integral_fsPullback: β is half the integral of ω_FS, which is Berry's −Ω/2.

Honest scope

⚠️ One surface, computed directly. Berry's adiabatic setting (BP-5, BACKLOG #56) is CsdLean4/Empirical/QM/BerryAdiabatic.lean; the discrete Aharonov–Bohm ring is BP-4 (#55), CsdLean4/Empirical/QM/AharonovBohm.lean. The ∫∫ here is an iterated interval integral of a function on the rectangle, not an integral of a form over a chain (the corpus defines none).

References: M. V. Berry, Proc. R. Soc. A 392 (1984) 45, §§3, 5; specs/berry-phase-scoping.md; specs/qm-empirical-tests.md ER3; specs/BACKLOG.md #54.

noncomputable def CSD.Empirical.QM.BerryPhase.coneSurface (θ : ℝ) (p : ℝ × ℝ) : EuclideanSpace ℂ (Fin 2)

The disc of the cone: Ψ(s, t) = (cos(sθ/2), e^{it} sin(sθ/2)).

Equations

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

theorem CSD.Empirical.QM.BerryPhase.coneSurface_one (θ t : ℝ) : coneSurface θ (1, t) = coneCurve θ t

The outer edge s = 1 of the disc is the cone curve.

theorem CSD.Empirical.QM.BerryPhase.norm_coneSurface (θ : ℝ) (p : ℝ × ℝ) : ‖coneSurface θ p‖ = 1

theorem CSD.Empirical.QM.BerryPhase.hasDerivAt_toLp_two {f g : ℝ → ℂ} {f' g' : ℂ} {x : ℝ} (hf : HasDerivAt f f' x) (hg : HasDerivAt g g' x) : HasDerivAt (fun (x : ℝ) => !₂[f x, g x]) !₂[f', g'] x

A pair of derivatives of the components gives the derivative of the EuclideanSpace curve.

theorem CSD.Empirical.QM.BerryPhase.hasDerivAt_coneSurface_left (θ s t : ℝ) : HasDerivAt (fun (s : ℝ) => coneSurface θ (s, t)) !₂[-(↑(Real.sin (s * (θ / 2))) * ↑(θ / 2)), Complex.exp (↑t * Complex.I) * (↑(Real.cos (s * (θ / 2))) * ↑(θ / 2))] s

∂_sΨ = (−(θ/2) sin(sθ/2), (θ/2) e^{it} cos(sθ/2)).

theorem CSD.Empirical.QM.BerryPhase.hasDerivAt_coneSurface_right (θ s t : ℝ) : HasDerivAt (fun (t : ℝ) => coneSurface θ (s, t)) !₂[0, Complex.I * Complex.exp (↑t * Complex.I) * ↑(Real.sin (s * (θ / 2)))] t

∂_tΨ = (0, i e^{it} sin(sθ/2)).

theorem CSD.Empirical.QM.BerryPhase.contDiff_coneSurface (θ : ℝ) : ContDiff ℝ 2 (coneSurface θ)

theorem CSD.Empirical.QM.BerryPhase.curvature_coneSurface (θ s t : ℝ) : GeometricPhase.curvature (coneSurface θ) (s, t) = θ / 2 * Real.sin (s * θ)

★ The curvature on the cone's disc is (θ/2) sin(sθ).

theorem CSD.Empirical.QM.BerryPhase.integral_curvature_coneSurface (θ : ℝ) : ∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..2 * Real.pi, GeometricPhase.curvature (coneSurface θ) (s, t) = solidAngle θ / 2

★ The curvature integral over the cone's disc is half the solid angle, π(1 − cos θ).

theorem CSD.Empirical.QM.BerryPhase.geometricPhase_coneCurve_eq_neg_integral_curvature (θ : ℝ) : GeometricPhase.geometricPhase (coneCurve θ) (2 * Real.pi) 0 = -∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..2 * Real.pi, GeometricPhase.curvature (coneSurface θ) (s, t)

★★ The curvature formula on the cone: the general theorem geometricPhase_eq_neg_integral_curvature applied to the disc coneSurface θ.

theorem CSD.Empirical.QM.BerryPhase.curvature_formula_consistent (θ : ℝ) : -∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..2 * Real.pi, GeometricPhase.curvature (coneSurface θ) (s, t) = GeometricPhase.geometricPhase (coneCurve θ) (2 * Real.pi) 0

★★ The two derivations agree: Berry's direct computation β = −Ω/2 (geometricPhase_coneCurve_solidAngle) and the disc integral of the curvature (integral_curvature_coneSurface) give the same equation as the general curvature formula.

The Fubini–Study reading (BACKLOG #65)

Mathlib/Geometry/Manifold/Instances/ProjectiveSpaceGeometricPhase.lean identifies the curvature with the Fubini–Study form of ℂℙⁿ on the velocities of the projected family. Here is that identification on this disc, where the number is Berry's: the form integrates to minus the solid angle over the cap, so half its integral is the geometric phase.

theorem CSD.Empirical.QM.BerryPhase.coneSurface_ne_zero (θ : ℝ) (p : ℝ × ℝ) : coneSurface θ p ≠ 0

The cone's disc is a family of unit vectors, hence never zero.

theorem CSD.Empirical.QM.BerryPhase.curvature_coneSurface_eq_neg_half_fsPullback (θ s t : ℝ) : GeometricPhase.curvature (coneSurface θ) (s, t) = -(1 / 2) * Projectivization.fsPullback (coneSurface θ) ⋯ (s, t)

★ The curvature on the cone's disc is −1/2 of the Fubini–Study form of ℂℙ¹ on the velocities of the projected disc.

theorem CSD.Empirical.QM.BerryPhase.integral_fsPullback_coneSurface (θ : ℝ) : ∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..2 * Real.pi, Projectivization.fsPullback (coneSurface θ) ⋯ (s, t) = -solidAngle θ

★★ The Fubini–Study form integrates to minus the solid angle over the cap. In the dd^c log(1 + ‖z‖²) normalisation of fsForm — whose value at a chart origin is −4 Im⟪·,·⟫ — the pullback of ω_FS along the cone's disc has total integral −Ω, Ω = 2π(1 − cos θ) the solid angle of the cone.

theorem CSD.Empirical.QM.BerryPhase.geometricPhase_coneCurve_eq_half_integral_fsPullback (θ : ℝ) : GeometricPhase.geometricPhase (coneCurve θ) (2 * Real.pi) 0 = 1 / 2 * ∫ (s : ℝ) in 0..1, ∫ (t : ℝ) in 0..2 * Real.pi, Projectivization.fsPullback (coneSurface θ) ⋯ (s, t)

★★ Berry's phase for the cone is half the integral of the Fubini–Study form over the cap — BP-3 in the form the textbooks state it, β = (1/2) ∫∫ [Ψ]^* ω_FS = −Ω/2, with the repository's own fsForm and its own normalisation.