The Aharonov–Bohm effect on a ring of N sites

Category: 1-Mathlib (CSD-free; staged for upstream). BACKLOG #55, brick BP-4 of specs/berry-phase-scoping.md.

A tight-binding ring of N sites threaded by a magnetic flux Φ: the amplitude to hop from j to j + 1 carries the Peierls phase e^{i a j}, and the flux is the phase accumulated around the loop, Φ = ∑ⱼ a j. The whole Aharonov–Bohm effect is two theorems about this matrix:

• the vector potential is not observable — the individual bond phases can be moved around at will by a diagonal unitary (★★ gaugeDiag_conj_ringHamOf), and every such move leaves the total flux alone (★ flux_gauge); in particular the uniform ring is unitarily equivalent to the ring with the whole phase on one bond (★★★ gaugeDiag_conj_ringHam_oneBond);
• the flux is observable — the spectrum is 2 cos((2πm + Φ)/N), which moves with Φ (★★ ringHam_mulVec_ringMode, ★★ dftMatrix_conj_ringHam), and no unitary conjugation can undo that: ★★★ not_exists_unitary_conj_ringHam exhibits two fluxes on a three-site ring whose rings are not unitarily equivalent.

The spectrum depends on Φ only modulo 2π (★ ringEigval_add_two_pi, ★★ range_ringEigval_add_two_pi): flux is measured in units of the quantum 2π. That is the whole of the ambiguity, and the converse holds: ★★★ exists_eq_of_range_ringEigval_eq — 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(fluxDist Φ / N) (★★★ isGreatest_range_ringEigval), a strictly decreasing function of the distance from the flux to the nearest whole quantum, so the spectrum reads that distance off and nothing else.

Main declarations

• ringHamOf N a — the ring with bond phases a; ringHam N Φ — the uniform ring a ≡ Φ/N; flux a = ∑ⱼ a j with flux_ringHam; ringHamOf_isHermitian (for 3 ≤ N);
• ringMode N k — the twisted Fourier mode ψ_k(j) = e^{−2πi jk/N}; ringEigval N Φ m;
• ★★ ringHam_mulVec_ringMode — the modes are eigenvectors with eigenvalue 2 cos((2πm + Φ)/N), m any integer label; ★ hasEigenvalue_ringHam;
• dftMatrix N — the unitary discrete Fourier matrix (★ dftMatrix_conjTranspose_mul), and ★★ dftMatrix_conj_ringHam — the ring Hamiltonian is diagonalised by the discrete Fourier transform, so ★★ eq_ringEigval_of_mulVec — those numbers are the whole spectrum;
• ★★ gaugeDiag_conj_ringHamOf, ★ flux_gauge, ★★★ gaugeDiag_conj_ringHam_oneBond;
• ★★★ not_exists_unitary_conj_ringHam;
• fluxDist Φ — the distance from Φ to the nearest whole quantum, with ★ fluxDist_le_abs (nothing is nearer) and ★ fluxDist_le_pi; ★★ ringEigval_le and ★★ ringEigval_neg_round (the top level and the label that attains it), ★★★ isGreatest_range_ringEigval, ★★★ fluxDist_eq_of_range_eq, ★★ range_ringEigval_neg (the sign is invisible, so the ambiguity below is real) and ★★★ exists_eq_of_range_ringEigval_eq.

Honest scope

⚠️ Finite-dimensional: a ring of N ≥ 3 sites, which is the lattice Aharonov–Bohm effect. The continuum version on L²(S¹) — the operator −(∂ − iΦ)² with spectrum (n − Φ)² — is not here and is not claimed (specs/berry-phase-scoping.md BP-4 says why: it is CV-scale).

⚠️ No solenoid, no vector potential as a 1-form, no double slit: the flux enters as the phase of the hopping amplitudes, which is Peierls' substitution taken as the definition of the model.

⚠️ The determination theorem compares level sets, Set.range (ringEigval N ·). It says nothing about multiplicities, and nothing about what a finite number of measurements with finite resolution could distinguish.

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; R. Peierls, Z. Phys. 80 (1933) 763; specs/berry-phase-scoping.md BP-4; specs/BACKLOG.md #55; specs/future-work.md.

The ring and its flux

noncomputable def QuantumInfo.AharonovBohm.ringHamOf (N : ℕ) (a : ZMod N → ℝ) : Matrix (ZMod N) (ZMod N) ℂ

The tight-binding ring of N sites with Peierls phases: a j is the phase of the hop from site j to site j + 1, so the matrix element ⟨j + 1|H|j⟩ is e^{i a j} and the Hamiltonian is Hermitian.

Equations

• One or more equations did not get rendered due to their size.

def QuantumInfo.AharonovBohm.flux (N : ℕ) [Fintype (ZMod N)] (a : ZMod N → ℝ) : ℝ

The flux threading the ring: the phase accumulated once around it.

Equations

• QuantumInfo.AharonovBohm.flux N a = ∑ j : ZMod N, a j

noncomputable def QuantumInfo.AharonovBohm.ringHam (N : ℕ) (Φ : ℝ) : Matrix (ZMod N) (ZMod N) ℂ

The uniform gauge: the flux Φ shared equally among the N bonds.

Equations

• QuantumInfo.AharonovBohm.ringHam N Φ = QuantumInfo.AharonovBohm.ringHamOf N fun (x : ZMod N) => Φ / ↑N

theorem QuantumInfo.AharonovBohm.flux_ringHam {N : ℕ} [NeZero N] (Φ : ℝ) : (flux N fun (x : ZMod N) => Φ / ↑N) = Φ

theorem QuantumInfo.AharonovBohm.two_ne_zero {N : ℕ} (hN : 3 ≤ N) : 2 ≠ 0

A ring with at least three sites has 2 ≠ 0 in its site group.

theorem QuantumInfo.AharonovBohm.sub_one_ne_add_one {N : ℕ} (hN : 3 ≤ N) (i : ZMod N) : i - 1 ≠ i + 1

On a ring with at least three sites the two neighbours of a site are distinct.

theorem QuantumInfo.AharonovBohm.self_ne_add_two {N : ℕ} (hN : 3 ≤ N) (i : ZMod N) : i ≠ i + 2

On a ring with at least three sites a site is not its own second neighbour.

theorem QuantumInfo.AharonovBohm.ringHamOf_apply_of_ne {N : ℕ} {a : ZMod N → ℝ} {i j : ZMod N} (h1 : i ≠ j + 1) (h2 : j ≠ i + 1) : ringHamOf N a i j = 0

theorem QuantumInfo.AharonovBohm.ringHamOf_apply_succ {N : ℕ} (a : ZMod N → ℝ) (j : ZMod N) : ringHamOf N a (j + 1) j = Complex.exp (↑(a j) * Complex.I)

theorem QuantumInfo.AharonovBohm.ringHamOf_apply_pred {N : ℕ} (hN : 3 ≤ N) (a : ZMod N → ℝ) (j : ZMod N) : ringHamOf N a j (j + 1) = (starRingEnd ℂ) (Complex.exp (↑(a j) * Complex.I))

theorem QuantumInfo.AharonovBohm.ringHamOf_isHermitian {N : ℕ} (hN : 3 ≤ N) (a : ZMod N → ℝ) : (ringHamOf N a).IsHermitian

★ The ring Hamiltonian is Hermitian.

The twisted Fourier modes

noncomputable def QuantumInfo.AharonovBohm.ringMode (N : ℕ) [NeZero N] (k : ZMod N) : ZMod N → ℂ

The twisted Fourier mode ψ_k(j) = e^{−2πi jk/N} (the discrete-Fourier convention).

Equations

• QuantumInfo.AharonovBohm.ringMode N k j = ZMod.stdAddChar (-(j * k))

@[simp]

theorem QuantumInfo.AharonovBohm.ringMode_zero {N : ℕ} [NeZero N] (k : ZMod N) : ringMode N k 0 = 1

theorem QuantumInfo.AharonovBohm.ringMode_ne_zero {N : ℕ} [NeZero N] (k : ZMod N) : ringMode N k ≠ 0

theorem QuantumInfo.AharonovBohm.ringMode_sub_one {N : ℕ} [NeZero N] (k j : ZMod N) : ringMode N k (j - 1) = ringMode N k j * ZMod.stdAddChar k

theorem QuantumInfo.AharonovBohm.ringMode_add_one {N : ℕ} [NeZero N] (k j : ZMod N) : ringMode N k (j + 1) = ringMode N k j * ZMod.stdAddChar (-k)

theorem QuantumInfo.AharonovBohm.stdAddChar_neg_eq_conj {N : ℕ} [NeZero N] (k : ZMod N) : ZMod.stdAddChar (-k) = (starRingEnd ℂ) (ZMod.stdAddChar k)

The standard character at −k is the conjugate of the character at k: its values are on the unit circle.

noncomputable def QuantumInfo.AharonovBohm.ringEigval (N : ℕ) (Φ : ℝ) (m : ℤ) : ℝ

The eigenvalue attached to the integer label m: 2 cos((2πm + Φ)/N).

Equations

• QuantumInfo.AharonovBohm.ringEigval N Φ m = 2 * Real.cos ((2 * Real.pi * ↑m + Φ) / ↑N)

theorem QuantumInfo.AharonovBohm.bondPhase_mul_stdAddChar {N : ℕ} [NeZero N] (Φ : ℝ) (m : ℤ) : Complex.exp (↑(Φ / ↑N) * Complex.I) * ZMod.stdAddChar ↑m = Complex.exp (↑((2 * Real.pi * ↑m + Φ) / ↑N) * Complex.I)

The uniform bond phase times the character at an integer label is a single exponential.

theorem QuantumInfo.AharonovBohm.ringHam_mulVec_ringMode {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) (m : ℤ) : (ringHam N Φ).mulVec (ringMode N ↑m) = ↑(ringEigval N Φ m) • ringMode N ↑m

★★ The twisted modes are the eigenvectors of the ring, with eigenvalue 2 cos((2πm + Φ)/N) for any integer label m of the mode. This is the Aharonov–Bohm spectrum: the flux shifts every level, and it does so continuously.

The flux quantum: the spectrum sees Φ only modulo 2π

theorem QuantumInfo.AharonovBohm.ringEigval_add_two_pi {N : ℕ} (Φ : ℝ) (m : ℤ) : ringEigval N (Φ + 2 * Real.pi) m = ringEigval N Φ (m + 1)

theorem QuantumInfo.AharonovBohm.ringEigval_add_card {N : ℕ} [NeZero N] (Φ : ℝ) (m : ℤ) : ringEigval N Φ (m + ↑N) = ringEigval N Φ m

theorem QuantumInfo.AharonovBohm.range_ringEigval_add_two_pi {N : ℕ} (Φ : ℝ) : Set.range (ringEigval N (Φ + 2 * Real.pi)) = Set.range (ringEigval N Φ)

★★ One flux quantum changes nothing. Adding 2π to the flux permutes the levels — the spectrum, as a set, is invariant.

theorem QuantumInfo.AharonovBohm.hasEigenvalue_ringHam {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) (m : ℤ) : Module.End.HasEigenvalue (ringHam N Φ).mulVecLin ↑(ringEigval N Φ m)

★ The levels of the ring are eigenvalues of its Hamiltonian, as Module.End.HasEigenvalue.

Gauge transformations: the vector potential is not observable

noncomputable def QuantumInfo.AharonovBohm.gaugeDiag (N : ℕ) (g : ZMod N → ℝ) : Matrix (ZMod N) (ZMod N) ℂ

A gauge transformation of the ring: the diagonal unitary diag(e^{i g j}).

Equations

• QuantumInfo.AharonovBohm.gaugeDiag N g = Matrix.diagonal fun (j : ZMod N) => Complex.exp (↑(g j) * Complex.I)

theorem QuantumInfo.AharonovBohm.conj_exp_mul_I (u : ℝ) : (starRingEnd ℂ) (Complex.exp (↑u * Complex.I)) = Complex.exp (↑(-u) * Complex.I)

theorem QuantumInfo.AharonovBohm.conj_exp_mul_I_mul_self (u : ℝ) : (starRingEnd ℂ) (Complex.exp (↑u * Complex.I)) * Complex.exp (↑u * Complex.I) = 1

theorem QuantumInfo.AharonovBohm.gaugeDiag_conjTranspose_mul {N : ℕ} [NeZero N] (g : ZMod N → ℝ) : (gaugeDiag N g).conjTranspose * gaugeDiag N g = 1

A gauge transformation is unitary.

theorem QuantumInfo.AharonovBohm.gaugeDiag_conj_ringHamOf {N : ℕ} [NeZero N] (hN : 3 ≤ N) (a g : ZMod N → ℝ) : (gaugeDiag N g).conjTranspose * ringHamOf N a * gaugeDiag N g = ringHamOf N fun (j : ZMod N) => a j + g j - g (j + 1)

★★ Gauge covariance of the ring. Conjugating by the diagonal unitary diag(e^{i g}) moves the bond phases by the discrete gradient of g: the vector potential is not observable, only gauge-equivalent descriptions of the same ring.

theorem QuantumInfo.AharonovBohm.flux_gauge {N : ℕ} [NeZero N] (a g : ZMod N → ℝ) : (flux N fun (j : ZMod N) => a j + g j - g (j + 1)) = flux N a

★ The flux is gauge-invariant: the discrete gradient of g sums to zero around the ring.

All the flux on one bond

def QuantumInfo.AharonovBohm.oneBondPhase (N : ℕ) (Φ : ℝ) : ZMod N → ℝ

The gauge in which the whole flux sits on the single bond from −1 to 0.

Equations

• QuantumInfo.AharonovBohm.oneBondPhase N Φ j = if j = -1 then Φ else 0

theorem QuantumInfo.AharonovBohm.flux_oneBondPhase {N : ℕ} [NeZero N] (Φ : ℝ) : flux N (oneBondPhase N Φ) = Φ

noncomputable def QuantumInfo.AharonovBohm.oneBondGauge (N : ℕ) (Φ : ℝ) : ZMod N → ℝ

The gauge function that pushes the uniform phases onto that one bond.

Equations

• QuantumInfo.AharonovBohm.oneBondGauge N Φ j = Φ / ↑N * ↑j.val

theorem QuantumInfo.AharonovBohm.val_add_one_of_ne {N : ℕ} [NeZero N] (hN : 3 ≤ N) {j : ZMod N} (h : j ≠ -1) : (j + 1).val = j.val + 1

Away from the distinguished site the successor's value is the successor of the value.

theorem QuantumInfo.AharonovBohm.uniform_add_oneBondGauge {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) (j : ZMod N) : Φ / ↑N + oneBondGauge N Φ j - oneBondGauge N Φ (j + 1) = oneBondPhase N Φ j

★ The uniform phases, gauge-shifted by oneBondGauge, are exactly the one-bond phases.

theorem QuantumInfo.AharonovBohm.gaugeDiag_conj_ringHam_oneBond {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) : (gaugeDiag N (oneBondGauge N Φ)).conjTranspose * ringHam N Φ * gaugeDiag N (oneBondGauge N Φ) = ringHamOf N (oneBondPhase N Φ)

★★★ The whole flux can be put on a single bond. The uniform ring and the ring whose entire Peierls phase sits on the bond from −1 to 0 are the same Hamiltonian in two gauges: conjugate by one explicit diagonal unitary. The spectrum therefore cannot see how the phase is distributed — only its total, the flux.

The discrete Fourier transform diagonalises the ring

theorem QuantumInfo.AharonovBohm.mulVec_three {N : ℕ} [NeZero N] (A B C : Matrix (ZMod N) (ZMod N) ℂ) (v : ZMod N → ℂ) : (A * B * C).mulVec v = A.mulVec (B.mulVec (C.mulVec v))

Three matrices acting on a vector, one at a time.

theorem QuantumInfo.AharonovBohm.sum_stdAddChar_mul {N : ℕ} [NeZero N] (t : ZMod N) : ∑ j : ZMod N, ZMod.stdAddChar (t * j) = if t = 0 then ↑N else 0

Character orthogonality on ZMod N: the sum of stdAddChar (t · j) over the ring is N for t = 0 and 0 otherwise.

theorem QuantumInfo.AharonovBohm.intCast_val {N : ℕ} [NeZero N] (k : ZMod N) : ↑↑k.val = k

The integer label of a site is the site.

noncomputable def QuantumInfo.AharonovBohm.dftMatrix (N : ℕ) [NeZero N] : Matrix (ZMod N) (ZMod N) ℂ

The discrete Fourier matrix of the ring: its columns are the twisted modes, normalised.

Equations

• QuantumInfo.AharonovBohm.dftMatrix N = Matrix.of fun (j k : ZMod N) => QuantumInfo.AharonovBohm.ringMode N k j / ↑√↑N

theorem QuantumInfo.AharonovBohm.dftMatrix_apply {N : ℕ} [NeZero N] (j k : ZMod N) : dftMatrix N j k = ringMode N k j / ↑√↑N

theorem QuantumInfo.AharonovBohm.dftMatrix_conjTranspose_mul {N : ℕ} [NeZero N] : (dftMatrix N).conjTranspose * dftMatrix N = 1

★ The Fourier matrix is unitary — character orthogonality.

theorem QuantumInfo.AharonovBohm.dftMatrix_mul_conjTranspose {N : ℕ} [NeZero N] : dftMatrix N * (dftMatrix N).conjTranspose = 1

theorem QuantumInfo.AharonovBohm.dftMatrix_conj_ringHam {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) : (dftMatrix N).conjTranspose * ringHam N Φ * dftMatrix N = Matrix.diagonal fun (k : ZMod N) => ↑(ringEigval N Φ ↑k.val)

★★ The ring Hamiltonian is diagonalised by the discrete Fourier transform, with the Aharonov–Bohm levels 2 cos((2πk + Φ)/N) on the diagonal.

theorem QuantumInfo.AharonovBohm.eq_ringEigval_of_mulVec {N : ℕ} [NeZero N] (hN : 3 ≤ N) (Φ : ℝ) {μ : ℂ} {v : ZMod N → ℂ} (hv : v ≠ 0) (h : (ringHam N Φ).mulVec v = μ • v) : ∃ (k : ZMod N), μ = ↑(ringEigval N Φ ↑k.val)

★★ Those levels are the whole spectrum. Every eigenvalue of the ring is one of the 2 cos((2πk + Φ)/N).

The flux is observable

theorem QuantumInfo.AharonovBohm.ringEigval_three_pi_ne_two (m : ℤ) : ringEigval 3 Real.pi m ≠ 2

At Φ = π no level of the three-site ring is 2: 2 cos((2πm + π)/3) = 2 would force 2m + 1 = 6n.

theorem QuantumInfo.AharonovBohm.ringEigval_three_zero_zero : ringEigval 3 0 0 = 2

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

★★★ The flux is observable: the Aharonov–Bohm phase is not a gauge artefact. No unitary conjugation carries the three-site ring with no flux to the three-site ring with flux π — the level 2 of the first is not a level of the second. Together with gaugeDiag_conj_ringHam_oneBond (the phases may be redistributed at will) this is the Aharonov–Bohm effect: the vector potential is not observable, the flux is.

The flux is determined by the spectrum

range_ringEigval_add_two_pi says the spectrum cannot distinguish Φ from Φ + 2π, and energy_lt_energy_of_flux_lt (Empirical/QM/AharonovBohm.lean) says a fixed label's level moves strictly with the flux over a range where nothing wraps. Neither says that the level set pins the flux down, which is what "the flux is observable" claims in full. It does, modulo a quantum and up to sign, because the top of the spectrum is 2 cos(d(Φ)/N) with d(Φ) the distance from Φ to the nearest whole quantum, and that is a strictly decreasing function of d.

noncomputable def QuantumInfo.AharonovBohm.fluxDist (Φ : ℝ) : ℝ

The distance from Φ to the nearest whole flux quantum: the only thing about the flux that the ring's spectrum can see.

Equations

• QuantumInfo.AharonovBohm.fluxDist Φ = |Φ - 2 * Real.pi * ↑(round (Φ / (2 * Real.pi)))|

theorem QuantumInfo.AharonovBohm.cos_abs_eq (y : ℝ) : Real.cos |y| = Real.cos y

theorem QuantumInfo.AharonovBohm.fluxDist_nonneg (Φ : ℝ) : 0 ≤ fluxDist Φ

theorem QuantumInfo.AharonovBohm.abs_sub_two_pi_mul (Φ : ℝ) (j : ℤ) : |Φ - 2 * Real.pi * ↑j| = |Φ / (2 * Real.pi) - ↑j| * (2 * Real.pi)

The distance to a given quantum, measured in units of the quantum.

theorem QuantumInfo.AharonovBohm.fluxDist_le_abs (Φ : ℝ) (k : ℤ) : fluxDist Φ ≤ |Φ - 2 * Real.pi * ↑k|

★ No quantum is nearer. fluxDist really is the distance to the nearest one.

theorem QuantumInfo.AharonovBohm.fluxDist_le_pi (Φ : ℝ) : fluxDist Φ ≤ Real.pi

★ Half a quantum is as far as a flux can be from the nearest whole one.

theorem QuantumInfo.AharonovBohm.cos_fluxDist (x : ℝ) : Real.cos (fluxDist x) = Real.cos x

The cosine of a level's argument is the cosine of its distance from a whole turn.

theorem QuantumInfo.AharonovBohm.ringEigval_le {N : ℕ} (hN : 0 < N) (Φ : ℝ) (m : ℤ) : ringEigval N Φ m ≤ 2 * Real.cos (fluxDist Φ / ↑N)

★★ No level rises above 2 cos(fluxDist Φ / N): a label's argument sits at least fluxDist Φ / N from a whole turn, and cosine falls away from it.

theorem QuantumInfo.AharonovBohm.ringEigval_neg_round {N : ℕ} (Φ : ℝ) : ringEigval N Φ (-round (Φ / (2 * Real.pi))) = 2 * Real.cos (fluxDist Φ / ↑N)

★★ The maximum is attained, at the label that centres its mode on the flux.

theorem QuantumInfo.AharonovBohm.isGreatest_range_ringEigval {N : ℕ} (hN : 0 < N) (Φ : ℝ) : IsGreatest (Set.range (ringEigval N Φ)) (2 * Real.cos (fluxDist Φ / ↑N))

★★★ The top of the spectrum reads the flux: the greatest level is 2 cos(fluxDist Φ / N), a strictly decreasing function of the distance from the flux to the nearest whole quantum.

theorem QuantumInfo.AharonovBohm.fluxDist_eq_of_range_eq {N : ℕ} (hN : 0 < N) {Φ Φ' : ℝ} (h : Set.range (ringEigval N Φ) = Set.range (ringEigval N Φ')) : fluxDist Φ = fluxDist Φ'

★★★ The spectrum determines the flux distance: two rings of the same size with the same level set sit at the same distance from a whole quantum.

theorem QuantumInfo.AharonovBohm.range_ringEigval_neg {N : ℕ} (Φ : ℝ) : Set.range (ringEigval N (-Φ)) = Set.range (ringEigval N Φ)

★★ The spectrum cannot see the sign of the flux: reversing it permutes the levels, so the ambiguity in the theorem below is real and not an artefact of the proof.

theorem QuantumInfo.AharonovBohm.exists_eq_of_range_ringEigval_eq {N : ℕ} (hN : 0 < N) {Φ Φ' : ℝ} (h : Set.range (ringEigval N Φ) = Set.range (ringEigval N Φ')) : ∃ (k : ℤ), Φ' = Φ + 2 * Real.pi * ↑k ∨ Φ' = -Φ + 2 * Real.pi * ↑k

★★★ The flux is determined by the spectrum, at every ring size: two fluxes with the same level set differ by a whole quantum, or are reflections of one another in a whole quantum. With range_ringEigval_add_two_pi and range_ringEigval_neg the converse holds as well, so this is exactly what a spectroscopic measurement of the ring determines — no more and no less.