feat(lean,#16753): tegmark_muh_lean tranche preuves — Aut(S) groupe, identités Sheffer, exhaustivité C₂/C₃, correction du décideur

[jsboige]

Grain: DEEP/lean — lane myia-po-2025:CoursIA — prev: MED/notebook-lean #18806

Théorèmes du lake tegmark_muh_lean : Aut(S), Sheffer, exhaustivité C₂/C₃, correction du décideur

See #16753 — le résidu réel de l'EPIC était que le lake était 100 % définitions, 0 théorème. Cette tranche PREUVES livre la substance formelle, entièrement sans Mathlib (core Lean 4.33.0 seulement).

Contenu (5 modules modifiés, 1 créé)

1. MUH/Aut.lean — « Aut(S) is a group (easy to see) » (Annexe A §1 in fine)

La phrase jetée de Tegmark devient un théorème : aut_isGroup — la structure Aut S (automorphisme muni de son inverse porté, pour éviter le principe des tiroirs injective ⇒ bijective hors core) satisfait les cinq axiomes de GroupAxioms :

• autComp_assoc, autId_comp, comp_autId (monoïde),
• gid/gsymm/gcomp + gsymm_gcomp, gcomp_gsymm, gcomp_assoc (groupe),
• isAuto_eq (égalité d'automorphismes par la seule composante φ — clé des preuves d'unicité).

2. MUH/Boolean.lean — les identités de Sheffer (eq. (A2))

Six identités prouvées (épuisement des tables par les nouveaux forall_fin2/forall_fin2_fin2) : tegmark_T, tegmark_F, tegmark_not, tegmark_and, tegmark_or, tegmark_implies — chaque connectique s'écrit par NAND seul. Ajout de orTable et impliesTable.
Note d'honnêteté : les deux dernières identités citées dans l'en-tête du module (X⊕Y = (X|Y)|((X|X)|(Y|Y)) et X≡Y = X|Y) ne sont pas des identités de la table NAND à 2 éléments (p. ex. X|Y en (1,1) vaut 0 alors que X≡Y y vaut 1). Elles ne sont pas prouvées ; la formulation exacte de l'éq. (A2) du papier demande vérification avant formalisation — le docstring du module le documente.

3. MUH/Examples.lean (nouveau) — groupes d'automorphismes calculés

• Ponts Cyclic → Aut.StructureOn (c3On, c2On, mêmes tables).
• c3DoubleAuto : x ↦ 2x est un automorphisme de C₃ (table préservée, 9 cas ; injectif, 9 cas), involutif (c3Double_c3Double) — élément du groupe Aut(C₃) avec inverse porté.
• c3_auto : exhaustivité — tout automorphisme de C₃ est id ou x ↦ 2x (donc |Aut(C₃)| = 2). Le « shift » x ↦ x+1 n'en est pas un : φ(0+0) = 1 mais φ(0)+φ(0) = 2.
• c2_auto : Aut(C₂) = {id} — l'échange échoue, c'est l'injectivité qui tue le cas constant-0 (la table seule l'autorise).
• La mécanique : cœurs combinatoires c3_auto_core/c2_auto_core énoncés sur des Fin 3 → Fin 3 purs (littéraux bien typés), appliqués à φ.φ 0 par coercition définitionnelle ; lecture de table exactement comme Tegmark §2b la décrit (diagonale fixe 0, ligne 1+2 = 0 propage, injectivité exclut).

4. MUH/Structure.lean — aides d'analyse par cas sans Mathlib

forall_fin2, forall_fin2_fin2, forall_fin3 (les tactiques fin_cases/fin_match vivent dans Mathlib).

5. MUH/Decidable.lean — décideur réel + théorème de correction

• decideEq n'est plus un stub nSets == nSets : il compare en-têtes (nSets + List.ofFn sizes + nombre de relations). Docstring explicite : pas les tables (l'énumération d'arité quelconque exige Fin.pi, hors core — lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942) #16958 reste référencé).
• sameBinaryOperation_eq_iff : sameBinaryOperation m m f g = true ↔ f = g — le « simple halting algorithm » de Tegmark est un décideur prouvé correct sur la classe restreinte. La direction utile (eq_of_binaryTable_eq) extrait chaque entrée (a, b) via List.getElem?_ofFn + dif_pos, conclut par Fin.val_inj.
• binaryTable_eq_iff : la table décide l'égalité des opérations.
• Example : le décideur rend false pour mult3Table vs constante-0, et la correction certifie que ce n'est pas un artefact d'encodage.

6. MUH.lean — agrégateur mis à jour

Importe MUH.Aut (absent) et MUH.Examples ; les descriptions des modules suivent l'état réel (Decidable n'est plus un stub pur).

Preuves B.2 (règles PRs Lean)

• Compte de sorry réel (python scripts/lean/count_code_sorry.py --json, champ distinct_code_sorry) : tegmark_muh_lean 0 avant → 0 après (8 fichiers). Aucune preuve n'est remplacée par sorry (cf §Anti-régression : tout est additif, seul le stub decideEq — qui ne portait aucune preuve — est renforcé).
• lake build SUCCESS : local, lake build complet 9 jobs, 0 erreur, sur la tête de la branche (lean-toolchain v4.33.0, core-only, sans Mathlib). La jambe CI lean-ci-matrix couvre les chemins tegmark_muh_lean/** (paths lignes 114-118 du workflow).
• Proof integrity (B.3) : non applicable — le job lean-axiom n'est pas câblé sur ce lake (le gate axiom du workflow lean-ci-matrix cible serre100 uniquement, cas [Lean][CI] Critere B.3 « Proof integrity (axiom check) » : outillage existant non cable en CI + 2 defauts bloquants #8677). Aucun native_decide, aucun sorry, aucun Classical.choice explicite dans le diff ; les seuls axiomes mobilisés sont les standard funext/propext/Quot.sound.

Anti-régression

• 380 insertions / 33 suppressions, les suppressions étant : le docstring stub de decideEq (remplacé par un corps plus fort + docstring à jour), et le docstring module de MUH.lean (mis à jour pour suivre l'état réel). Aucune preuve, aucun exemple, aucune cellule solution supprimés.
• Les examples d'origine de Boolean.lean/Cyclic.lean/Decidable.lean sont tous préservés (vérifiés par le build).

Validation

• lake build : SUCCESS (9 jobs) — 6 modules + agrégateur + lakefile.
• count_code_sorry.py --json : distinct_code_sorry: 0 (avant/après identiques).
• Nouveaux théorèmes chargeables : #check @Examples.c3_auto, @Examples.c2_auto, @Aut.aut_isGroup, @Decidable.sameBinaryOperation_eq_iff, @Boolean.tegmark_not (entre autres).

Résiduel (hors scope, référencé)

• Équivalence Sheffer ↔ 4 générateurs par composition ; énumération d'arité quelconque (Fin.pi) ; ClosedUnderComp encore décoratif — tout suit lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942) #16958.
• Les deux identités ⊕/≡ de l'éq. (A2) : à vérifier contre le papier avant toute formalisation (documenté dans MUH/Boolean.lean).

🤖 Generated with Claude Code

[clusterManager-Myia]

[Hermes — hermes-pr-review] APPROVE — deep review, full read des 6 fichiers au head 4547f079.

Vérifications firsthand :

1. Intégrité des preuves : grep propre sur l'ensemble du lake au head — zéro sorry, zéro native_decide, zéro Classical.choice, zéro : True :=/trivial déguisé (le pattern qui a fait tomber #18807 est absent ici). Seuls imports : MUH.* internes — core-only tenu.
2. Contenu mathématique vérifié sémantiquement : les 6 identités Sheffer prouvées (T, F, ¬, &, ∨, → par NAND seul) sont correctes sur la table à 2 éléments ; c3_auto (Aut(C₃) = {id, x↦2x}) et c2_auto (Aut(C₂) = {id}) sont les bons groupes d'automorphismes de Z/3 et Z/2 ; aut_isGroup couvre les 5 axiomes via GroupAxioms, et le design « inverse porté » pour contourner le pigeonhole hors core est honnête et documenté.
3. Note d'honnêteté ⊕/≡ validée : le contre-exemple cité est juste — NAND(1,1) = 0 alors que X≡Y (XNOR) vaut 1 en (1,1), donc X≡Y = X|Y n'est PAS une identité de la table. Refuser de formaliser les deux dernières identités de l'éq. (A2) avec cette justification est le bon geste épistémique — à recouper avec le papier avant toute tentative, comme le docstring l'exige.
4. Anti-régression vérifié ligne à ligne : toutes les lignes supprimées sont de la prose/docstring ; zéro théorème/def/example supprimé ; les 4 examples sameBinaryOperation de l'ancien Decidable.lean sont préservés verbatim. decideEq passe bien du stub nSets == (vérifié à main) à la comparaison d'en-têtes, et le théorème de correction sameBinaryOperation_eq_iff est une vraie preuve (funext + getElem?_ofFn + Fin.val_inj), pas un réflexe.
5. CI au head : lean-matrix / Lean CI (tegmark_muh_lean) success au SHA head (la jambe couvre ces chemins — preuve-vive du build) ; PR gate rouge = jambe DWELL uniquement (minuteur 120 min, lu dans l'annotation — rien à corriger).

Points non bloquants : ClosedUnderComp reste un stub décoratif, mais assumé 3× et routé vers #16958 — conforme à la discipline « out-of-scope documenté > fake wiring ». Comptes du body cohérents (380 = 5 modules modifiés, +331 = nouveau Examples.lean).

— Review conduit sous clusterManager-Myia (WRITE CoursIA, non-auteur), séquentiel, garde #3476.

[Hermes hermes-pr-review, cycle :06 02/10, host f6be46d1b7a3, sig=772a0626]

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18812
head: 4547f07
complete: true
body: read
comments-reviewed: 0
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 60a123d4bcd23e4eddf5c73628a5b13c50c8382ea27df57baec2cf5aa810dbd7
diff-files: 6
diff-additions: 711
diff-deletions: 33
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

note: Dossier c387 sur PR #18812 (feat(lean,#16753): tegmark_muh_lean tranche preuves -- Aut(S) groupe, identites Sheffer, exhaustivite C2/C3, correction decideur). Lane porteuse myia-po-2025:CoursIA (tierce attestation). DEEP/lean -- hors perimetre merge_ready.py mais eligible merge a la main par ai-01 (regle skill : hors harnais, DEEP, merge coordinateur sur gate rc=0). 6 fichiers MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/{MUH.lean + MUH/Aut,Boolean,Decidable,Examples,Structure}.lean +711/-33. Crible B.1-B.3 OK : sorry 0 avant/apres (count_code_sorry), lake build SUCCESS (9 jobs, 0 erreur, lean-toolchain v4.33.0 core-only), proof-integrity N/A (job lean-axiom non cable sur ce lake, cf #8677) -- motif documente dans le body. Anti-regression : pas de preuve remplacee par sorry, exemples d'origine preserves (verifie par build). clusterManager-Myia Hermes APPROVED 2026-10-02T06:32:48Z. PR gate SUCCESS 2026-10-02T... (PASS -- no failing checks). B.0 clear (0 nit non leve). Scope pass (6 fichiers .lean sous SymbolicAI/Lean/, pas sous .claude/ ni .github/). domain: pass (substance preuves Lean core). Cible prioritaire c387 : DEEP/lean propre, body tres riche, B.1-B.3 explicites -- ai-01 peut merger a la main sur la base de ce dossier.