En fait je me suis rendu compte que mon idée de preuve reposait sur l'argument
$mathjax$8+1 < 9$mathjax$
, c'était pas hyper satisfaisant… ^^ Donc pour l'instant je n'ai pas de preuve jolie en fait.
En revanche, on peut baisser le nombre de graphes à considérer pour le cas
$mathjax$p = 4$mathjax$
à de l'ordre de 400, donc j'ai pu faire une recherche exhaustive sans trop de raffinement (
i.e. Python et produit matriciel naïf pour tester les solutions), et n'en ai pas trouvé.
Je détaille ici comment je pense qu'on peut réduire le nombre de cas, en cherchant des conditions nécessaires sur la forme d'un tel graphe.
Supposons qu'on ait un tel graphe.
On prend
$mathjax$s_0$mathjax$
un sommet.
On sait que
$mathjax$s_0$mathjax$
a
$mathjax$4$mathjax$
voisins. On note
$mathjax$N = \{s_1, s_2, s_3, s_4\}$mathjax$
l'ensemble de ses voisins.
Les autres sommets
$mathjax$s_5, …, s_{16}$mathjax$
doivent être à distance
$mathjax$2$mathjax$
de
$mathjax$s_0$mathjax$
, donc chacun est nécessairement voisins d'au moins un sommet de
$mathjax$N$mathjax$
. De plus ils sont voisins chacun d'au plus un sommet de
$mathjax$N$mathjax$
, sinon si on en a un relié à deux sommets de
$mathjax$N$mathjax$
, on obtient deux chemins de longueur 2 dudit sommet à
$mathjax$s_0$mathjax$
.
Le graphe a donc nécessairement cette forme (avec encore des arêtes en plus bien sûr ! ^^) :
Show/Hide spoilerAfficher/Masquer le spoiler
On a de plus saturé le degré de
$mathjax$s_0$mathjax$
et des sommets de
$mathjax$N$mathjax$
. Les arêtes supplémentaires impliqueront donc uniquement des sommets de
$mathjax$s_5$mathjax$
à
$mathjax$s_{16}$mathjax$
(on note
$mathjax$S$mathjax$
l'ensemble de ces sommets, et pour
$mathjax$i\in\{0,1,2,3\}, S_i = \{s_{3i+5}, s_{3i+6}, s_{3i+7}\}$mathjax$
Maintenant pour avancer on passe à quelques arguments de type «Sudoku» (c'est un peu le même genre de raisonnement je trouve ^^) :
→
$mathjax$s_5$mathjax$
doit être en particulier à distance 2 des sommets
$mathjax$s_2, s_3, s_4$mathjax$
. Comme ceux-ci sont saturés, tout comme
$mathjax$s_0$mathjax$
, on doit passer par des sommets voisins de
$mathjax$s_2, s_3, s_4$mathjax$
:
$mathjax$s_5$mathjax$
doit avoir au moins un voisin dans
$mathjax$S_1$mathjax$
, un dans
$mathjax$S_2$mathjax$
et un dans
$mathjax$S_3$mathjax$
. Sans perte de généralité, on arrive à avoir ces trois nouvelles arêtes :
Show/Hide spoilerAfficher/Masquer le spoiler
→ En raisonnant de même avec
$mathjax$s_6$mathjax$
et
$mathjax$s_7$mathjax$
, avec le fait que deux sommets de
$mathjax$S_0$mathjax$
ne peuvent pas être voisins d'un même sommet de
$mathjax$S_i$mathjax$
pour
$mathjax$i\geq1$mathjax$
(sinon ça nous donne deux chemins de longueur 2 du voisin commun vers
$mathjax$s_1$mathjax$
) on a nécessairement cette forme :
Show/Hide spoilerAfficher/Masquer le spoiler
Il nous reste donc
$mathjax$9$mathjax$
arêtes à placer, impliquant uniquement des sommets de
$mathjax$S_1 \cup S_2 \cup S_3$mathjax$
car on vient de saturer les sommets de
$mathjax$S_0$mathjax$
.
→
$mathjax$s_8, s_9$mathjax$
et
$mathjax$s_10$mathjax$
doivent être à distance 2 de
$mathjax$s_3$mathjax$
. On doit ajouter pour chacun une arête le reliant à un sommet de
$mathjax$S_2$mathjax$
. De plus on ne doit pas relier deux sommets de la même couleur (sur le coloriage ci-dessus), sinon ça nous donnerait un chemin de longueur 2 et un chemin de longueur 1 vers le sommet de
$mathjax$S_0$mathjax$
dont est issue la couleur, ce qui est proscrit par l'identité matricielle. On a donc deux possibilités pour placer ces trois arêtes, où deux est le nombre de permutations de
$mathjax$\{1,2,3\}$mathjax$
sans point fixe.
——→ Soit on a
$mathjax$\{s_8,s_{12}\}, \{s_9,s_{13}\}, \{s_{10},s_{11}\}$mathjax$
à ajouter aux arêtes.
——→ Soit on a
$mathjax$\{s_8,s_{13}\}, \{s_9,s_{11}\}, \{s_{10},s_{12}\}$mathjax$
à ajouter aux arêtes.
Pour chacun de ces choix, on a le choix dual à faire pour mettre les sommets de
$mathjax$S_1$mathjax$
à distance 2 de
$mathjax$s_4$mathjax$
(i.e. on choisira l'association qui correspond à l'autre permutation des couleurs), donc, par symétrie, ce choix n'est pas vraiment important. Sans perte de généralité, on a maintenant la forme (en violet et jaune sont les arêtes que l'on vient de rajouter, ça commence à être un peu le bazar je sais…) :
Show/Hide spoilerAfficher/Masquer le spoiler
On vient de plus de saturer les sommets de
$mathjax$S_1$mathjax$
. Il reste 3 arêtes à placer impliquant les sommets de
$mathjax$S_2 \cup S_3$mathjax$
.
C'est à partir de là que j'ai lancé la recherche exhaustive et n'ai rien trouvé.
Le risque est que j'ai me sois grossièrement planté quelque part dans l'établissement de ces conditions nécessaires, mais je pense que c'est assez propre déjà.
Je publierai le programme qui fait la recherche une fois que je l'aurai un peu nettoyé si tu veux le vérifier, pour l'instant il doit être assez peu lisible. ^^
Je pense qu'en y réfléchissant un peu plus on peut comprendre pourquoi ça coince sur ce cas à la main une fois qu'on a une forme bien définie du graphe, et ça pourrait donner la piste pour montrer le cas général.
by 
