6. Limites et état du développement🔗

Slean vérifie ici : la forme versionnée du dossier, les identifiants et références, l'ordre causal du journal, la comparaison décimale locale, le plafond de coût déclaré, la règle de promotion, les références des portes ET/OU et la projection d'audience. Il peut montrer une erreur précise ou conserver un résultat indéterminé.

Slean ne vérifie pas ici : que la mesure a été réellement prise, que les octets d'un artefact sont authentiques, que l'horloge externe ou l'évaluateur est fiable, qu'une porte ET/OU démontre sa cible, que la décision humaine est judicieuse, ou que l'affirmation scientifique est vraie. Le théorème Lean local porte sur une propriété conditionnelle du mécanisme, pas sur ces faits empiriques. Aucune vérification indépendante de preuve n'est configurée.

Ce site est un prototype local antérieur à la publication. Les exemples sont synthétiques. La licence publique, la visibilité du dépôt, le domaine et les intégrations restent des décisions distinctes. La construction exécute les tests et compile les exemples avant de générer le manuel. build-info.json indique le commit source, la propreté de l'arbre lorsque les métadonnées Git sont disponibles, le schéma, Lean et le tag sélectionné ; sans ces métadonnées, source_tree_clean vaut null car la propreté est inconnue. Un build sans tag reste une prévisualisation de développement.