Poteaux pourris

Preuve en vidéo : https://youtu.be/x5tfCXnLW3U
On modélise les $17$ poteaux pourris comme les points de l’ensemble $\mathbb{U}_{17}=\left\{e^{i\frac{2k\pi}{17}}\mid 0\leq k\leq 16\right\}$ et les poteaux pourris comme une partie $P\subset \mathbb{U}_{17}$ de $5$ éléments. On note $I_m=\{e^{i\frac{2k\pi}{17}}\mid m\leq k\leq m+6\}$ les intervalles de $7$ poteaux consécutifs.

Cas 1 : il existe $I_m$ contenant $d\geq 3$ poteaux pourris.
Dans ce cas l’intervalle $I_{m+7}$, disjoint de $I_m,$ contient au plus les deux poteaux pourris restants. Or si $I_m$ contient $d$ poteaux pourris alors $I_{m+1}$ en contient soit $d-1,$ soit $d$, soit $d+1.$ Autrement dit, le nombre de poteaux pourris d’écart entre deux intervalles consécutifs est d’au plus $1.$ Ainsi, parmi les intervalles $I_m,\dots,I_{m+6}$, au moins un contient $3$ poteaux pourris (on peut voir cela comme une sorte de version discrète du théorème des valeurs intermédiaire).

Cas 2 : tous les $I_m$ contiennent moins de $2$ poteaux pourris.
On va montrer par l’absurde que ce cas n’arrive pas.
On pose $f\colon m\in\{0,\dots,16\}\longmapsto \#(I_m\cap P)$, la fonction qui à $m$ associe le nombre de poteaux pourris contenus dans $I_m$. Quel que soit l’ensemble $P$ choisi on aura toujours
$$\sum_{m=0}^{16}f(m)=5\times7=35$$car chacun des $5$ poteau pourris appartient à exactement $7$ intervalles $I_m$ (il s’agit d’un invariant). Or, par hypothèse, $\forall m\in\{0,\dots,16\},f(m)\leq 2$ donc
$$35=\sum_{m=0}^{16}f(m)\leq 2\times 17=34$$ ce qui est absurde.