`Compfiles/Imo2018P5.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 8 curated AI-written annotations and 3305 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned compfiles documentation, Pinned compfiles corpus index

8 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2018, Problem 5

Let a₁, a₂, ... be an infinite sequence of positive integers. Suppose that there is an integer N > 1 such that for each n ≥ N the number

a₁/a₂ + a₂/a₃ ... + aₙ₋₁/aₙ + aₙ/a₁

is an integer. Prove that there is a positive integer M such that aₘ = aₘ₊₁ for all m ≥ M.

Imports (2)

Imported by 1 file

Compfiles.lean

def Imo2018P5.S The sum `a₀/a₁ + a₁/a₂ + line 34 source
Source comment
The sum `a₀/a₁ + a₁/a₂ + ... + aₙ₋₁/a₀` of the problem statement.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, Rat
Proof uses: Finset.sum, Finset.range, HDiv.hDiv, HMod.hMod, HAdd.hAdd, OfNat.ofNat
10 instances, coercions and auxiliary constants left out.
```
def S (a : ℕ → ℤ) (n : ℕ) : ℚ := ∑ i ∈ Finset.range n, (a i : ℚ) / a ((i + 1) % n)
```
lemma Imo2018P5.S_sub Difference of two consecutive sums: for n ≥ 1, S (n+1) - S n = aₙ₋₁/aₙ + (aₙ - aₙ₋₁)/a₀ line 38 source
Source comment
Difference of two consecutive sums: for `n ≥ 1`, `S (n+1) - S n = aₙ₋₁/aₙ + (aₙ - aₙ₋₁)/a₀`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LE.le, OfNat.ofNat, Eq, Rat, HSub.hSub, Imo2018P5.S, HAdd.hAdd, HDiv.hDiv
Proof uses: Finset.sum, Finset.range, id, Eq.mpr, HMod.hMod, congrArg, Finset.sum_range_succ, HAdd, Eq.rec, Eq.refl, Finset.sum_congr, rfl, Finset, Membership.mem, Nat.mod_eq_of_lt, Eq.mp, LT.lt, propext, Finset.mem_range, Nat.mod_self and 51 more
76 instances, coercions and auxiliary constants left out.

Tactic trace: 30 steps
Open to load the checked before-and-after goal states.
```
lemma S_sub (a : ℕ → ℤ) (n : ℕ) (hn : 1 ≤ n) :
    S a (n + 1) - S a n = (a (n - 1) : ℚ) / a n + ((a n : ℚ) - a (n - 1)) / a 0 := by
…
```
Mentions: Imo2018P5.S
lemma Imo2018P5.step The key per-step relation line 68 source
Source comment
The key per-step relation. If `S n` and `S (n+1)` are both integers, then there is an integer `k` (namely `a₀·aₙ₋₁/aₙ`) with `aₙ * k = a₀ * aₙ₋₁` and `a₀ ∣ k + aₙ - aₙ₋₁`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, Exists, Eq, Rat, Imo2018P5.S, And, HMul.hMul, HSub.hSub, Dvd.dvd, HAdd.hAdd
Proof uses: HDiv.hDiv, Imo2018P5.S_sub, Exists.intro, And.intro, Eq.mpr, id, congr, congrArg, Eq.trans, Int.cast_mul, Int.cast_sub, Eq.mp, Eq.symm, Ne, cast, Not, Nat.cast_zero, Int.cast_zero, LT.lt.ne', inferInstance and 85 more
120 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma step (a : ℕ → ℤ) (apos : ∀ n, 0 < a n) (N : ℕ)
    (h : ∀ n, N ≤ n → ∃ z : ℤ, z = S a n) {n : ℕ} (hn : N ≤ n) (hn1 : 1 ≤ n) :
    ∃ k : ℤ, a n * k = a 0 * a (n - 1) ∧ a 0 ∣ k + a n - a (n - 1) := by
…
```
Mentions: h, Imo2018P5.S
lemma Imo2018P5.val_rule The valuation rule line 90 source
Source comment
The valuation rule. For a prime `p`, write `α, κ, V, V'` for the `p`-adic valuations of `a₀, k, aₙ₋₁, aₙ` respectively, where `k` comes from `step`. Then: `κ < α` forces `V = κ` and `V' = α`; `κ = α` forces `V' = V`; `α < κ` forces `α ≤ V' < V`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, Nat.Prime, Eq, HMul.hMul, HSub.hSub, Dvd.dvd, HAdd.hAdd, And, padicValInt, LE.le
Proof uses: Fact, Fact.mk, Eq.mpr, id, congrArg, rfl, Ne, LT.lt.ne', False, mul_ne_zero, Eq.symm, Eq.mp, MulZeroClass.mul_zero, padicValInt.mul, HPow.hPow, dvd_trans, padicValInt_dvd, Or.resolve_left, Iff.mp, Or and 70 more
133 instances, coercions and auxiliary constants left out.

Tactic trace: 135 steps
Open to load the checked before-and-after goal states.
```
lemma val_rule (a : ℕ → ℤ) (apos : ∀ n, 0 < a n) {p : ℕ} (hp : p.Prime)
    {n : ℕ} {k : ℤ} (hk1 : a n * k = a 0 * a (n - 1)) (hk2 : a 0 ∣ k + a n - a (n - 1)) :
    (padicValInt p k < padicValInt p (a 0) →
        padicValInt p (a (n - 1)) = padicValInt p k ∧ padicValInt p (a n) = padicValInt p (a 0)) ∧
    (padicValInt p k = padicValInt p (a 0) → padicValInt p (a n) = padicValInt p (a (n - 1))) ∧
    (padicValInt p (a 0) < padicValInt p k →
        padicValInt p (a n) < padicValInt p (a (n - 1)) ∧
        padicValInt p (a 0) ≤ padicValInt p (a n)) := by
…
```
lemma Imo2018P5.bound Boundedness: for n ≥ N - 1 and every prime p, v_p(aₙ) ≤ v_p(a₀) + v_p(a_{N-1}), proved by induction using val_rule line 211 source
Source comment
Boundedness: for `n ≥ N - 1` and every prime `p`, `v_p(aₙ) ≤ v_p(a₀) + v_p(a_{N-1})`, proved by induction using `val_rule`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, Exists, Eq, Rat, Imo2018P5.S, HSub.hSub, Nat.Prime, padicValInt, HAdd.hAdd
Proof uses: Nat.le_induction, Nat.le_add_left, And, HMul.hMul, Dvd.dvd, Imo2018P5.step, Imo2018P5.val_rule, Or, lt_trichotomy, Eq.mp, congrArg, Nat.add_sub_cancel, Eq.mpr, id, Nat.le_add_right
37 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
lemma bound (a : ℕ → ℤ) (apos : ∀ n, 0 < a n) (N : ℕ) (hN : 0 < N)
    (h : ∀ n, N ≤ n → ∃ z : ℤ, z = S a n)
    (n : ℕ) (hn : N - 1 ≤ n) (p : ℕ) (hp : p.Prime) :
    padicValInt p (a n) ≤ padicValInt p (a 0) + padicValInt p (a (N - 1)) := by
…
```
Mentions: h, Imo2018P5.S
lemma Imo2018P5.dvd_bound Divisibility form of the bound: aₙ ∣ a₀ · a_{N-1} for n ≥ N - 1 line 231 source
Source comment
Divisibility form of the bound: `aₙ ∣ a₀ · a_{N-1}` for `n ≥ N - 1`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, Exists, Eq, Rat, Imo2018P5.S, HSub.hSub, Dvd.dvd, HMul.hMul
Proof uses: Int.natAbs, Eq.mpr, id, congrArg, Int.natAbs_mul, Finsupp, Nat.factorization, Eq.symm, propext, Nat.factorization_le_iff_dvd, Iff.mpr, Ne, Int.natAbs_ne_zero, LT.lt.ne', mul_ne_zero, dite, Nat.Prime, HAdd.hAdd, Nat.factorization_mul, Finsupp.add_apply and 8 more
50 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
```
lemma dvd_bound (a : ℕ → ℤ) (apos : ∀ n, 0 < a n) (N : ℕ) (hN : 0 < N)
    (h : ∀ n, N ≤ n → ∃ z : ℤ, z = S a n) (n : ℕ) (hn : N - 1 ≤ n) :
    a n ∣ a 0 * a (N - 1) := by
…
```
Mentions: h, Imo2018P5.S
lemma Imo2018P5.walk_const No closed walk line 250 source
Source comment
No closed walk. If the sequence returns to the same value (`a n₁ = a n₂` with `n₁ < n₂`, `N ≤ n₁`), then it was constant on the whole interval `[n₁, n₂]`.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, Exists, Eq, Rat, Imo2018P5.S
Proof uses: Membership.mem, Finset, Finset.Ioc, And, HMul.hMul, HSub.hSub, Dvd.dvd, HAdd.hAdd, dite, Iff.mp, Finset.mem_Ioc, Imo2018P5.step, Exists.intro, And.intro, Not, absurd, Nat.Prime, padicValInt, Imo2018P5.val_rule, Or and 47 more
93 instances, coercions and auxiliary constants left out.

Tactic trace: 205 steps (first 200 of 205)
Open to load the checked before-and-after goal states.
```
lemma walk_const (a : ℕ → ℤ) (apos : ∀ n, 0 < a n) (N : ℕ) (hN : 0 < N)
    (h : ∀ n, N ≤ n → ∃ z : ℤ, z = S a n)
    {n₁ n₂ : ℕ} (hn₁ : N ≤ n₁) (hlt : n₁ < n₂) (heq : a n₁ = a n₂)
    (j : ℕ) (hj1 : n₁ ≤ j) (hj2 : j ≤ n₂) : a j = a n₁ := by
…
```
Mentions: h, Imo2018P5.S
problem Imo2018P5.imo2018_p5 line 415 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Int, LT.lt, OfNat.ofNat, LE.le, Exists, Eq, Rat, Finset.sum, Finset.range, HDiv.hDiv, HMod.hMod, HAdd.hAdd
Proof uses: Imo2018P5.S, Classical.byContradiction, Not, HMul.hMul, HSub.hSub, rfl, mul_pos, GE.ge, Membership.mem, Finset, Finset.Icc, Eq.mpr, And, id, congrArg, propext, Finset.mem_Icc, And.intro, Int.le_of_dvd, Imo2018P5.dvd_bound and 26 more
73 instances, coercions and auxiliary constants left out.

Tactic trace: 35 steps
Open to load the checked before-and-after goal states.