Compfiles/Imo1990P2.lean

GitHub source file

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

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

11 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 1990, Problem 2

Take n ≥ 3 and consider a set E of 2n - 1 distinct points on a circle. Suppose that exactly k of these points are to be colored black. Such a coloring is said to be "good" if there is at least one pair of black points such that the interior of one of the arcs between them contains exactly n points from E. Find the smallest value of k so that every such coloring of k points of E is good.

Imports (2)
Imported by 1 file
  1. determine Imo1990P2.solution line 29 source

    no axioms what this means

    Statement uses: Nat

    Proof uses: ite, Eq, HMod.hMod, OfNat.ofNat, HSub.hSub

    6 instances, coercions and auxiliary constants left out.

  2. def Imo1990P2.IsGood Label the points by ZMod (2 * n - 1) line 35 source

    Source documentation

    Label the points by ZMod (2 * n - 1). A set B of black points is good if it contains two points x and y with y - x = n + 1 or x - y = n + 1, which is exactly the condition that one of the two arcs between them contains n points of E in its interior.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, ZMod, HSub.hSub, HMul.hMul, OfNat.ofNat

    Proof uses: Exists, And, Membership.mem, Or, Eq, HAdd.hAdd

    23 instances, coercions and auxiliary constants left out.

    def IsGood (n : ℕ) (B : Finset (ZMod (2 * n - 1))) : Prop :=
…
  3. theorem Imo1990P2.IsGood.mono line 41 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, ZMod, HSub.hSub, HMul.hMul, OfNat.ofNat, LE.le, Imo1990P2.IsGood

    Proof uses: And, Membership.mem, Exists, Or, Eq, HAdd.hAdd, Exists.intro, And.intro

    31 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

    Open to load the checked before-and-after goal states.

  4. theorem Imo1990P2.bad_disjoint_translate A bad (i.e. not good) coloring and its translate by n + 1 are disjoint line 47 source

    Source documentation

    A bad (i.e. not good) coloring and its translate by n + 1 are disjoint.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, Finset, ZMod, HSub.hSub, HMul.hMul, OfNat.ofNat, Not, Imo1990P2.IsGood, Disjoint, Finset.image, HAdd.hAdd

    Proof uses: Eq.mpr, Membership.mem, id, Eq, congrArg, propext, Finset.disjoint_left, And, Exists, False, Eq.mp, Finset.mem_image, Exists.intro, Or, And.intro, Or.inl, Eq.symm, add_sub_cancel_left, Eq.refl

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

    Open to load the checked before-and-after goal states.

    theorem bad_disjoint_translate {n : ℕ} {B : Finset (ZMod (2 * n - 1))}
    (hbad : ¬ IsGood n B) :
    Disjoint B (B.image (· + ((n + 1 : ℕ) : ZMod (2 * n - 1)))) := by
…

    Mentions: Imo1990P2.IsGood

  5. theorem Imo1990P2.card_range_filter_mod_eq Exactly t of the numbers 0, ..., 3 * t - 1 are congruent to j mod 3 line 59 source

    Source documentation

    Exactly t of the numbers 0, ..., 3 * t - 1 are congruent to j mod 3.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LT.lt, OfNat.ofNat, Eq, Finset.card, Finset.filter, HMod.hMod, Finset.range, HMul.hMul

    Proof uses: Finset.card_bij, Membership.mem, Finset, HDiv.hDiv, Eq.mpr, id, congrArg, propext, Finset.mem_range, Eq.mp, And, Finset.mem_filter, Exists.intro, Exists, HAdd.hAdd, Finset.card_range

    24 instances, coercions and auxiliary constants left out.

    Tactic trace: 19 steps

    Open to load the checked before-and-after goal states.

    theorem card_range_filter_mod_eq (t j : ℕ) (hj : j < 3) :
    ((Finset.range (3 * t)).filter (· % 3 = j)).card = t := by
…
  6. theorem Imo1990P2.card_univ_filter_val_mod_eq When 3 ∣ N, exactly N / 3 elements of ZMod N have a given val residue mod 3 line 79 source

    Source documentation

    When 3 ∣ N, exactly N / 3 elements of ZMod N have a given val residue mod 3.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, Dvd.dvd, OfNat.ofNat, LT.lt, Eq, Finset.card, ZMod, Finset.filter, HMod.hMod, ZMod.val, Finset.univ, HDiv.hDiv

    Proof uses: Finset, Finset.image, Finset.range, Finset.ext, Eq.mpr, Iff, Membership.mem, And, id, congrArg, propext, Finset.mem_filter, Exists, Finset.mem_image, congr, Eq.trans, True, congrFun', true_and, funext and 19 more

    42 instances, coercions and auxiliary constants left out.

    Tactic trace: 22 steps

    Open to load the checked before-and-after goal states.

    theorem card_univ_filter_val_mod_eq {N : ℕ} [NeZero N] (hN : 3 ∣ N) (j : ℕ)
    (hj : j < 3) :
    ((Finset.univ : Finset (ZMod N)).filter (fun x => x.val % 3 = j)).card = N / 3 := by
…
  7. theorem Imo1990P2.val_mod_translate Translation by n + 1 preserves val % 3 when 3 ∣ n + 1 and 3 ∣ 2 * n - 1 line 104 source

    Source documentation

    Translation by n + 1 preserves val % 3 when 3 ∣ n + 1 and 3 ∣ 2 * n - 1.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, NeZero, HSub.hSub, HMul.hMul, OfNat.ofNat, Dvd.dvd, HAdd.hAdd, ZMod, Eq, HMod.hMod, ZMod.val

    Proof uses: Nat.ModEq, Eq.mpr, id, congrArg, Eq.symm, propext, ZMod.natCast_eq_natCast_iff, Nat.cast_add, ZMod.natCast_rightInverse, Nat.ModEq.of_dvd, Iff.mpr, Nat.add_modEq_left_iff, Nat.ModEq.trans

    45 instances, coercions and auxiliary constants left out.

    Tactic trace: 8 steps

    Open to load the checked before-and-after goal states.

    theorem val_mod_translate {n : ℕ} [NeZero (2 * n - 1)] (h3n : 3 ∣ n + 1)
    (h3N : 3 ∣ 2 * n - 1) (x : ZMod (2 * n - 1)) :
    (x + ((n + 1 : ℕ) : ZMod (2 * n - 1))).val % 3 = x.val % 3 := by
…
  8. theorem Imo1990P2.coprime_aux If n % 3 ≠ 2 then 2 * n - 1 and n + 1 are coprime line 119 source

    Source documentation

    If n % 3 ≠ 2 then 2 * n - 1 and n + 1 are coprime.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Ne, HMod.hMod, Nat.Coprime, HSub.hSub, HMul.hMul, HAdd.hAdd

    Proof uses: Eq.mpr, Eq, Nat.gcd, id, congrArg, propext, Nat.coprime_iff_gcd_eq_one, Dvd.dvd, dvd_trans, Nat.gcd_dvd_right, dvd_mul_left, Nat.gcd_dvd_left, Nat.dvd_sub, Eq.mp, Or, Iff.mp, Nat.dvd_prime, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl and 9 more

    27 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

    Open to load the checked before-and-after goal states.

    theorem coprime_aux {n : ℕ} (hn : 3 ≤ n) (h3 : n % 3 ≠ 2) :
    Nat.Coprime (2 * n - 1) (n + 1) := by
…
  9. theorem Imo1990P2.card_le_of_bad Upper bound: a bad coloring has at most solution n - 1 black points line 136 source

    Source documentation

    Upper bound: a bad coloring has at most solution n - 1 black points.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Finset, ZMod, HSub.hSub, HMul.hMul, Not, Imo1990P2.IsGood, Finset.card, Imo1990P2.solution

    Proof uses: NeZero, NeZero.mk, Disjoint, Finset.image, HAdd.hAdd, Imo1990P2.bad_disjoint_translate, Function.Injective, Eq, add_right_cancel, dite, HMod.hMod, Exists, Exists.intro, HDiv.hDiv, id, Eq.mpr, ite, congrArg, ite_eq_left, Dvd.dvd and 71 more

    90 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

    Open to load the checked before-and-after goal states.

    theorem card_le_of_bad {n : ℕ} (hn : 3 ≤ n) {B : Finset (ZMod (2 * n - 1))}
    (hbad : ¬ IsGood n B) : B.card ≤ solution n - 1 := by
…

    Mentions: Imo1990P2.IsGood, Imo1990P2.solution

  10. theorem Imo1990P2.exists_bad Lower bound: there is a bad coloring with solution n - 1 black points line 202 source

    Source documentation

    Lower bound: there is a bad coloring with solution n - 1 black points.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, Exists, Finset, ZMod, HSub.hSub, HMul.hMul, And, Eq, Finset.card, Imo1990P2.solution, Not, Imo1990P2.IsGood

    Proof uses: NeZero, NeZero.mk, dite, HMod.hMod, Exists.intro, Finset.image, Finset.Icc, And.intro, id, Eq.mpr, ite, congrArg, ite_eq_left, Finset.card_image_of_injOn, Membership.mem, Set, Nat.ModEq, Iff.mp, ZMod.natCast_eq_natCast_iff, Eq.mp and 99 more

    147 instances, coercions and auxiliary constants left out.

    Tactic trace: 127 steps

    Open to load the checked before-and-after goal states.

    theorem exists_bad {n : ℕ} (hn : 3 ≤ n) :
    ∃ B : Finset (ZMod (2 * n - 1)), B.card = solution n - 1 ∧ ¬ IsGood n B := by
…

    Mentions: Imo1990P2.solution, Imo1990P2.IsGood

  11. problem Imo1990P2.imo1990_p2 line 317 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Nat, LE.le, OfNat.ofNat, IsLeast, Set.ofPred, Finset, ZMod, HSub.hSub, HMul.hMul, Eq, Finset.card, Imo1990P2.IsGood, Imo1990P2.solution

    Proof uses: And.intro, Membership.mem, Set, lowerBounds, Classical.byContradiction, Not, Imo1990P2.card_le_of_bad, dite, False, HMod.hMod, Eq.mp, ite, congrArg, ite_eq_left, ite_eq_right, And, Exists, Imo1990P2.exists_bad, Decidable.byContradiction, Nat.one_le_of_lt and 3 more

    29 instances, coercions and auxiliary constants left out.

    Tactic trace: 24 steps

    Open to load the checked before-and-after goal states.