The Aharonov–Bohm effect, read as quantum mechanics #

Category: 3-Local (QM-validity). BACKLOG #55, brick BP-4 of specs/berry-phase-scoping.md; the flux twin specs/qm-empirical-tests.md ER3 asked for.

Glossary: https://glossary.constraintsurfacedynamics.com/aharonov-bohm/ Plain-language, CSD-role and formal statements of the Aharonov-Bohm effect, with this module as the Lean anchor. Kept symmetric by scripts/check-glossary.sh.

Mathlib/QuantumInfo/AharonovBohmRing.lean is the linear algebra: a ring of N sites with Peierls phases, its levels 2 cos((2πm + Φ)/N), its diagonalisation by the discrete Fourier transform, and its gauge covariance. This module reads those theorems as the experiment.

★★ energy_lt_energy_of_flux_lt — the levels move with the flux, strictly and continuously: a spectroscopic measurement on the ring sees Φ, although the field vanishes on every site the electron visits. That is the Aharonov–Bohm effect (Chambers 1960, Tonomura 1986 in the interference form).
★★ oneBond_mulVec_gauge_mode and ★★ same_levels_of_gauge — the vector potential is not observable: put the entire phase on one bond and the levels do not move, because the two rings are the same operator in two gauges.
★★ flux_quantum — the levels see Φ only modulo 2π: flux is measured in units of the quantum, and Φ and Φ + 2π are indistinguishable by any measurement whatsoever.
★★★ flux_not_gauge_artefact — and yet Φ = π is not Φ = 0: no change of basis carries one three-site ring to the other. Both halves of the effect, in one file.
The three-site levels as numbers: levels_three_zero, levels_three_pi — {2, −1, −1} at zero flux and {1, −2, 1} at half a quantum.
★★★ flux_determined_by_spectrum — the general form of the same observability claim: at every ring size, two fluxes with the same level set differ by a whole quantum or are reflections of one another. flux_not_gauge_artefact exhibits one pair that the spectrum tells apart; this says the spectrum tells every pair apart, up to exactly the two invisible operations.
★★★ flux_determined_by_circle_spectrum and ★★ gauge_removable_iff_flux_quantum — the same two halves of the effect in the textbook continuum model, a particle on the circle with the twisted derivative ∂ − iΦ: the levels (n − Φ)² determine the flux modulo a quantum and up to sign, and the gauge factor that removes the twist is single-valued on the circle exactly when the flux is a whole quantum. Mathlib/QuantumInfo/AharonovBohmCircle.lean is the linear algebra.

Honest scope #

⚠️ A lattice ring, not a solenoid: the flux enters through Peierls' substitution, which this model takes as its definition, and "the field vanishes on the ring" is a statement about the model's inputs, not a derived one. No double-slit and no interference pattern (specs/berry-phase-scoping.md BP-4).

⚠️ The two models are analogues, not a limit. The circle statements are proved about the circle, from its own definition of the twist; nothing here derives them as an N → ∞ limit of the ring, and the flux quantum, the levels, and even which end of the spectrum reads the flux all differ between the two. Reading the pair as one effect in two formulations is a judgement about the physics, not a theorem of this corpus.

⚠️ No unbounded-operator theory on the circle side: −(∂ − iΦ)² is iterated differentiation of the Fourier modes, not a self-adjoint operator with a domain, so "the spectrum" there means the set of levels of those modes. QuantumInfo.AharonovBohmCircle.circleMode_eq_fourier identifies them with Mathlib's fourier family, whose completeness in L² is fourierBasis; the step from that to a spectral theorem is not taken.

⚠️ Nothing here is CSD-specific: the module records that the corpus reproduces the effect, which is what the empirical-twin ledger asks of it.

References: Y. Aharonov, D. Bohm, Phys. Rev. 115 (1959) 485; R. G. Chambers, Phys. Rev. Lett. 5 (1960) 3; A. Tonomura et al., Phys. Rev. Lett. 56 (1986) 792; specs/qm-empirical-tests.md ER3; specs/berry-phase-scoping.md BP-4; specs/BACKLOG.md #55.

The flux is determined by the spectrum #

source

theorem CSD.Empirical.QM.AharonovBohm.flux_determined_by_spectrum {N : ℕ} (hN : 0 < N) {Φ Φ' : ℝ} (h : Set.range (QuantumInfo.AharonovBohm.ringEigval N Φ) = Set.range (QuantumInfo.AharonovBohm.ringEigval N Φ')) :

∃ (k : ℤ), Φ' = Φ + 2 * Real.pi * ↑k ∨ Φ' = -Φ + 2 * Real.pi * ↑k

★★★ The flux is observable, in full. A spectroscopic measurement of the ring determines the flux exactly as far as it can be determined: two fluxes with the same level set differ by a whole quantum, or are reflections of one another in a whole quantum. Both of those really are invisible — QuantumInfo.AharonovBohm.range_ringEigval_add_two_pi and QuantumInfo.AharonovBohm.range_ringEigval_neg — so nothing weaker would be true and nothing stronger is available. flux_not_gauge_artefact is the same statement for one concrete pair on the triangle; this is the statement for every pair at every ring size.

The mechanism is that the top of the spectrum is 2 cos(d/N) with d the distance from the flux to the nearest whole quantum, so the highest level falls strictly as the flux moves away from a quantum, and reading it off inverts the relation.

The same effect on the circle #

source

theorem CSD.Empirical.QM.AharonovBohm.flux_determined_by_circle_spectrum {Φ Φ' : ℝ} (h : Set.range (QuantumInfo.AharonovBohmCircle.circleEigval Φ) = Set.range (QuantumInfo.AharonovBohmCircle.circleEigval Φ')) :

∃ (k : ℤ), Φ' = Φ + ↑k ∨ Φ' = -Φ + ↑k

★★★ The flux is observable in the continuum model too. A particle on the circle with the twisted derivative ∂ − iΦ has levels (n − Φ)², and those determine the flux exactly as far as it can be determined: two fluxes with the same level set differ by a whole quantum, or are reflections of one another. The flux quantum here is 1 rather than 2π, and it is the ground level, not the top one, that reads the flux — QuantumInfo.AharonovBohmCircle.isLeast_range_circleEigval — so this is the ring's flux_determined_by_spectrum in a different parametrisation, not an instance of it.

source

theorem CSD.Empirical.QM.AharonovBohm.gauge_removable_iff_flux_quantum (Φ : ℝ) :

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

★★ The vector potential is removable, the flux is not — the continuum form. The gauge factor e^{iΦx} that turns the twisted derivative into the plain one is a function on the circle exactly when the flux is a whole quantum; at any other flux it is multivalued, which is why the levels move. same_levels_of_gauge is the lattice half of the same statement.

The levels move with the flux #

source

theorem CSD.Empirical.QM.AharonovBohm.energy_lt_energy_of_flux_lt {N : ℕ} (hN : 3 ≤ N) {Φ₁ Φ₂ : ℝ} (h0 : 0 ≤ Φ₁) (h12 : Φ₁ < Φ₂) (h2 : Φ₂ ≤ Real.pi * ↑N) :

QuantumInfo.AharonovBohm.ringEigval N Φ₂ 0 < QuantumInfo.AharonovBohm.ringEigval N Φ₁ 0

★★ The flux is observable, continuously. On a ring of N ≥ 3 sites the lowest level 2 cos(Φ/N) falls strictly as the flux grows through [0, πN]: a spectroscopic measurement reads the flux off the ring, although the magnetic field vanishes at every site.

The vector potential is not observable #

source

theorem CSD.Empirical.QM.AharonovBohm.oneBond_mulVec_gauge_mode {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) (m : ℤ) :

(QuantumInfo.AharonovBohm.ringHamOf N (QuantumInfo.AharonovBohm.oneBondPhase N Φ)).mulVec ((QuantumInfo.AharonovBohm.gaugeDiag N (QuantumInfo.AharonovBohm.oneBondGauge N Φ)).conjTranspose.mulVec (QuantumInfo.AharonovBohm.ringMode N ↑m)) = ↑(QuantumInfo.AharonovBohm.ringEigval N Φ m) • (QuantumInfo.AharonovBohm.gaugeDiag N (QuantumInfo.AharonovBohm.oneBondGauge N Φ)).conjTranspose.mulVec (QuantumInfo.AharonovBohm.ringMode N ↑m)

★★ The gauge-transformed modes diagonalise the one-bond ring. Moving the whole Peierls phase onto a single bond moves the eigenvectors by a diagonal unitary and leaves every level where it was.

source

theorem CSD.Empirical.QM.AharonovBohm.same_levels_of_gauge {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) (m : ℤ) :

Module.End.HasEigenvalue (QuantumInfo.AharonovBohm.ringHamOf N (QuantumInfo.AharonovBohm.oneBondPhase N Φ)).mulVecLin ↑(QuantumInfo.AharonovBohm.ringEigval N Φ m)

★★ Redistributing the phase changes no level. Every level of the uniform ring is a level of the ring with the whole phase on one bond, and conversely by QuantumInfo.AharonovBohm.eq_ringEigval_of_mulVec: the two gauges are spectroscopically indistinguishable.

The flux quantum, and what survives it #

source

theorem CSD.Empirical.QM.AharonovBohm.flux_quantum (N : ℕ) (Φ : ℝ) :

Set.range (QuantumInfo.AharonovBohm.ringEigval N (Φ + 2 * Real.pi)) = Set.range (QuantumInfo.AharonovBohm.ringEigval N Φ)

★★ A whole flux quantum is invisible. The set of levels is unchanged by Φ ↦ Φ + 2π: no measurement on the ring distinguishes fluxes differing by a quantum.

source

theorem CSD.Empirical.QM.AharonovBohm.flux_not_gauge_artefact :

¬∃ (U : Matrix (ZMod 3) (ZMod 3) ℂ), U.conjTranspose * U = 1 ∧ U * QuantumInfo.AharonovBohm.ringHam 3 0 * U.conjTranspose = QuantumInfo.AharonovBohm.ringHam 3 Real.pi

★★★ Half a quantum is visible. No change of basis carries the flux-free three-site ring to the ring with flux π: the Aharonov–Bohm phase is physical, not an artefact of the vector potential's gauge.