Mutome (site externe)
Menu

Le trafic (règle 184)

Pas à pas : pourquoi le nombre de voitures ne change jamais dans la règle 184, et ce que le théorème Lean démontre exactement.

Ce qu’on regarde

Une route circulaire de 28 cases. Une case noire est une voiture, une case blanche est libre. À chaque pas, toutes les voitures bougent en même temps selon une seule règle : avancer d’une case vers la droite si la case devant est libre, sinon attendre.

Règle 184 : le trafic

Vue

Pas 16 : 14 voitures

pasvoitures0141142143144145146147148149141014111412141314141415141614

voiturecase librenombre conservé

Simulation dans votre navigateur, convention centrée. Le nombre de voitures, à droite, ne change pas. La preuve, elle, vaut pour tous les anneaux.

Lire la figure pas à pas

  1. La première ligne est la route au départ, avec 14 voitures.
  2. Chaque ligne suivante est la route un pas plus tard. Le temps descend.
  3. Regardez une voiture isolée : elle avance d’une case à chaque ligne, en diagonale vers la droite.
  4. Regardez un bouchon : seule la voiture de tête peut avancer, les autres attendent. Le bouchon se défait par l’avant.
  5. Le nombre à droite de chaque ligne compte les voitures. Il vaut 14 à chaque ligne.

Pourquoi le nombre ne change pas

Une voiture ne disparaît jamais : elle reste sur place ou passe dans la case suivante. Et deux voitures n’arrivent jamais dans la même case, puisqu’une voiture n’avance que si la case devant est libre. Chaque changement d’une case est donc expliqué par une voiture qui traverse une frontière.

Ce qui sort d’une case entre dans la suivante

Vue

Pas 0 : 4 voitures franchissent une frontière

Pas 0Pas 1+10−1+1−1+1000−1+1−1variation de chaque case = ce qui entre − ce qui sort77

voitureune voiture franchit une frontièrenombre conservé

Chaque flèche est une voiture qui franchit une frontière. Une case perd ce qui sort et gagne ce qui entre ; autour de l’anneau, les pertes et les gains s’annulent.

C’est exactement ce que dit le certificat : la variation de chaque case égale ce qui entre moins ce qui sort. Autour de l’anneau, ce qui sort d’une case entre dans la suivante. Voir Affirmation et certificat.

L’énoncé Lean

Lean 4
theorem traffic :
    Conserved (eca 184) (tableFn 2 [0, 1]) 1 :=
  conserved_of_fluxCheck _ _
    (tableFn 2 [1, 1, 1, 1, 1, 1, 0, 0]) 1
    (by decide +kernel)

La bibliothèque contient la même loi sous une autre forme : elle compte les cases libres, avec la densité tableFn 2 [1, 0]. Sur un anneau de taille fixe, compter les cases libres ou compter les voitures revient au même.

Ce que cela démontre

Dans la règle 184 telle qu’elle est définie en Lean, le nombre de voitures ne change jamais, sur des anneaux de toutes les tailles et pour toutes les configurations de départ. Le noyau a vérifié le certificat sur les 16 motifs de 4 cases, et le théorème conserved_of_fluxCheck fait le reste.

Ce que cela ne démontre pas

  • Rien sur le vrai trafic routier. La règle 184 est un modèle, et c’est une preuve dans un monde.
  • Rien sur la vitesse ou les bouchons : seule la conservation du nombre de voitures est démontrée.
  • La figure n’est pas la preuve. Elle montre 16 pas sur une configuration ; la preuve vaut pour toutes.