mathlib3 documentation

mathlib-archive / imo.imo2006_q5

IMO 2006 Q5 #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 imo2006_q5.int.nat_abs_eq_of_chain_dvd {l : cycle } {x y : } (hl : cycle.chain has_dvd.dvd 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 imo2006_q5.int.add_eq_add_of_nat_abs_eq_of_nat_abs_eq {a b c d : } (hne : a b) (h₁ : (c - a).nat_abs = (d - b).nat_abs) (h₂ : (c - b).nat_abs = (d - a).nat_abs) :
a + b = c + d

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

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

theorem imo2006_q5 {P : polynomial } (hP : 1 < P.nat_degree) {k : } (hk : 0 < k) :

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