Réfutation et contre-exemple
Une affirmation fausse est rejetée avec un contre-exemple concret, que le noyau vérifie lui aussi.
Une réponse aussi nette dans l’autre sens
Quand une affirmation est fausse, Slean ne répond pas « non prouvé ». Il cherche une configuration précise sur laquelle la quantité change, et le noyau vérifie ce calcul. Une réfutation est donc aussi sûre qu’une preuve.
Un exemple
Affirmation : « dans la règle 30, le nombre de cases noires ne change jamais ». Prenons un anneau de 3 cases, avec une seule case noire.
Le plus petit contre-exemple
- case 1 lit
100 → 1 - case 2 lit
001 → 1 - case 3 lit
010 → 1
Après un pas, les trois cases sont noires. Le nombre de cases noires passe de 1 à 3. L’affirmation est fausse, et cet anneau de 3 cases en est le témoin.
En Lean
theorem rule30_refuted :
¬ Conserved (eca 30) (tableFn 2 [0, 1]) 1 :=
not_conserved_of_witness _ _ 1 [0, 0, 1]
(by decide) (by decide +kernel) (by decide +kernel)Le théorème not_conserved_of_witness dit : si une configuration concrète voit son total changer en un pas, alors la quantité n’est pas conservée. Les trois vérifications finales contrôlent que le monde a au moins un état, que la configuration est valide, et que les deux totaux diffèrent.
Pourquoi c’est utile
- Une proposition fausse coûte une proposition au budget, et elle laisse une trace : la réfutation entre dans la bibliothèque.
- Un agent qui propose au hasard accumule des réfutations, ce que la mesure voit. Voir Mesurer une découverte.
- Les réfutations sont publiées avec les succès. C’est une des règles de mesure.
L’exemple détaillé est à la page Une loi réfutée.