# Documentation

Archive.Imo.Imo2006Q5

# IMO 2006 Q5 #

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$.

## Sketch of solution #

The following solution is adapted from https://artofproblemsolving.com/wiki/index.php/2006_IMO_Problems/Problem_5.

Let $P^k$ denote the polynomial $P$ composed with itself $k$ times. We rely on a key observation: if $P^k(t)=t$, then $P(P(t))=t$. We prove this by building the cyclic list $(P(t)-t,P^2(t)-P(t),\ldots)$, and showing that each entry divides the next, which by transitivity implies they all divide each other, and thus have the same absolute value.

If the entries in this list are all pairwise equal, then we can show inductively that for positive $n$, $P^n(t)-t$ must always have the same sign as $P(t)-t$. Substituting $n=k$ gives us $P(t)=t$ and in particular $P(P(t))=t$.

Otherwise, there must be two consecutive entries that are opposites of one another. This means $P^{n+2}(t)-P^{n+1}(t)=P^n(t)-P^{n+1}(t)$, which implies $P^{n+2}(t)=P^n(t)$ and $P(P(t))=t$.

With this lemma, we can reduce the problem to the case $k=2$. If every root of $P(P(t))-t$ is also a root of $P(t)-t$, then we're done. Otherwise, there exist $a$ and $b$ with $a\ne b$ and $P(a)=b$, $P(b)=a$. For any root $t$ of $P(P(t))-t$, defining $u=P(t)$, we easily verify $a-t\mid b-u$, $b-u\mid a-t$, $a-u\mid b-t$, $b-t\mid a-u$, which imply $|a-t|=|b-u|$ and $|a-u|=|b-t|$. By casing on these equalities, we deduce $a+b=t+u$. This means that every root of $P(P(t))-t$ is a root of $P(t)+t-a-b$, and we're again done.

theorem Imo2006Q5.Int.natAbs_eq_of_chain_dvd {l : } {x : } {y : } (hl : Cycle.Chain (fun x x_1 => x x_1) l) (hx : x l) (hy : y l) :

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

theorem Imo2006Q5.Int.add_eq_add_of_natAbs_eq_of_natAbs_eq {a : } {b : } {c : } {d : } (hne : a b) (h₁ : Int.natAbs (c - a) = Int.natAbs (d - b)) (h₂ : Int.natAbs (c - b) = Int.natAbs (d - a)) :
a + b = c + d
theorem Imo2006Q5.Polynomial.isPeriodicPt_eval_two {P : } {t : } (ht : t Function.periodicPts fun x => ) :
Function.IsPeriodicPt (fun x => ) 2 t

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

theorem Imo2006Q5.Polynomial.iterate_comp_sub_X_ne {P : } (hP : ) {k : } (hk : 0 < k) :
)^[k] Polynomial.X - Polynomial.X 0
theorem Imo2006Q5.imo2006_q5' {P : } (hP : ) :

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

theorem imo2006_q5 {P : } (hP : ) {k : } (hk : 0 < k) :
Finset.card (Multiset.toFinset (Polynomial.roots ()^[k] Polynomial.X - Polynomial.X)))

The general problem follows easily from the k = 2 case.