`Compfiles/Imo1978P3.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

15 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1978, Problem 3

The set of all positive integers is the union of two disjoint subsets {f(1), f(2), ..., f(n), ...} and {g(1), g(2), ..., g(n), ...}, where

f(1) < f(2) < ... < f(n) < ..., g(1) < g(2) < ... < g(n) < ...,

and g(n) = f(f(n)) + 1 for all n ≥ 1.

Determine f(240).

Imports (2)

Imported by 1 file

Compfiles.lean

determine Imo1978P3.solution line 33 source
no axioms what this means
Statement uses: Nat
Proof uses: OfNat.ofNat
1 instances, coercions and auxiliary constants left out.
def Imo1978P3.a The lower Wythoff sequence ⌊n·φ⌋, which is the function f in the problem line 52 source
Source documentation
The lower Wythoff sequence ⌊n·φ⌋, which is the function f in the problem.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Int.toNat, Int.floor, Real, HMul.hMul, Real.goldenRatio
7 instances, coercions and auxiliary constants left out.
```
noncomputable def a (n : ℕ) : ℕ := (⌊(n : ℝ) * φ⌋).toNat
```
lemma Imo1978P3.a_eq line 54 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, Imo1978P3.a, Int.floor, Real, HMul.hMul, Real.goldenRatio
Proof uses: id, Eq.mpr, Int.toNat, congrArg, Int.toNat_of_nonneg, Iff.mpr, LE.le, OfNat.ofNat, Int.floor_nonneg, mul_nonneg, Nat.cast_nonneg', le_of_lt, div_pos, HAdd.hAdd, Real.sqrt, add_pos', Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Eq.refl and 6 more
61 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.a_add_eq a n + n = ⌊n·φ²⌋, using φ² = φ + 1 line 60 source
Source documentation
a n + n = ⌊n·φ²⌋, using φ² = φ + 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, HAdd.hAdd, Imo1978P3.a, Int.floor, Real, HMul.hMul, HPow.hPow, Real.goldenRatio, OfNat.ofNat
Proof uses: Eq.mpr, id, congrArg, Imo1978P3.a_eq, Real.goldenRatio_sq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, NNRat.rawCast, Real.sqrt, Mathlib.Tactic.Ring.Common.mul_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.symm, Eq.refl, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.div_congr, Mathlib.Tactic.Ring.cast_pos, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_one, Mathlib.Tactic.Ring.Common.add_pf_add_lt and 24 more
67 instances, coercions and auxiliary constants left out.

Tactic trace: 5 steps
Open to load the checked before-and-after goal states.
```
lemma a_add_eq (n : ℕ) : ((a n : ℤ) + n) = ⌊(n : ℝ) * φ ^ 2⌋ := by
…
```
Mentions: Imo1978P3.a
lemma Imo1978P3.beattySeq_a line 65 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, beattySeq, Real.goldenRatio, Imo1978P3.a
Proof uses: Eq.mpr, Int.floor, Real, HMul.hMul, id, congrArg, Imo1978P3.a_eq, beattySeq.eq_1, congrFun', Int.cast_natCast, Eq.refl
15 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.beattySeq_a_add line 68 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, Eq, Int, beattySeq, HPow.hPow, Real, Real.goldenRatio, OfNat.ofNat, HAdd.hAdd, Imo1978P3.a
Proof uses: Eq.mpr, Int.floor, HMul.hMul, id, congrArg, Imo1978P3.a_add_eq, beattySeq.eq_1, congrFun', Int.cast_natCast, Eq.refl
29 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.holderConj line 71 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Real.HolderConjugate, Real.goldenRatio, HPow.hPow, Real, Nat, OfNat.ofNat
Proof uses: Real.HolderTriple.mk, Eq.mpr, Eq, HAdd.hAdd, Inv.inv, id, congrArg, inv_one, Eq.symm, inv_pow, Neg.neg, Real.goldenConj, Real.inv_goldenRatio, neg_sq, Real.goldenConj_sq, Mathlib.Tactic.Ring.of_eq, Nat.rawCast, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.add_congr, Rat.rawCast and 72 more
99 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.a_pos line 76 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Imo1978P3.a
Proof uses: LE.le, Real, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_one, HMul.hMul, Real.goldenRatio, Trans.trans, Eq, Real.one_lt_goldenRatio, one_mul, mul_le_mul_of_nonneg_right, le_of_lt, div_pos, HAdd.hAdd, Real.sqrt, add_pos' and 82 more
109 instances, coercions and auxiliary constants left out.

Tactic trace: 11 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.a_strictMono line 87 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: StrictMono, Nat, Imo1978P3.a
Proof uses: strictMono_nat_of_lt_succ, LE.le, Int, HAdd.hAdd, OfNat.ofNat, Eq.mpr, Int.floor, Real, HMul.hMul, Real.goldenRatio, id, Eq, congrArg, Imo1978P3.a_eq, LT.lt, Real.one_lt_goldenRatio, le_of_not_gt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, HSub.hSub and 75 more
86 instances, coercions and auxiliary constants left out.

Tactic trace: 16 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.a_mono line 102 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LE.le, Imo1978P3.a
Proof uses: StrictMono.monotone, Imo1978P3.a_strictMono
4 instances, coercions and auxiliary constants left out.
lemma Imo1978P3.ha_cover Every positive integer is a k or a k + k for some k ≥ 1 line 105 source
Source documentation
Every positive integer is a k or a k + k for some k ≥ 1.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Or, Exists, And, Eq, Imo1978P3.a, HAdd.hAdd
Proof uses: Int, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Set, symmDiff, Set.ofPred, GT.gt, beattySeq, Real.goldenRatio, HPow.hPow, Real, Irrational.beattySeq_symmDiff_beattySeq_pos, Imo1978P3.holderConj, Real.goldenRatio_irrational, Membership.mem, Not and 13 more
52 instances, coercions and auxiliary constants left out.

Tactic trace: 31 steps
Open to load the checked before-and-after goal states.
```
lemma ha_cover (m : ℕ) (hm : 0 < m) :
    (∃ k, 0 < k ∧ a k = m) ∨ (∃ k, 0 < k ∧ a k + k = m) := by
…
```
Mentions: Imo1978P3.a
lemma Imo1978P3.ha_disj The two sequences a k and a k + k are disjoint line 129 source
Source documentation
The two sequences a k and a k + k are disjoint.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Ne, Imo1978P3.a, HAdd.hAdd
Proof uses: Eq, Int, Imo1978P3.a_pos, cast, Eq.symm, Eq.trans, congrFun', congrArg, Nat.cast_zero, Eq.mpr, id, Nat.cast_add, Mathlib.Tactic.Ring.of_eq, HMul.hMul, HPow.hPow, Nat.rawCast, Mathlib.Tactic.Ring.Common.add_congr, Mathlib.Tactic.Ring.Common.atom_pf, rfl, Eq.refl and 25 more
62 instances, coercions and auxiliary constants left out.

Tactic trace: 20 steps
Open to load the checked before-and-after goal states.
```
lemma ha_disj (j k : ℕ) (hj : 0 < j) (hk : 0 < k) : a j ≠ a k + k := by
…
```
Mentions: Imo1978P3.a
lemma Imo1978P3.a_240 line 140 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Eq, Nat, Imo1978P3.a, OfNat.ofNat
Proof uses: Real, HPow.hPow, Real.sqrt, Real.sq_sqrt, Mathlib.Meta.NormNum.isNat_le_true, Mathlib.Meta.NormNum.isNat_ofNat, Nat.cast_zero, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool, Bool.true, LE.le, Real.sqrt_nonneg, Real.goldenRatio, HDiv.hDiv, HAdd.hAdd, rfl, HMul.hMul, Eq.mpr, id and 105 more
116 instances, coercions and auxiliary constants left out.

Tactic trace: 22 steps
Open to load the checked before-and-after goal states.
lemma Imo1978P3.wythoff_unique A strictly increasing positive sequence F is uniquely determined by the property that {F k} and {F k + k} partition the positive integers line 158 source
Source documentation
A strictly increasing positive sequence F is uniquely determined by the property that {F k} and {F k + k} partition the positive integers. We state this as: any two such sequences F and A agree. The key fact is that F n is the least positive integer not among {F k, F k + k : k < n}.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Or, Exists, And, Eq, HAdd.hAdd, Ne
Proof uses: LE.le, Decidable.byContradiction, Not, False, eq_or_lt_of_le, Eq.mp, lt_irrefl, congrArg, absurd, LT.lt.not_gt, Or.inl, Exists.intro, And.intro, Eq.mpr, id, Or.inr, ne_of_lt, Eq.symm, Nat.strong_induction_on
25 instances, coercions and auxiliary constants left out.

Tactic trace: 36 steps
Open to load the checked before-and-after goal states.
```
lemma wythoff_unique (F A : ℕ → ℕ)
    (hFmono : ∀ p q, 0 < p → p < q → F p < F q)
    (hAmono : ∀ p q, 0 < p → p < q → A p < A q)
    (hFpos : ∀ k, 0 < k → 0 < F k)
    (hApos : ∀ k, 0 < k → 0 < A k)
    (coverF : ∀ m, 0 < m → (∃ k, 0 < k ∧ F k = m) ∨ (∃ k, 0 < k ∧ F k + k = m))
    (coverA : ∀ m, 0 < m → (∃ k, 0 < k ∧ A k = m) ∨ (∃ k, 0 < k ∧ A k + k = m))
    (disjF : ∀ p q, 0 < p → 0 < q → F p ≠ F q + q)
    (disjA : ∀ p q, 0 < p → 0 < q → A p ≠ A q + q) :
    ∀ n, 0 < n → F n = A n := by
…
```
problem Imo1978P3.imo1978_p3 line 208 source
standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat, LT.lt, OfNat.ofNat, Ne, Or, Exists, And, Eq, HAdd.hAdd, Imo1978P3.solution
Proof uses: Set.InjOn, Finset, Finset.Icc, Membership.mem, Set, lt_trichotomy, absurd, ne_of_lt, Eq.mp, LE.le, Eq.trans, Set.Icc, congrFun', congrArg, Finset.coe_Icc, Eq.symm, eq_or_lt_of_le, Eq.mpr, id, le_refl and 40 more
48 instances, coercions and auxiliary constants left out.

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