The Aharonov–Bohm effect on the circle

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #90, the continuum residue of #55.

QuantumInfo/AharonovBohmRing.lean is the lattice version: N sites, levels 2 cos((2πm + Φ)/N), and the flux visible modulo a quantum and up to sign. This is the textbook continuum version on the circle ℝ/2πℤ, where the twisted Hamiltonian (−i∂ − Φ)² = −(∂ − iΦ)² has the Fourier modes ψ_n(x) = e^{inx} as its eigenfunctions with levels (n − Φ)², the flux quantum is 1, and the same two operations are invisible.

• circleMode n — the Fourier mode, with ★ circleMode_eq_fourier identifying it with Mathlib's fourier n on AddCircle (2π) and circleMode_periodic its periodicity;
• ★★ twisted_deriv_circleMode — (∂ − iΦ)ψ_n = i(n − Φ)ψ_n, and ★★★ twisted_eigen — −(∂ − iΦ)²ψ_n = (n − Φ)²ψ_n, the eigenvalue equation written out;
• circleEigval Φ n = (n − Φ)²; ★★ isLeast_range_circleEigval — the ground level is the squared distance from the flux to the nearest quantum, attained at the mode round Φ;
• ★★ range_circleEigval_add_one and ★★ range_circleEigval_neg — one whole quantum, and reversing the flux, permute the levels;
• ★★★ exists_eq_of_range_circleEigval_eq — and those are the only two: two fluxes with the same level set differ by a whole quantum or are reflections of one another;
• ★★ gauge_periodic_iff — the gauge that removes the flux lives on the circle only when the flux is a whole quantum, which is the continuum form of "the vector potential is not observable but the flux is".

Honest scope

⚠️ No unbounded-operator theory. −(∂ − iΦ)² is written out as iterated derivatives of a specific smooth function, not as a self-adjoint operator on L²(S¹) with a domain. The pin has the skeleton — LinearPMap, its adjoint, IsSelfAdjoint — and nothing built on it: Mathlib has no diagonal multiplication operator on a Hilbert basis and no spectrum of one (MATHLIB-ABSENT(LinearPMap.diagonal, LinearPMap.spectrum)), and no unbounded spectral theory to put them in (MATHLIB-ABSENT(file:Mathlib/Analysis/InnerProductSpace/UnboundedSpectrum)). So "spectrum" here means the set of eigenvalues of the Fourier modes, Set.range (circleEigval Φ), and every theorem below is about that set.

⚠️ The missing layer is built, elsewhere. As of 2026-09-30 the operator statements this module does not make are made in CircleSobolev.lean (BACKLOG.md #93, closed): twistedOp Φ is −(∂ − iΦ)² on L²(ℝ/2πℤ) as the diagonal operator of these levels, ★★★ isSelfAdjoint_twistedOp and ★★★ spectrum_twistedOp give self-adjointness and the honest spectrum, ★★★ twistedOp_toL2 shows it acts on every C² periodic function exactly as the differential operator does, and ★★★ exists_eq_of_spectrum_twistedOp_eq is the determination theorem below with spectrum in place of level set. What stays true of this module is what it says: the eigenvalue equation here is pointwise on the modes, and Set.range (circleEigval Φ) is a level set, not a spectrum. circleMode_eq_fourier is the bridge that makes the family Mathlib's own: fourierBasis is a Hilbert basis of L²(AddCircle 2π), so the modes are complete and the twist does not change them — only their levels — but the step from that to "these are all the spectral values of a self-adjoint operator" is not taken here.

⚠️ The flux quantum is 1 in this parametrisation, where the ring module's is 2π; the levels are (n − Φ)² rather than 2 cos((2πm + Φ)/N), and the ground level rather than the top level is what reads the flux. The two statements are analogues, not instances of one another.

⚠️ No solenoid and no double slit here either: the flux enters as the twist in the derivative, which is the minimal-coupling substitution taken as the definition of the model.

References: Y. Aharonov, D. Bohm, Phys. Rev. 115 (1959) 485; the lattice twin in QuantumInfo/AharonovBohmRing.lean and its empirical reading in Empirical/QM/AharonovBohm.lean; specs/berry-phase-scoping.md BP-4; specs/BACKLOG.md #90.

The Fourier modes of the circle

noncomputable def QuantumInfo.AharonovBohmCircle.circleMode (n : ℤ) (x : ℝ) : ℂ

The Fourier mode ψ_n(x) = e^{inx}, a function on ℝ of period 2π.

Equations

• QuantumInfo.AharonovBohmCircle.circleMode n x = Complex.exp (↑n * ↑x * Complex.I)

theorem QuantumInfo.AharonovBohmCircle.circleMode_eq_fourier (n : ℤ) (x : ℝ) : (fourier n) ↑x = circleMode n x

★ The modes are Mathlib's Fourier family on AddCircle (2π), so fourierBasis applies to them: they are a Hilbert basis of L² and the twist below does not change them.

theorem QuantumInfo.AharonovBohmCircle.circleMode_periodic (n : ℤ) (x : ℝ) : circleMode n (x + 2 * Real.pi) = circleMode n x

The modes have period 2π.

theorem QuantumInfo.AharonovBohmCircle.circleMode_ne_zero (n : ℤ) (x : ℝ) : circleMode n x ≠ 0

theorem QuantumInfo.AharonovBohmCircle.hasDerivAt_circleMode (n : ℤ) (x : ℝ) : HasDerivAt (circleMode n) (Complex.I * ↑n * circleMode n x) x

The derivative of a mode: ψ_n' = i n ψ_n.

theorem QuantumInfo.AharonovBohmCircle.deriv_circleMode (n : ℤ) (x : ℝ) : deriv (circleMode n) x = Complex.I * ↑n * circleMode n x

The twisted derivative and the levels

noncomputable def QuantumInfo.AharonovBohmCircle.circleEigval (Φ : ℝ) (n : ℤ) : ℝ

The level of the mode n at flux Φ.

Equations

• QuantumInfo.AharonovBohmCircle.circleEigval Φ n = (↑n - Φ) ^ 2

theorem QuantumInfo.AharonovBohmCircle.twisted_deriv_circleMode (Φ : ℝ) (n : ℤ) (x : ℝ) : deriv (circleMode n) x - Complex.I * ↑Φ * circleMode n x = Complex.I * ↑(↑n - Φ) * circleMode n x

★★ The twisted derivative of a mode: (∂ − iΦ)ψ_n = i(n − Φ)ψ_n. The twist shifts the label by the flux, which is the whole of the Aharonov–Bohm effect in one line.

theorem QuantumInfo.AharonovBohmCircle.hasDerivAt_twisted_circleMode (Φ : ℝ) (n : ℤ) (x : ℝ) : HasDerivAt (fun (y : ℝ) => deriv (circleMode n) y - Complex.I * ↑Φ * circleMode n y) (Complex.I * ↑(↑n - Φ) * (Complex.I * ↑n * circleMode n x)) x

The twisted derivative of a mode is a constant multiple of it, so it can be differentiated again.

theorem QuantumInfo.AharonovBohmCircle.twisted_eigen (Φ : ℝ) (n : ℤ) (x : ℝ) : -(deriv (fun (y : ℝ) => deriv (circleMode n) y - Complex.I * ↑Φ * circleMode n y) x - Complex.I * ↑Φ * (deriv (circleMode n) x - Complex.I * ↑Φ * circleMode n x)) = ↑(circleEigval Φ n) * circleMode n x

★★★ The eigenvalue equation: −(∂ − iΦ)²ψ_n = (n − Φ)²ψ_n. The flux shifts every level by shifting the label it is measured from, and no level is left where it was unless the shift is a whole quantum.

The flux is determined by the levels

theorem QuantumInfo.AharonovBohmCircle.sq_sub_round_le_circleEigval (Φ : ℝ) (n : ℤ) : (Φ - ↑(round Φ)) ^ 2 ≤ circleEigval Φ n

★ No mode sits lower: the ground level is the squared distance from the flux to the nearest whole quantum.

theorem QuantumInfo.AharonovBohmCircle.circleEigval_round (Φ : ℝ) : circleEigval Φ (round Φ) = (Φ - ↑(round Φ)) ^ 2

The ground level is attained, at the mode nearest the flux.

theorem QuantumInfo.AharonovBohmCircle.isLeast_range_circleEigval (Φ : ℝ) : IsLeast (Set.range (circleEigval Φ)) ((Φ - ↑(round Φ)) ^ 2)

★★ The ground level reads the flux: it is the squared distance from the flux to the nearest whole quantum, attained at the mode nearest it.

theorem QuantumInfo.AharonovBohmCircle.range_circleEigval_add_one (Φ : ℝ) : Set.range (circleEigval (Φ + 1)) = Set.range (circleEigval Φ)

★★ One whole quantum changes nothing: adding 1 to the flux permutes the levels.

theorem QuantumInfo.AharonovBohmCircle.range_circleEigval_neg (Φ : ℝ) : Set.range (circleEigval (-Φ)) = Set.range (circleEigval Φ)

★★ The levels cannot see the sign of the flux, so the ambiguity below is real.

theorem QuantumInfo.AharonovBohmCircle.exists_eq_of_sq_sub_round_eq {Φ Φ' : ℝ} (hsq : (Φ - ↑(round Φ)) ^ 2 = (Φ' - ↑(round Φ')) ^ 2) : ∃ (k : ℤ), Φ' = Φ + ↑k ∨ Φ' = -Φ + ↑k

★★★ The flux is determined by the levels, exactly as far as it can be: two fluxes with the same level set differ by a whole quantum, or are reflections of one another in one. With range_circleEigval_add_one and range_circleEigval_neg the converse holds too, so this is the continuum twin of the ring's exists_eq_of_range_ringEigval_eq.

theorem QuantumInfo.AharonovBohmCircle.exists_eq_of_range_circleEigval_eq {Φ Φ' : ℝ} (h : Set.range (circleEigval Φ) = Set.range (circleEigval Φ')) : ∃ (k : ℤ), Φ' = Φ + ↑k ∨ Φ' = -Φ + ↑k

The gauge that removes the flux

noncomputable def QuantumInfo.AharonovBohmCircle.gaugeMode (Φ x : ℝ) : ℂ

The gauge factor e^{iΦx} that turns the twisted derivative into the plain one.

Equations

• QuantumInfo.AharonovBohmCircle.gaugeMode Φ x = Complex.exp (↑Φ * ↑x * Complex.I)

theorem QuantumInfo.AharonovBohmCircle.gauge_periodic_iff (Φ : ℝ) : (∀ (x : ℝ), gaugeMode Φ (x + 2 * Real.pi) = gaugeMode Φ x) ↔ ∃ (k : ℤ), Φ = ↑k

★★ The vector potential is removable, the flux is not. The gauge factor that undoes the twist is a function on the circle exactly when the flux is a whole quantum; for any other flux it is multivalued, which is why the levels move.