Compfiles/Imo2006P5.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

6 declarations, 0 contain sorry, 0 declared as axioms

International Mathematical Olympiad 2006, Problem 5

Let $P(x)$ be a polynomial of degree $n>1$ with integer coefficients, and let $k$ be a positive integer. Consider the polynomial $Q(x) = P(P(\ldots P(P(x))\ldots))$, where $P$ occurs $k$ times. Prove that there are at most $n$ integers $t$ such that $Q(t)=t$.

Imports (3)
Imported by 1 file
  1. theorem Imo2006P5.Int.natAbs_eq_of_chain_dvd If every entry in a cyclic list of integers divides the next, then they all have the same absolute value line 63 source

    Source documentation

    If every entry in a cyclic list of integers divides the next, then they all have the same absolute value.

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

    Statement uses: Cycle, Int, Cycle.Chain, Dvd.dvd, Membership.mem, Eq, Nat, Int.natAbs

    Proof uses: Int.natAbs_eq_of_dvd_dvd, Eq.mp, congrArg, propext, Cycle.chain_iff_pairwise

    6 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    theorem Int.natAbs_eq_of_chain_dvd {l : Cycle ℤ} {x y : ℤ} (hl : l.Chain (· ∣ ·)) (hx : x ∈ l)
    (hy : y ∈ l) : x.natAbs = y.natAbs := by
…
  2. theorem Imo2006P5.Int.add_eq_add_of_natAbs_eq_of_natAbs_eq line 68 source

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

    Statement uses: Int, Ne, Eq, Nat, Int.natAbs, HSub.hSub, HAdd.hAdd

    7 instances, coercions and auxiliary constants left out.

    Tactic trace: 1 steps

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

  3. theorem Imo2006P5.Polynomial.isPeriodicPt_eval_two The main lemma in the proof: if $P^k(t)=t$, then $P(P(t))=t$ line 74 source

    Source documentation

    The main lemma in the proof: if $P^k(t)=t$, then $P(P(t))=t$.

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

    Statement uses: Polynomial, Int, Membership.mem, Set, Function.periodicPts, Polynomial.eval, Function.IsPeriodicPt, OfNat.ofNat, Nat

    Proof uses: Cycle, Cycle.map, HSub.hSub, Function.periodicOrbit, Nat.iterate, HAdd.hAdd, Eq.mpr, Exists, And, Eq, id, congrArg, propext, Cycle.mem_map, Nat.succ, Function.iterate_succ_apply', Exists.intro, And.intro, Function.iterate_mem_periodicOrbit, rfl and 52 more

    57 instances, coercions and auxiliary constants left out.

    Tactic trace: 42 steps

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

    theorem Polynomial.isPeriodicPt_eval_two {P : Polynomial ℤ} {t : ℤ}
    (ht : t ∈ periodicPts fun x => P.eval x) : IsPeriodicPt (fun x => P.eval x) 2 t := by
…

    Mentions: P

  4. theorem Imo2006P5.Polynomial.iterate_comp_sub_X_ne line 133 source

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

    Statement uses: Polynomial, Int, LT.lt, Nat, OfNat.ofNat, Polynomial.natDegree, Ne, HSub.hSub, Nat.iterate, Polynomial.comp, Polynomial.X

    Proof uses: Eq.mpr, id, Eq, congrArg, propext, sub_ne_zero, ne_of_apply_ne, And, Not, Eq.trans, HPow.hPow, congr, HMul.hMul, Polynomial.natDegree_iterate_comp, Polynomial.natDegree_X, mul_one, Or, Eq.mp, LT.lt.ne', one_lt_pow₀

    62 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

  5. theorem Imo2006P5.imo2006_p5' We solve the problem for the specific case k = 2 first line 140 source

    Source documentation

    We solve the problem for the specific case k = 2 first.

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

    Statement uses: Polynomial, Int, LT.lt, Nat, OfNat.ofNat, Polynomial.natDegree, LE.le, Finset.card, Multiset.toFinset, Polynomial.roots, HSub.hSub, Polynomial.comp, Polynomial.X

    Proof uses: Eq, Eq.mpr, id, congrArg, Polynomial.natDegree_sub_eq_left_of_natDegree_lt, congrFun', Polynomial.natDegree_X, Eq.refl, Ne, False.elim, False, LE.le.not_gt, zero_le_one, Eq.mp, Eq.symm, Polynomial.natDegree_zero, dite, Finset, LE.le.trans, Finset.card_le_card and 39 more

    81 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

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

    theorem imo2006_p5' {P : Polynomial ℤ} (hP : 1 < P.natDegree) :
    (P.comp P - X).roots.toFinset.card ≤ P.natDegree := by
…

    Mentions: P

  6. problem Imo2006P5.imo2006_p5 line 198 source

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

    Statement uses: Polynomial, Int, LT.lt, Nat, OfNat.ofNat, Polynomial.natDegree, LE.le, Finset.card, Multiset.toFinset, Polynomial.roots, HSub.hSub, Nat.iterate, Polynomial.comp, Polynomial.X

    Proof uses: LE.le.trans, Finset.card_le_card, Membership.mem, Finset, Ne, id, Eq.mp, Not, Eq, congrFun', congrArg, Polynomial.comp_X, Imo2006P5.Polynomial.iterate_comp_sub_X_ne, zero_lt_two, Polynomial.IsRoot, Polynomial.isRoot_of_mem_roots, Iff.mp, Multiset, Multiset.mem_toFinset, Eq.mpr and 16 more

    50 instances, coercions and auxiliary constants left out.

    Tactic trace: 7 steps

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