Combien d'états faut-il pour reproduire les observations d'un système ? Le labo étudie des machines à mémoire finie, leurs erreurs de simulation et les stratégies d'observation, avec des hypothèses explicites sur les actions, l'horizon et la mémoire disponible.
Le dépôt rassemble modèles, manuscrits, certificats de calcul rationnel et modules Lean 4. Le README distingue les énoncés formalisés, les expériences finies et les extensions encore ouvertes ; chaque résultat reste attaché à son contrat mathématique.
C'est un compagnon de recherche public, pas une validation scientifique externe. La nouveauté et la priorité ne sont pas établies ; les cas traités ne ferment pas le programme général.