The Three-Gap (Steinhaus) theorem

A self-contained Lean 4 / Mathlib formalization of the three-gap theorem, depending only on Mathlib. It works in [0,1) through Int.fract (NOT AddCircle), via the first-return (Slater / van Ravenstein) route.

Status

Complete and machine-checked — three_gap_card_le_three (for every a : ℝ and N : ℕ, the N-point orbit {i·a mod 1 : i < N} partitions [0,1) into at most three distinct gap lengths) is proved with no sorry, no warnings, and only the standard axioms propext / Classical.choice / Quot.sound. Uniform in a (rational and irrational alike).

The development, in order:

• orbit, gaps, gaps_sum_eq_one — construction; the gaps sum to 1;
• sortedVal and its order theory (sortedVal_strictMono, _zero, _last, …);
• the two first returns etaPos = η⁺, etaNeg = η⁻, with minimality;
• three_gap_card_le_three_of_subset — the reduction "gap values lie in a three-element set ⇒ at most three distinct gap lengths";
• the multiplier layer (canMul, mPlus, mMinus) with the index-shift identities (fract_index_shift) and the noPointBetween lemmas;
• cases A (gap_eq_etaPos) and B (gap_eq_etaNeg) of the first-return classification, with the index-bridge infrastructure;
• the corner case η⁺ + η⁻ (corner_gap), via the M-circle (L1/L3) and an induction-free closure of L2 — see the "corner case" section below;
• the full classification neighbour_gap_in_returns and the bound three_gap_card_le_three.

Design

gaps enumerates the sorted distinct points through Finset.orderEmbOfFin (Fin k ↪o ℝ, k = (orbit a N).card), extended to a total sortedVal : ℕ → ℝ; the gaps are the adjacent differences over Finset.range (k - 1) plus the wrap-around (min + 1) - max, and gaps_sum_eq_one is a Finset telescoping sum.

Note on noncomputable: on ℝ, DecidableEq and the order are noncomputable, so orbit, orbitCard, orbitEmb, sortedVal, gaps, canMul, … are all noncomputable.

noncomputable def SteinhausThreeGap.orbit (a : ℝ) (N : ℕ) : Finset ℝ

The (finite, distinct) orbit { Int.fract (i * a) | i < N } in [0,1).

noncomputable, since Finset.image on ℝ uses the (noncomputable) DecidableEq ℝ instance.

Equations

• SteinhausThreeGap.orbit a N = Finset.image (fun (i : ℕ) => Int.fract (↑i * a)) (Finset.range N)

theorem SteinhausThreeGap.orbit_nonempty (a : ℝ) {N : ℕ} (hN : 0 < N) : (orbit a N).Nonempty

The orbit is nonempty as soon as there is at least one index, i.e. 0 < N. Ties the hypothesis 0 < N of gaps_sum_eq_one to the orbit.

theorem SteinhausThreeGap.orbit_subset_Ico (a : ℝ) (N : ℕ) : ↑(orbit a N) ⊆ Set.Ico 0 1

Every orbit point is a fractional part, hence lies in [0,1).

noncomputable def SteinhausThreeGap.orbitCard (a : ℝ) (N : ℕ) : ℕ

The number of distinct orbit points. noncomputable, as it depends on the noncomputable orbit.

Equations

• SteinhausThreeGap.orbitCard a N = (SteinhausThreeGap.orbit a N).card

noncomputable def SteinhausThreeGap.orbitEmb (a : ℝ) (N : ℕ) : Fin (orbitCard a N) ↪o ℝ

The increasing enumeration Fin k ↪o ℝ of the distinct orbit points, where k = orbitCard a N. Element i is the i-th smallest point.

Equations

• SteinhausThreeGap.orbitEmb a N = (SteinhausThreeGap.orbit a N).orderEmbOfFin ⋯

noncomputable def SteinhausThreeGap.sortedVal (a : ℝ) (N i : ℕ) : ℝ

The sorted distinct orbit points as a total index function ℕ → ℝ: sortedVal a N i is the i-th smallest point when i < orbitCard a N, and a junk value 0 otherwise. Only indices 0, …, orbitCard a N - 1 matter; the telescoping below is purely formal in sortedVal.

Equations

• SteinhausThreeGap.sortedVal a N i = if h : i < SteinhausThreeGap.orbitCard a N then (SteinhausThreeGap.orbitEmb a N) ⟨i, h⟩ else 0

noncomputable def SteinhausThreeGap.gaps (a : ℝ) (N : ℕ) : Multiset ℝ

The multiset of consecutive gaps of the sorted distinct orbit points, plus the single wrap-around gap (min + 1) - max.

With k = orbitCard a N and g = sortedVal a N:

• the k - 1 adjacent gaps g (i+1) - g i, i = 0, …, k - 2, by mapping over Finset.range (k - 1);
• the wrap-around gap g 0 + 1 - g (k - 1) (i.e. min + 1 - max), added as a singleton.

Equations

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

theorem SteinhausThreeGap.gaps_sum_eq_one (a : ℝ) (N : ℕ) (hN : 0 < N) : (gaps a N).sum = 1

The gaps sum to one. Telescoping of the adjacent differences gives max - min; adding the wrap-around gap (min + 1) - max yields 1.

The proof is a pure Finset telescoping sum (Finset.sum_range_sub) followed by ring.

Phase 1 — orbit membership and the sorted enumeration

theorem SteinhausThreeGap.mem_orbit_iff (a : ℝ) (N : ℕ) (x : ℝ) : x ∈ orbit a N ↔ ∃ i < N, Int.fract (↑i * a) = x

Membership in the orbit. x is an orbit point iff it is Int.fract (i * a) for some index i < N.

theorem SteinhausThreeGap.zero_mem_orbit (a : ℝ) {N : ℕ} (hN : 0 < N) : 0 ∈ orbit a N

0 lies in every nonempty orbit (index i = 0 gives Int.fract 0 = 0).

theorem SteinhausThreeGap.sortedVal_strictMono (a : ℝ) (N : ℕ) {i j : ℕ} (hij : i < j) (hj : j < orbitCard a N) : sortedVal a N i < sortedVal a N j

The sorted enumeration is strictly increasing on the valid index range: for i < j with j < orbitCard a N, sortedVal a N i < sortedVal a N j.

theorem SteinhausThreeGap.sortedVal_zero (a : ℝ) {N : ℕ} (hN : 0 < N) : sortedVal a N 0 = (orbit a N).min' ⋯

The first sorted value is the minimum.

theorem SteinhausThreeGap.sortedVal_last (a : ℝ) {N : ℕ} (hN : 0 < N) : sortedVal a N (orbitCard a N - 1) = (orbit a N).max' ⋯

The last sorted value is the maximum.

theorem SteinhausThreeGap.sortedVal_mem (a : ℝ) {N i : ℕ} (h : i < orbitCard a N) : sortedVal a N i ∈ orbit a N

Every sorted value (below the count) is an orbit point.

Phase 2 — gap infrastructure and the distinct-gap-count reduction

noncomputable def SteinhausThreeGap.gapAt (a : ℝ) (N i : ℕ) : ℝ

The i-th adjacent gap of the sorted enumeration.

Equations

• SteinhausThreeGap.gapAt a N i = SteinhausThreeGap.sortedVal a N (i + 1) - SteinhausThreeGap.sortedVal a N i

theorem SteinhausThreeGap.gaps_eq (a : ℝ) (N : ℕ) : gaps a N = Multiset.map (gapAt a N) (Finset.range (orbitCard a N - 1)).val + {sortedVal a N 0 + 1 - sortedVal a N (orbitCard a N - 1)}

gaps written through gapAt (definitional).

theorem SteinhausThreeGap.gapAt_pos (a : ℝ) (N : ℕ) {i : ℕ} (h : i + 1 < orbitCard a N) : 0 < gapAt a N i

Internal (non-wrap-around) gaps are positive.

theorem SteinhausThreeGap.mem_gaps_iff (a : ℝ) (N : ℕ) (x : ℝ) : x ∈ gaps a N ↔ (∃ i < orbitCard a N - 1, gapAt a N i = x) ∨ x = sortedVal a N 0 + 1 - sortedVal a N (orbitCard a N - 1)

Membership in gaps, unpacked into the internal gaps and the wrap-around gap.

theorem SteinhausThreeGap.gaps_toFinset_card_le (a : ℝ) (N : ℕ) : (gaps a N).toFinset.card ≤ (gaps a N).card

A loose bound: the number of distinct gap values is at most the number of gaps.

theorem SteinhausThreeGap.three_gap_card_le_three_of_subset (a : ℝ) (N : ℕ) {x y z : ℝ} (hsub : (gaps a N).toFinset ⊆ {x, y, z}) : (gaps a N).toFinset.card ≤ 3

Reduction lemma for the three-gap bound. If every distinct gap value lies in a fixed three-element set, then there are at most three distinct gap lengths. The Phase 2 core supplies the hypothesis with {η⁺, η⁻, η⁺+η⁻}.

Phase 2 core — the two first returns η⁺, η⁻ (self-contained infrastructure)

The positive return η⁺ is the smallest positive orbit point; the negative return η⁻ is 1 - max(orbit). We package the positive orbit points as posOrbit a N := (orbit a N).erase 0. Everything below is proved unconditionally (no surjectivity of the sorted enumeration is needed); the genuinely combinatorial crux and the lemmas that depend on the enumeration-onto bridge are organized in the Phase 2 core sections below.

noncomputable def SteinhausThreeGap.posOrbit (a : ℝ) (N : ℕ) : Finset ℝ

The positive orbit points (orbit a N) \ {0}. Each lies in (0,1).

Equations

• SteinhausThreeGap.posOrbit a N = (SteinhausThreeGap.orbit a N).erase 0

theorem SteinhausThreeGap.mem_posOrbit_iff (a : ℝ) (N : ℕ) (x : ℝ) : x ∈ posOrbit a N ↔ x ≠ 0 ∧ x ∈ orbit a N

theorem SteinhausThreeGap.posOrbit_subset_orbit (a : ℝ) (N : ℕ) : posOrbit a N ⊆ orbit a N

theorem SteinhausThreeGap.posOrbit_pos (a : ℝ) (N : ℕ) {x : ℝ} (hx : x ∈ posOrbit a N) : 0 < x

theorem SteinhausThreeGap.posOrbit_lt_one (a : ℝ) (N : ℕ) {x : ℝ} (hx : x ∈ posOrbit a N) : x < 1

theorem SteinhausThreeGap.posOrbit_nonempty (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : (posOrbit a N).Nonempty

theorem SteinhausThreeGap.orbitCard_le (a : ℝ) (N : ℕ) : orbitCard a N ≤ N

orbitCard a N ≤ N (the orbit is the image of range N).

theorem SteinhausThreeGap.pos_of_two_le_orbitCard (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : 0 < N

A nondegenerate orbit (2 ≤ orbitCard) forces 0 < N.

noncomputable def SteinhausThreeGap.etaPos (a : ℝ) (N : ℕ) : ℝ

The positive return η⁺: the smallest positive orbit point. Junk 1 in the degenerate regime.

Equations

• SteinhausThreeGap.etaPos a N = if h : (SteinhausThreeGap.posOrbit a N).Nonempty then (SteinhausThreeGap.posOrbit a N).min' h else 1

noncomputable def SteinhausThreeGap.etaNeg (a : ℝ) (N : ℕ) : ℝ

The negative return η⁻ = 1 - (largest positive orbit point). Junk 1 in the degenerate regime.

Equations

• SteinhausThreeGap.etaNeg a N = if h : (SteinhausThreeGap.posOrbit a N).Nonempty then 1 - (SteinhausThreeGap.posOrbit a N).max' h else 1

theorem SteinhausThreeGap.etaPos_mem (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : etaPos a N ∈ posOrbit a N

η⁺ is achieved by an actual positive orbit point: it lies in posOrbit.

theorem SteinhausThreeGap.etaPos_pos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : 0 < etaPos a N

η⁺ > 0.

theorem SteinhausThreeGap.etaPos_le (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {x : ℝ} (hx : x ∈ posOrbit a N) : etaPos a N ≤ x

η⁺ is minimal among positive orbit points.

theorem SteinhausThreeGap.no_orbit_below_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {x : ℝ} (hx : x ∈ orbit a N) (hx0 : 0 < x) : etaPos a N ≤ x

η⁺ is the smallest positive orbit point.

theorem SteinhausThreeGap.max_posOrbit_mem (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : 1 - etaNeg a N ∈ posOrbit a N

1 - η⁻ (the largest positive orbit point) is achieved.

theorem SteinhausThreeGap.etaNeg_pos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : 0 < etaNeg a N

η⁻ > 0.

theorem SteinhausThreeGap.le_one_sub_etaNeg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {x : ℝ} (hx : x ∈ posOrbit a N) : x ≤ 1 - etaNeg a N

Every positive orbit point is ≤ 1 - η⁻.

theorem SteinhausThreeGap.sortedVal_zero_eq_zero (a : ℝ) {N : ℕ} (hN : 0 < N) : sortedVal a N 0 = 0

With at least one orbit point, the smallest sorted value is 0.

theorem SteinhausThreeGap.sortedVal_monotone (a : ℝ) (N : ℕ) {i j : ℕ} (hij : i ≤ j) (hj : j < orbitCard a N) : sortedVal a N i ≤ sortedVal a N j

sortedVal is monotone (non-strict) on the valid index range.

theorem SteinhausThreeGap.lt_of_sortedVal_lt (a : ℝ) (N : ℕ) {i m : ℕ} (hi : i < orbitCard a N) (h : sortedVal a N i < sortedVal a N m) : i < m

sortedVal reflects strict order on valid indices.

theorem SteinhausThreeGap.gaps_card_eq_one_of_degenerate (a : ℝ) {N : ℕ} (h1 : orbitCard a N ≤ 1) : (gaps a N).card = 1

In the degenerate regime orbitCard a N ≤ 1, gaps a N has a single element.

Phase 2 core — enumeration-onto bridge and the two returns as gap values

The bridge from the sorted enumeration back to the orbit, the no-orbit-point-between lemma, and the identification of the first internal gap with η⁺ and the wrap-around gap with η⁻. Together with three_gap_card_le_three_of_subset these reduce the three-gap bound to the single first-return classification lemma (neighbour_gap_in_returns, the genuine combinatorial core, proved below).

theorem SteinhausThreeGap.exists_index_of_mem_orbit (a : ℝ) (N : ℕ) {y : ℝ} (hy : y ∈ orbit a N) : ∃ j < orbitCard a N, sortedVal a N j = y

The sorted enumeration is onto the orbit. Every orbit point is sortedVal j for some valid index j.

theorem SteinhausThreeGap.no_orbit_strictly_between (a : ℝ) (N : ℕ) {i : ℕ} (hi : i + 1 < orbitCard a N) {z : ℝ} (hz : z ∈ orbit a N) (hlo : sortedVal a N i < z) (hhi : z < sortedVal a N (i + 1)) : False

No orbit point lies strictly between two consecutive sorted points.

theorem SteinhausThreeGap.sortedVal_one_eq_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : sortedVal a N 1 = etaPos a N

sortedVal a N 1 = η⁺.

theorem SteinhausThreeGap.wraparound_eq_etaNeg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : sortedVal a N 0 + 1 - sortedVal a N (orbitCard a N - 1) = etaNeg a N

The wrap-around gap equals η⁻.

theorem SteinhausThreeGap.gapAt_zero_eq_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : gapAt a N 0 = etaPos a N

The first internal gap is η⁺.

theorem SteinhausThreeGap.etaPos_is_gap (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : etaPos a N ∈ gaps a N

η⁺ occurs as a gap value. (API extra; not used by the main chain.)

theorem SteinhausThreeGap.etaNeg_is_gap (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : etaNeg a N ∈ gaps a N

η⁻ occurs as a gap value. (API extra; not used by the main chain.)

Phase 2 core — fractional-part rotation helpers (toward the first-return lemma)

theorem SteinhausThreeGap.fract_add_fract_eq (x y : ℝ) : Int.fract (Int.fract x + Int.fract y) = Int.fract (x + y)

Fractional-part index-shift identity. Reducing the two summands mod 1 first does not change the fractional part of a sum: Int.fract (Int.fract x + Int.fract y) = Int.fract (x + y). With x = u*a, y = m*a this is the value form of the multiplier shift u, m ↦ u + m.

theorem SteinhausThreeGap.fract_rotate_mem (a : ℝ) (N : ℕ) {u m : ℕ} (hum : u + m < N) : Int.fract (Int.fract (↑u * a) + Int.fract (↑m * a)) ∈ orbit a N

Forward rotation closure (multiplier in range). If u + m < N, the rotated value Int.fract (Int.fract (u*a) + Int.fract (m*a)) is again an orbit point. This is the half of the Slater closure that does not wrap past index N; the values that fall off the end (u + m ≥ N) are where the negative return appears. (API extra; not used by the main chain.)

Multiplier-indexed infrastructure (toward the first-return dichotomy)

The value-Finset orbit hides the index ("multiplier") behind each point. We recover a canonical multiplier and the forward value-shift; the discriminant of the three-gap dichotomy is the Nat condition canMul + mp < N.

noncomputable def SteinhausThreeGap.mulFiber (a : ℝ) (N : ℕ) (p : ℝ) : Finset ℕ

The finset of indices < N whose rotation value equals p.

Equations

• SteinhausThreeGap.mulFiber a N p = {k ∈ Finset.range N | Int.fract (↑k * a) = p}

theorem SteinhausThreeGap.mem_mulFiber_iff (a : ℝ) (N : ℕ) (p : ℝ) (k : ℕ) : k ∈ mulFiber a N p ↔ k < N ∧ Int.fract (↑k * a) = p

theorem SteinhausThreeGap.mulFiber_nonempty (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) : (mulFiber a N p).Nonempty

noncomputable def SteinhausThreeGap.canMul (a : ℝ) (N : ℕ) (p : ℝ) (hp : p ∈ orbit a N) : ℕ

Canonical (least) multiplier of an orbit point p.

Equations

• SteinhausThreeGap.canMul a N p hp = (SteinhausThreeGap.mulFiber a N p).min' ⋯

theorem SteinhausThreeGap.canMul_mem_fiber (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) : canMul a N p hp ∈ mulFiber a N p

theorem SteinhausThreeGap.canMul_lt (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) : canMul a N p hp < N

theorem SteinhausThreeGap.fract_canMul (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) : Int.fract (↑(canMul a N p hp) * a) = p

theorem SteinhausThreeGap.exists_return_multiplier (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : ∃ mp < N, Int.fract (↑mp * a) = etaPos a N

Return-multiplier existence for η⁺ (the smallest positive orbit point): some mp < N rotates to η⁺.

theorem SteinhausThreeGap.exists_back_return_multiplier (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : ∃ mn < N, Int.fract (↑mn * a) = 1 - etaNeg a N

Backward return-multiplier existence for 1 - η⁻ (the largest positive orbit point): some mn < N rotates to 1 - η⁻.

theorem SteinhausThreeGap.fract_shift_eq (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) {mp : ℕ} (hmpval : Int.fract (↑mp * a) = etaPos a N) : Int.fract (↑(canMul a N p hp + mp) * a) = Int.fract (p + etaPos a N)

Value-shift identity. Rotating an orbit point p (canonical multiplier u = canMul p) by a return multiplier mp for η⁺ lands on Int.fract (p + η⁺). (API extra; the main chain uses fract_index_shift.)

theorem SteinhausThreeGap.shift_mem_orbit (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) {mp : ℕ} (hmpval : Int.fract (↑mp * a) = etaPos a N) (hrange : canMul a N p hp + mp < N) (hlt1 : p + etaPos a N < 1) (hp0 : 0 ≤ p) (heta0 : 0 ≤ etaPos a N) : p + etaPos a N ∈ orbit a N

Forward shift lands in the orbit when the multiplier stays in range (canMul p + mp < N) and p + η⁺ < 1 (no wrap). (API extra; unused.)

Forward-neighbour upper bound (API extra — superseded by Case A below)

theorem SteinhausThreeGap.gap_le_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) (hfwd : sortedVal a N i + etaPos a N < 1 ∧ sortedVal a N i + etaPos a N ∈ orbit a N) : gapAt a N i ≤ etaPos a N

Forward-neighbour upper bound. Under the forward hypothesis hfwd, the gap is at MOST η⁺: the orbit point q := sortedVal i + η⁺ lies strictly above sortedVal i and < 1, so by no_orbit_strictly_between it cannot sit strictly below sortedVal (i+1). (API extra; superseded by gap_eq_etaPos.)

Index-bridge infrastructure (multiplier indices and difference extraction)

Toward the first-return classification, recovering the index structure behind the orbit values. The decisive discriminant is the index condition j + m⁺ < N, NOT the value condition xⱼ + η⁺ ∈ orbit: those differ (e.g. α = 4/5, N = 4, point 2/5 has 2/5 + η⁺ = 4/5 ∈ orbit yet gap = η⁻, since its index is off-end).

theorem SteinhausThreeGap.fract_sub_fract_eq (x y : ℝ) : Int.fract (Int.fract x - Int.fract y) = Int.fract (x - y)

Fractional-part subtraction identity (companion of fract_add_fract_eq).

theorem SteinhausThreeGap.forward_inRange_card {N mp : ℕ} (h : mp ≤ N) : {j ∈ Finset.range N | j + mp < N}.card = N - mp

Pure Nat/Finset counting seed: exactly N - mp indices keep their forward +mp shift in range, so exactly mp fall off the end. (API extra; unused.)

noncomputable def SteinhausThreeGap.mPlus (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : ℕ

Forward return multiplier as an index: the canonical (least) index whose rotation value is η⁺.

Equations

• SteinhausThreeGap.mPlus a N h2 = SteinhausThreeGap.canMul a N (SteinhausThreeGap.etaPos a N) ⋯

theorem SteinhausThreeGap.mPlus_lt (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : mPlus a N h2 < N

theorem SteinhausThreeGap.fract_mPlus (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : Int.fract (↑(mPlus a N h2) * a) = etaPos a N

theorem SteinhausThreeGap.mPlus_pos (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : 0 < mPlus a N h2

theorem SteinhausThreeGap.sub_mem_orbit_of_index_le (a : ℝ) (N : ℕ) {j w : ℕ} (hjw : j ≤ w) (hw : w < N) (hlt : Int.fract (↑j * a) < Int.fract (↑w * a)) : Int.fract (↑w * a) - Int.fract (↑j * a) ∈ orbit a N

Difference extraction, w ≥ j. If two orbit points have non-decreasing indices j ≤ w < N and increasing values, their difference is an orbit point. Combined with no_orbit_below_etaPos this rules out a between-point reachable from a higher index.

theorem SteinhausThreeGap.compl_mem_orbit_of_index_gt (a : ℝ) (N : ℕ) {j w : ℕ} (hwj : w < j) (hj : j < N) (hlt : Int.fract (↑j * a) < Int.fract (↑w * a)) : 1 - (Int.fract (↑w * a) - Int.fract (↑j * a)) ∈ orbit a N

Difference extraction, w < j (dual). If the larger value {w·a} has the smaller index w < j, the complement 1 - ({w·a} - {j·a}) is an orbit point ({(j-w)·a}) in the top band (1 - η⁺, 1). Via le_one_sub_etaNeg this gives {w·a} - {j·a} ≥ η⁻; used in the backward index-bridge toward Case B.

The forward (η⁺) case

theorem SteinhausThreeGap.fract_index_shift (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) (j : ℕ) : Int.fract (↑(j + mPlus a N h2) * a) = Int.fract (Int.fract (↑j * a) + etaPos a N)

Shifting an index by m⁺ realises the rotation by η⁺ at the value level: {(j+m⁺)·a} = {{j·a} + η⁺}.

theorem SteinhausThreeGap.fract_index_shift_noWrap (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) (j : ℕ) (hlt1 : Int.fract (↑j * a) + etaPos a N < 1) : Int.fract (↑(j + mPlus a N h2) * a) = Int.fract (↑j * a) + etaPos a N

No-wrap specialisation: when {j·a} + η⁺ < 1, the m⁺-shifted index lands on exactly {j·a} + η⁺.

theorem SteinhausThreeGap.fract_add_etaPos_le_one (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {d : ℕ} (hd : d + mPlus a N h2 < N) : Int.fract (↑d * a) + etaPos a N ≤ 1

D1 — an in-range index is not in the top band. If d + m⁺ < N then {d·a} + η⁺ ≤ 1. (If not, {(d+m⁺)·a} = {d·a}+η⁺-1 is a positive orbit value < η⁺, contradicting minimality.)

theorem SteinhausThreeGap.noPointBetween (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {j : ℕ} (hj : j + mPlus a N h2 < N) {z : ℝ} (hz : z ∈ orbit a N) (hlo : Int.fract (↑j * a) < z) (hhi : z < Int.fract (↑j * a) + etaPos a N) : False

No orbit point lies in (xⱼ, xⱼ + η⁺) when j + m⁺ < N. w ≥ j: the difference is a positive orbit value < η⁺ (minimality). w < j: the complementary index j - w would be in the top band, contradicting D1.

theorem SteinhausThreeGap.gap_eq_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) {j : ℕ} (hjfr : Int.fract (↑j * a) = sortedVal a N i) (hjN : j + mPlus a N h2 < N) : gapAt a N i = etaPos a N

Case A (forward): an index j of v = sortedVal i with j + m⁺ < N forces gap = η⁺.

Backward (η⁻) machinery — mirror of the forward case

noncomputable def SteinhausThreeGap.mMinus (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : ℕ

Backward return multiplier: the canonical index of the MAX orbit value 1-η⁻.

Equations

• SteinhausThreeGap.mMinus a N h2 = SteinhausThreeGap.canMul a N (1 - SteinhausThreeGap.etaNeg a N) ⋯

theorem SteinhausThreeGap.mMinus_lt (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : mMinus a N h2 < N

theorem SteinhausThreeGap.fract_mMinus (a : ℝ) (N : ℕ) (h2 : 2 ≤ orbitCard a N) : Int.fract (↑(mMinus a N h2) * a) = 1 - etaNeg a N

theorem SteinhausThreeGap.fract_index_shift_neg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) (j : ℕ) : Int.fract (↑(j + mMinus a N h2) * a) = Int.fract (Int.fract (↑j * a) + (1 - etaNeg a N))

Index shift by m⁻ realises rotation by 1-η⁻ (i.e. by -η⁻) at value level.

theorem SteinhausThreeGap.fract_sub_etaNeg_ge (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {d : ℕ} (hd : d + mMinus a N h2 < N) (h0 : 0 < Int.fract (↑d * a)) : etaNeg a N ≤ Int.fract (↑d * a)

D1' (mirror): an in-range index is not in the bottom band. If d + m⁻ < N and {d·a} > 0 then η⁻ ≤ {d·a}.

theorem SteinhausThreeGap.noPointBetween_neg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {j : ℕ} (hj : j + mMinus a N h2 < N) {z : ℝ} (hz : z ∈ orbit a N) (hlo : Int.fract (↑j * a) - etaNeg a N < z) (hhi : z < Int.fract (↑j * a)) : False

No orbit point lies in (xⱼ - η⁻, xⱼ) when j + m⁻ < N (backward mirror of noPointBetween).

theorem SteinhausThreeGap.gap_eq_etaNeg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) {j' : ℕ} (hjfr : Int.fract (↑j' * a) = sortedVal a N (i + 1)) (hjN : j' + mMinus a N h2 < N) : gapAt a N i = etaNeg a N

Case B (backward): an index j' of v' = sortedVal (i+1) with j' + m⁻ < N forces gap = η⁻.

The corner case η⁺ + η⁻ — completing the classification

The remaining case of the three-gap bound: the corner, where both first returns fall off the end (canMul v + m⁺ ≥ N and canMul v' + m⁻ ≥ N). Then the gap is η⁺ + η⁻ (corner_gap). The argument:

• corner_canMul_lt_mMinus (hP1 : canMul v < m⁻): if j ≥ m⁻ then v+η⁻ would be the successor v', forcing canMul v' + m⁻ < N, contradicting hB.
• upper bound v' ≤ v+η⁺+η⁻: realise q := v+η⁺+η⁻ as {(canMul v + m⁺ - m⁻)·a} (index < N by hP1).
• lower bound: no orbit point in (v, v+η⁺+η⁻), split as L1 (v, v+η⁺), L2 v+η⁺ ∉ orbit a N, L3 (v+η⁺, q).

L1/L3 (corner_noPoint_lo / corner_noPoint_hi) use the M-circle M := m⁺ + m⁻: orbit a N ⊆ orbit a M, the returns are unchanged (no_new_below_etaPos, no_new_above_etaNeg, etaPos_eq_extend, etaNeg_eq_extend), and hP1 keeps the shifted indices < M.

L2 is closed WITHOUT induction (uniform in a, rational or irrational): if v+η⁺ = {k·a} with k ≥ j then m⁺ ≤ k-j, so k ≥ j+m⁺ ≥ N, impossible; if k < j then d := j+m⁺-k is a period ({d·a}=0) with m⁺ < d < m⁺+m⁻, contradicting minimality of m⁻ (the max 1-η⁻ at index m⁻-d) or of m⁺ (η⁺=η⁻, then at index d-m⁻). This replaces van Ravenstein / Mayero's induction-on-N and avoids their irrational-only restriction.

theorem SteinhausThreeGap.fract_sub_mMinus (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {k : ℕ} (hk : mMinus a N h2 ≤ k) : Int.fract (↑(k - mMinus a N h2) * a) = Int.fract (Int.fract (↑k * a) - (1 - etaNeg a N))

Backward index shift by m⁻. For m⁻ ≤ k, subtracting the canonical m⁻ from the index k rotates the value by -(1-η⁻) mod 1.

theorem SteinhausThreeGap.canMul_le (a : ℝ) (N : ℕ) {p : ℝ} (hp : p ∈ orbit a N) {c : ℕ} (hc : c < N) (hcval : Int.fract (↑c * a) = p) : canMul a N p hp ≤ c

Minimality of the canonical multiplier. Any in-range index c < N whose rotation value is p is at least canMul a N p.

theorem SteinhausThreeGap.fract_sub_mPlus (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {k : ℕ} (hk : mPlus a N h2 ≤ k) : Int.fract (↑(k - mPlus a N h2) * a) = Int.fract (Int.fract (↑k * a) - etaPos a N)

Forward index shift by m⁺. For m⁺ ≤ k, subtracting the canonical m⁺ from the index k rotates the value by -η⁺ mod 1.

theorem SteinhausThreeGap.no_new_below_etaPos (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {k : ℕ} (hkN : N ≤ k) (hkM : k < mPlus a N h2 + mMinus a N h2) (hpos : 0 < Int.fract (↑k * a)) : etaPos a N ≤ Int.fract (↑k * a)

Returns are preserved when extending the orbit to M = m⁺ + m⁻ indices (positive return). No new index k ∈ [N, m⁺+m⁻) produces a positive value below η⁺. (Key step of the M-circle route to the corner bound: a value s = {k·a} ∈ (0, η⁺) would force {(k-m⁻)·a} = η⁺, hence m⁺ ≤ k-m⁻ by minimality, i.e. k ≥ m⁺+m⁻, contradiction.)

theorem SteinhausThreeGap.no_new_above_etaNeg (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {k : ℕ} (hkN : N ≤ k) (hkM : k < mPlus a N h2 + mMinus a N h2) : Int.fract (↑k * a) ≤ 1 - etaNeg a N

Returns are preserved when extending the orbit to M = m⁺ + m⁻ indices (negative return). No new index k ∈ [N, m⁺+m⁻) produces a value in the top band (1-η⁻, 1). Mirror of no_new_below_etaPos.

M-circle infrastructure (orbit extension N ↦ M = m⁺ + m⁻)

Monotonicity of the orbit in the index count, and the fact that the two returns η⁺, η⁻ are unchanged when the orbit is extended from N to M = m⁺ + m⁻ (no new index in [N, M) produces a smaller positive value or a larger value). These let the corner "no point in the big gap" arguments (corner_noPoint_lo/hi) borrow the in-range first-return machinery in the larger circle.

theorem SteinhausThreeGap.orbit_mono (a : ℝ) {N M : ℕ} (h : N ≤ M) : orbit a N ⊆ orbit a M

The orbit grows with the index count.

theorem SteinhausThreeGap.orbitCard_mono (a : ℝ) {N M : ℕ} (h : N ≤ M) : orbitCard a N ≤ orbitCard a M

theorem SteinhausThreeGap.posOrbit_mono (a : ℝ) {N M : ℕ} (h : N ≤ M) : posOrbit a N ⊆ posOrbit a M

theorem SteinhausThreeGap.etaPos_eq_extend (a : ℝ) {N M : ℕ} (h2 : 2 ≤ orbitCard a N) (hNM : N ≤ M) (hM2 : 2 ≤ orbitCard a M) (hnew : ∀ (k : ℕ), N ≤ k → k < M → 0 < Int.fract (↑k * a) → etaPos a N ≤ Int.fract (↑k * a)) : etaPos a M = etaPos a N

Positive return preserved under extension. If every new index k ∈ [N, M) avoids the band (0, η⁺), then η⁺ is unchanged from N to M.

theorem SteinhausThreeGap.etaNeg_eq_extend (a : ℝ) {N M : ℕ} (h2 : 2 ≤ orbitCard a N) (hNM : N ≤ M) (hM2 : 2 ≤ orbitCard a M) (hnew : ∀ (k : ℕ), N ≤ k → k < M → Int.fract (↑k * a) ≤ 1 - etaNeg a N) : etaNeg a M = etaNeg a N

Negative return preserved under extension. If every new index k ∈ [N, M) avoids the top band (1 - η⁻, 1), then η⁻ is unchanged from N to M.

theorem SteinhausThreeGap.corner_canMul_lt_mMinus (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) (hvmem : sortedVal a N i ∈ orbit a N) (hv'mem : sortedVal a N (i + 1) ∈ orbit a N) (hB : ¬canMul a N (sortedVal a N (i + 1)) hv'mem + mMinus a N h2 < N) : canMul a N (sortedVal a N i) hvmem < mMinus a N h2

Corner discriminant hP1 (independent of the lower bound). In the corner, the canonical index j = canMul v of the left point satisfies j < m⁻.

Proof: if j ≥ m⁻, then w := v + η⁻ = {(j-m⁻)·a} ∈ orbit a N (a valid index < N). As w lies in range with canMul w + m⁻ ≤ j < N, case B (gap_eq_etaNeg) shows the predecessor of w is w - η⁻ = v; hence w is the successor v' of v, so v' = v + η⁻ and canMul v' ≤ j - m⁻, giving canMul v' + m⁻ ≤ j < N — contradicting the corner hypothesis hB.

theorem SteinhausThreeGap.corner_noPoint_lo (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hvmem : sortedVal a N i ∈ orbit a N) (hP1 : canMul a N (sortedVal a N i) hvmem < mMinus a N h2) (hA : N ≤ canMul a N (sortedVal a N i) hvmem + mPlus a N h2) {z : ℝ} (hz : z ∈ orbit a N) (hlo : sortedVal a N i < z) (hhi : z < sortedVal a N i + etaPos a N) : False

L1 — no orbit point in (v, v + η⁺) (corner). Direct difference extraction: a point z = {w·a} with v < z < v + η⁺ gives, when w ≥ j, a positive value z - v < η⁺ in orbit a N (contra η⁺ minimal); and when w < j, a positive value η⁺ - (z-v) < η⁺ in the extended orbit orbit a M (M = m⁺ + m⁻) at index (j-w) + m⁺ < M, contradicting minimality of etaPos a M = etaPos a N. The discriminant hP1 : j < m⁻ makes the shifted index stay in range < M.

theorem SteinhausThreeGap.corner_noPoint_hi (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hvmem : sortedVal a N i ∈ orbit a N) (hP1 : canMul a N (sortedVal a N i) hvmem < mMinus a N h2) (hA : N ≤ canMul a N (sortedVal a N i) hvmem + mPlus a N h2) {z : ℝ} (hz : z ∈ orbit a N) (hlo : sortedVal a N i + etaPos a N < z) (hhi : z < sortedVal a N i + etaPos a N + etaNeg a N) : False

L3 — no orbit point in (v + η⁺, v + η⁺ + η⁻) (corner). Mirror of L1: the point p₁ = v + η⁺ = {(j+m⁺)·a} ∈ orbit a M. A point z with p₁ < z < p₁ + η⁻ has every index w < N ≤ j + m⁺, so {((j+m⁺)-w)·a} = 1 - (z - p₁) lies in (1 - η⁻, 1) ∩ orbit a M, exceeding the maximum 1 - η⁻ of orbit a M — contradiction.

theorem SteinhausThreeGap.corner_gap (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) (hvmem : sortedVal a N i ∈ orbit a N) (hv'mem : sortedVal a N (i + 1) ∈ orbit a N) (hA : ¬canMul a N (sortedVal a N i) hvmem + mPlus a N h2 < N) (hB : ¬canMul a N (sortedVal a N (i + 1)) hv'mem + mMinus a N h2 < N) : gapAt a N i = etaPos a N + etaNeg a N

The corner case. When both first returns fall off the end (canMul v + m⁺ ≥ N and canMul v' + m⁻ ≥ N), the internal gap is η⁺ + η⁻. The lower bound hLower (no orbit point lies strictly in (v, v + η⁺ + η⁻)) is proved inline below; the proof is self-contained, with no external input.

theorem SteinhausThreeGap.neighbour_gap_in_returns (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) {i : ℕ} (hi : i + 1 < orbitCard a N) : gapAt a N i ∈ {etaPos a N, etaNeg a N, etaPos a N + etaNeg a N}

The first-return classification. Every internal gap is η⁺, η⁻, or η⁺ + η⁻: case A (gap_eq_etaPos) when canMul v + m⁺ < N, case B (gap_eq_etaNeg) when canMul v' + m⁻ < N, and the corner (corner_gap) otherwise. (No i = 0 special case is needed: there canMul v = 0 and m⁺ < N, so case A always fires.)

theorem SteinhausThreeGap.gaps_subset_returns (a : ℝ) {N : ℕ} (h2 : 2 ≤ orbitCard a N) : (gaps a N).toFinset ⊆ {etaPos a N, etaNeg a N, etaPos a N + etaNeg a N}

All distinct gap values lie in {η⁺, η⁻, η⁺ + η⁻} (non-degenerate regime).

theorem SteinhausThreeGap.three_gap_card_le_three (a : ℝ) (N : ℕ) : (gaps a N).toFinset.card ≤ 3

The three-gap (Steinhaus) theorem, distinct-gap-count form. Every gap of {i·a mod 1 : i < N} is η⁺, η⁻, or η⁺ + η⁻, so at most three lengths.

theorem SteinhausThreeGap.three_gap_lengths_eq (a : ℝ) {N : ℕ} (h3 : (gaps a N).toFinset.card = 3) : (gaps a N).toFinset = {etaPos a N, etaNeg a N, etaPos a N + etaNeg a N}

The sum relation. When the gaps take exactly three distinct lengths, those lengths are precisely η⁺, η⁻, and η⁺ + η⁻; in particular the largest, η⁺ + η⁻, is the sum of the other two (they are positive: etaPos_pos, etaNeg_pos). The nondegeneracy 2 ≤ orbitCard is derived from h3.