Aharonov-Bohm effect

An electron that never enters a magnetic field can still be shifted by it, as the enclosed flux changes the interference between paths, which shows that the field's potential carries physics the field strength alone doesn't.

proved in corpus · proved here, no imported axiomsLean flux_not_gauge_artefact
Photograph of Yakir Aharonov seated at a chessboard in a study
Yakir Aharonov, the first name on the effect.Kobi Kalmanovitz, CC BY-SA 3.0, via Wikimedia Commons

In plain terms

Classical electromagnetism describes forces by field strengths, and the potential is treated as a convenience, a bookkeeping function whose absolute value has no meaning since you can add a constant to it without changing anything. Quantum mechanics disagrees, in a way that can be measured.

Send an electron around both sides of a region containing magnetic flux, with the field itself confined so that the electron never touches it. The two paths acquire different phases, the difference being set by the flux they enclose between them, and the interference pattern shifts accordingly. Nothing local explains the shift, as the electron went nowhere the field was.

Both halves of the story matter. The potential is still not observable on its own, as moving the phase around between different parts of the path, which is what changing the potential does, leaves every measurable prediction alone. What's observable is the total enclosed flux, and only up to a fixed unit, since adding one whole quantum of flux is undetectable. So the effect is neither that the potential is real nor that only the field is, but that the right object is the phase accumulated around a closed loop.

In CSD

The effect is one of the empirical twins the programme keeps, so the corpus reproduces it rather than interpreting it, and it does both halves on a lattice ring of sites with the flux entering through the standard phase substitution on the bonds. The levels move strictly and continuously with the flux, so a spectroscopic measurement reads the flux off the ring although the field vanishes at every site the electron visits. Putting the whole phase on a single bond leaves the levels untouched, because the two rings are the same operator in two gauges, and the levels see the flux only up to one quantum.

The sharpest statement is that the two are compatible: half a quantum of flux is genuinely different from none, since no change of basis carries one three-site ring to the other, and yet the potential remains unobservable. The effect also sits next to the geometric phase, being the same holonomy idea with the loop in space rather than in the space of states.

Both halves also hold in the textbook continuum picture, a particle on a circle whose derivative carries the flux as a twist, where the levels are squared distances from each whole number to the flux. There the lowest level reads the flux off, rather than the highest as on the ring, and the gauge factor that removes the twist is a function on the circle only when the flux is a whole quantum, which is why the levels move at all. The honest boundary is that the two pictures are analogues rather than one derived from the other, as nothing takes a limit of large rings, and that this is a ring of sites and a bare circle rather than a solenoid, with no double slit and no interference pattern, and that nothing here is CSD-specific.

Mathematically

The linear algebra is AharonovBohmRing.lean: N sites with Peierls phases, levels 2 cos((2 pi m + Phi)/N), diagonalised by the discrete Fourier transform, with gauge covariance. energy_lt_energy_of_flux_lt is strict monotonicity of the lowest level in the flux on the relevant range; oneBond_mulVec_gauge_mode and same_levels_of_gauge are gauge covariance, as concentrating the phase on one bond is a unitary relabelling; flux_quantum is periodicity in the flux quantum; flux_not_gauge_artefact says the three-site rings at zero and at half a quantum are not related by any change of basis, with the explicit levels levels_three_zero giving {2, -1, -1} and levels_three_pi giving {1, -2, 1}.

exists_eq_of_range_ringEigval_eq closes the observability claim in general: two fluxes with the same level set differ by a whole quantum or are reflections of one another, at every ring size. The top of the spectrum is 2 cos(d/N) with d the distance from the flux to the nearest whole quantum (isGreatest_range_ringEigval), which is strictly decreasing in d, and range_ringEigval_neg shows the sign really is invisible, so that ambiguity is the truth rather than slack in the proof.

The continuum twin is AharonovBohmCircle.lean, on the circle of circumference 2 pi with the twisted derivative: twisted_eigen is the eigenvalue equation for the Fourier modes with levels (n - Phi)^2, isLeast_range_circleEigval identifies the ground level as the squared distance from the flux to the nearest whole number, exists_eq_of_range_circleEigval_eq determines the flux from the levels modulo a quantum and up to sign, and gauge_periodic_iff says the gauge factor is single-valued on the circle exactly when the flux is whole. circleMode_eq_fourier identifies the modes with Mathlib's own Fourier family.

On the circle side the operator is now genuine: CircleSobolev.lean has the twisted Laplacian as a self-adjoint operator on the square-integrable functions, whose spectrum is the closure of those levels, and exists_eq_of_spectrum_twistedOp_eq determines the flux from that spectrum rather than from a chosen list of levels. The identification with the differential operator holds on every twice-differentiable periodic function, which needed the classical fact that differentiating multiplies the nth Fourier coefficient by i n.

The Peierls substitution is the model's definition rather than a derived statement, so the sentence that the field vanishes on the ring is an input. The continuum solenoid and the interference form are not formalised, and the operator statement is not extended from twice-differentiable functions to every element of its domain, which would need a Sobolev embedding the library does not have.

The name

Yakir Aharonov and David Bohm published the effect in 1959 at Bristol, and Werner Ehrenberg and Raymond Siday had found it a decade earlier in 1949 in a paper on electron optics that went unread. Robert Chambers saw it in the laboratory in 1960, and Akira Tonomura's group settled the remaining doubts in 1986 with a toroidal magnet covered in superconductor, so that no stray field could reach the electrons at all.

The effect became the standard argument that gauge potentials are not mere bookkeeping, and the loop phase it identifies is the same object that appears throughout gauge theory as a Wilson loop.

Related entries

Module
CsdLean4/Empirical/QM/AharonovBohm.lean
On the site
The current-claims page lists the established results this empirical reproduction joins
New to this?
explainquantum is a beginners' course in quantum mechanics, which starts from scratch and needs no maths
Background
Aharonov-Bohm, Significance of electromagnetic potentials in the quantum theory (Phys. Rev. 115, 485)

Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.

Part of Constraint-Surface Dynamics · Formalised in csd-lean4.

Privacy policy