# Relecture de SERIS — 1er octobre 2026

## Fait local et périmètre

Le préprint v5-bis, la documentation du prototype et `src/CLARA_DEMO/demo_official/seris/formal/hallucination_impossibility.lean` ont été relus. La v5.1 est une nouvelle édition autorisée pour le site de l’auteur. Les anciens préprints, propositions privées, présentations et sources exécutables restent inchangés.

## Corrections de fond

- L’exclusion d’une branche prouve une admissibilité relative aux prédicats et aux entrées vérifiées, sous conditions. Elle ne prouve pas une impossibilité générale d’halluciner, une vérité des observations ou une sécurité du monde réel.
- La formalisation Lean contient un `sorry` dans `selectBest_mem`. Le théorème dépendant est donc présenté comme un développement incomplet, sans revendiquer une nouvelle vérification machine. Voir la documentation primaire de Lean sur [les preuves](https://lean-lang.org/doc/reference/latest/ValidatingProofs/) et [les axiomes](https://lean-lang.org/doc/reference/latest/Axioms/).
- Le terme vectoriel ajouté à une équation scalaire est remplacé par un couplage scalaire proposé. Un champ constant non nul réfute l’équivalence antérieure entre petites dérivées et convergence vers zéro.
- TopK renvoie des branches et précise les égalités et l’absence de candidat. FOA-3 explicite une séquence de contrôles ; sa formule ne démontre pas une supériorité sur FOA-2 déjà filtré.
- Un poids négatif ne supprime pas une branche : la compatibilité stricte exige un prédicat d’exclusion.
- Le seuil de score du cas à cinq cellules est séparé des contrôles structurels exécutables avant scoring.
- Une géométrie compressée ne garantit pas la reconstruction exacte de toute histoire. Les données nécessaires à un audit doivent être conservées et leur coût assumé.
- Le champ, les signaux et la mémoire résonante sont présentés comme des propositions à spécifier et à évaluer, distinctes du noyau borné.

## Décision éditoriale

Les comparaisons universelles avec les LLM, les journaux et les autres systèmes sont remplacées par des comparaisons de rôles et de mécanismes. Le texte reconnaît la composition ML/raisonnement automatisé déjà documentée dans le prototype. Il conserve les idées et les questions ouvertes sans attribuer une insuffisance générale aux personnes ou à leurs choix.

Le nom du projet est SERIS, « Structured Exact Reasoning & Inference System ». FOA y signifie « Field of Attention Operator », à distinguer du corpus « Fractal Ontological Architectures » publié séparément.

## Limites de validation

La relecture porte sur la cohérence des énoncés et leur diplomatie. Elle n’est ni une évaluation par les pairs, ni un audit de déploiement, ni une reproduction des benchmarks historiques. Aucun runtime n’a été remis en service. Le nouveau seal atteste de l’intégrité et de la signature des fichiers de cette édition uniquement.