Structures mathématiques finies : l'Annexe A de la MUH en Lean

[jsboige]

Part of #16741 — arc B — ouverte, responsable, prouvable, explicable

Livrable

Formaliser les définitions de l'Annexe A de R16 : définition d'une structure (ensembles + relations + générateurs + composition) ; Aut(S) est un groupe (le « easy to see » du papier = exercice idéal) ; théorème : l'équivalence de structures finies est décidable par algorithme haltant (énumération des tableaux) ; exemples C₂/C₃/algèbre de Boole générée par NAND seul.

Contenu à distiller

• Définition Lean d'une structure finie (ensembles, relations, générateurs, composition).
• Aut(S) est un groupe — formalisation de l'argument esquissé « easy to see ».
• Théorème de décidabilité de l'équivalence par énumération haltante.
• Exemples : C₂, C₃, algèbre de Boole générée par NAND.

Sources

• R16 — The Mathematical Universe (arXiv:0704.0646)
  PDF : G:\Mon Drive\MyIA\IA\Bibliographie IA\Consciousness\2007 - Tegmark - The Mathematical Universe.pdf (sha8 85712871)

Localisation papier : R16 Annexe A + §III — [DISTILL R16-3]

Cible (vérifiée contre le dépôt)

Même décision lake que T11.

Priorité et contraintes

P2 — Pont rare : un papier de cosmologie formel qui fournit des énoncés Lean nets. Cite T19 (le cadre conceptuel).

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- Annexe A MUH en Lean — structure finie + Aut(S) groupe + décidabilité énumération haltante + exemples C₂/C₃/Boole-NAND (lake T11)

(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

[jsboige]

[CLAIMED] lane myia-po-2027:CoursIA-2 -- Annexe A MUH en Lean

(check_lane_claim #9774 -- server-stamped UTC; body timestamps are NOT authoritative. Release with [RELEASED] when your PR lands.)

[jsboige]

[CLAIMED] lane myia-po-2024:CoursIA -- companion notebook for the MUH lake (Annexe A visiting), does NOT deliver the halting-decider criterion

Scope declare : paths: MyIA.AI.Notebooks/SymbolicAI/Lean/Lean-36-Structures-Finies-MUH.ipynb, MyIA.AI.Notebooks/SymbolicAI/Lean/README.md

Livre : un notebook compagnon natif (kernel lean4-wsl) qui importe et execute le lake tegmark_muh_lean (Structure/Encoding/Cyclic/Boolean/Aut/Decidable) et mesure ou en est le livrable de cette issue. Il ne re-implemente pas le lake et ne touche pas ses modules.

Etat mesure du livrable de #16753 (firsthand, main courant) :

Critere de l'issue	Etat
Definition Lean d'une structure finie	LIVRE (MUH/Structure.lean, #16942)
Aut(S) est un groupe	LIVRE (MUH/Aut.lean)
Theoreme : equivalence decidable par algorithme haltant	NON LIVRE — MUH/Decidable.lean porte un stub declare (decideEq compare nSets), et MUH.lean l'ecrit noir sur blanc : « pas un algorithme enumeratif haltant »
Exemples C2/C3/Boole par NAND	LIVRE (MUH/Cyclic.lean, MUH/Boolean.lean)

Le notebook rend cet ecart visible par une sortie : #eval Decidable.decideEq Cyclic.c3 Cyclic.c2 rend true alors que les deux structures ont des cardinaux differents (c3Sizes 0 = 3, c2Sizes 0 = 2).

Le claim myia-po-2027:CoursIA-2 du 2026-09-20 sur cette issue porte sur la formalisation Lean, non sur ce notebook ; les chemins sont disjoints.

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA-2 — prev: MED/docs #17935
[CLAIMED] lane myia-po-2025:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/Decidable.lean -- tranche de comparaison effective des structures finies (tables, cardinalités, signatures), distincte de l’équivalence par génération mutuelle encore ouverte. Aucun changement aux autres modules ni revendication de clôture de #16753.

[jsboige]

[CLAIMED] lane myia-po-2025:CoursIA -- residu mesure au 2026-10-02 : le lake tegmark_muh_lean est 100%% defs, 0 theorem, 0 sorry (count_code_sorry + grep theorem/lemma sur les 6 modules) -- tranche PREUVES : Aut(S) groupe (Aut.lean), correction de decideEq (Decidable.lean, decidabilite par enumeration haltante R16 Annexe A), proprietes des exemples C2/C3/Boole-NAND -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/*.lean

[jsboige]

Tranche PREUVES livre : PR #18812 — Aut(S) groupe (5 axiomes, sans Mathlib), 6 identites Sheffer (A2), exhaustivite Aut(C3)={id, x->2x} / Aut(C2)={id}, theoreme de correction du decideur (sameBinaryOperation_eq_iff). lake build SUCCESS 9 jobs, distinct_code_sorry 0 avant/apres. Claim paths: MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/** maintenu pour la suite eventuelle (residuel #16958 : equivalence Sheffer, Fin.pi, ClosedUnderComp).