Skip to content

lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942) #16958

Closed
#17431
Closed
lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942)#16958
#17431

Description

@jsboige
jsboige
opened on Sep 20, 2026

[suivi de PR #16942, Hermes review c.722 — ouvert AVANT merge alinea 3 B.0]

Concerns ouverts sur #16942 (non leves dans la PR courante)

Concern #1 — Rel.table typing deguere

Verdict Hermes : type de Rel.table dans MUH/Structure.lean line 60 — curryfie (i : Fin sig.arity) → (Fin (sizes (sig.args i))) → Fin (sizes sig.out) traite i comme un INDEX et non comme un argument du produit.

Cas concrets :

  • Boolean.fullBoolean.NOT : a : Fin 1 puis castSucc rend 0 → 1 constant → la relation NOT committée est la constante 1, pas la negation.
  • Cyclic.mult3 : sig.arity = 2, table : Fin 2 → Fin 3 → Fin 3 → la 1re entree prend 2 valeurs (Fin 2) au lieu de 3 (Fin 3) → pas la loi du groupe C3.

Fix attendu : retyper en (args : (i : Fin sig.arity) → Fin (sizes (sig.args i))) → Fin (sizes sig.out) (fonction tuple). Implique de modifier fullBoolean (table NOT/AND/F/T), sheffer (NAND), c2 (mult2), c3 (mult3), et Aut.IsAutomorphism.rel_pres (c.716 introduit une preuve qui utilise r.table i (args i) — doit passer a r.table args).

Concern #2 — Ecart claim/code sur la decidabilite (Decidable.lean)

Verdict Hermes :

  • Decidable.decideEq = stub (`s1.nSets == s2.nSets)), MUH.lean annonce un algorithme enumeratif haltant qui n'existe pas dans le code.
  • inductive ClosedUnderComp est vide (constructeur trivial seul) → decoratif.
  • Boolean.lean annonce une equivalence Sheffer/8-generateurs (Tegmark eq. A2) ; le code ne porte que 4 example ... := rfl sur des valeurs de tables, pas de generation par composition, pas de theoreme d'equivalence.

Fix attendu : OU re-ecrire MUH.lean/README au scope reel (Encoding limite au preambule, admis par le code), OU implementer l'enumeration annoncee + la generation par composition + le theoreme d'equivalence (plus lourd).

Concern #3 — CI [RESOLU dans #16942 c.722]

Ajout tegmarkmuh au manifeste scripts/lean/ci_lakes.json + 4 paths ajoutes au push+pull_request blocks de .github/workflows/lean-ci-matrix.yml. scripts/ci/check_lake_matrix_paths.py rend OK 19 lakes, union coherent. Commit 4363a3fae303.

Plan

  1. Pousse une PR par concern (scindees pour granularite de review).
  2. Concern feat: add stiegler or tools #1 herite de la dependance Lean centrale — se prete a un refactor en lake isole (zéro Mathlib, toolchain v4.33.0).
  3. Concern Genetic sharp playground #2 herite de la discipline doc-vs-code : un audit cross-file (MUH.lean + README + Decidable.lean + Boolean.lean) decide si on re-ecrit la doc ou on implemente.

Liens

Activity

  1. jsboige commented on Sep 20, 2026

    @jsboige
    jsboige
    on Sep 20, 2026
    OwnerAuthor

    Grain: DEEP/lean -- lane myia-po-2027:CoursIA-2 -- prev: MED/docs #16969

    [CLAIMED] lane myia-po-2027:CoursIA-2 -- tegmark_muh_lean retypage Rel.table (Concern #1 Hermes) ; périmètre : MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/{Structure,Boolean,Cyclic,Aut}.lean + tests example/rfl

    [CLAIMED-AMEND] lane myia-po-2027:CoursIA-2 -- paths: MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/**/*.lean

    Concern #2 (Décidabilité claim/code) reste ouvert, livraison séparée — sa portée (énumération haltante OU réécriture scope) demande un arbitrage au coordinateur.

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

  2. jsboige
    added a commit that references this issue on Sep 20, 2026

    fix(lean,#16958): retype Rel.table as dependent-tuple function (Herme…

    e6194d7

  3. jsboige commented on Sep 20, 2026

    @jsboige
    jsboige
    on Sep 20, 2026
    OwnerAuthor

    Concern #1 LEVÉ c.726 (head e6194d7 sur feature/lean-muh-annex-a-16753) :

    • Rel.table retypé en tuple curryfié (args : (i : Fin sig.arity) → Fin (sizes (sig.args i))) → Fin (sizes sig.out)
    • Boolean.NOT n'est plus constante 1 ; mult3Table est la table 3×3 complète (9/9 cases, dont (2,2)→1)
    • Aut.IsAutomorphism.rel_pres : pointwise transport du tuple, autComp preuve mécanique (simp only [Function.comp_apply] + double rw)
    • Build : lake build MUH 8/8 jobs OK ; 0 sorry ; example defaultBinary3 couvre l'évaluation curryfiée

    PR #16942 amendée (body v3) avec section Concern #1 LEVÉ + Concern #2 OUVERT explicite. Hermes re-request-review triggered sur le nouveau head.

    Concern #2 (Décidabilité claim/code — Decidable.decideEq stub, équivalence Sheffer/8-gen) reste hors-scope de cette PR : livraison séparée attendue (arbitrage coordinateur sur réécriture scope OU implémentation énumération).

    Grain: DEEP/lean -- lane myia-po-2027:CoursIA-2 -- prev: MED/docs #16969

  4. jsboige
    added a commit that references this issue on Sep 21, 2026

    feat(lean,#16753): Tegmark R16 Annexe A — Boolean NAND + C₂/C₃ + stru…

    8b0166f

  5. jsboige commented on Sep 22, 2026

    @jsboige
    jsboige
    on Sep 22, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2023:CoursIA-2 -- tegmark_muh_lean Concern #2 (Decidable.lean decideEq stub + ClosedUnderComp vide) -- Concern #1 laissé en observation pour vérification orthogonale (Rel.table typing). Scope : MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/**/*.lean + MyIA.AI.Notebooks/SymbolicAI/Lean/tegmark_muh_lean/MUH/Decidable.lean -- 2026-09-22T17:30Z

    Reprise de la claim périmée po-2027 (49.5h > 48h stale threshold, vérifié via scripts/check_lane_claim.py --lane myia-po-2023:CoursIA-2 16958). Aucune PR ouverte couvrant ce grain (gh pr list --search "tegmark_muh_lean OR 16753" ne renvoie aucun PR CoursIA en OPEN). Le claim po-2027-AMEND portait sur Concern #1 uniquement ; je l'élargis à #2 et garde #1 en observation.

  6. jsboige commented on Sep 22, 2026

    @jsboige
    jsboige
    on Sep 22, 2026
    OwnerAuthor

    [INFO] po-2023 c.802 — Concern #2 livré via PR #17431 (pas Concern #1)

    Vérif first-hand (Tell c.770 strict fondateur v2 ★★★★ leçon c.1374)

    Livraison

    PR #17431 (fix/16958-concern2-claim-code-align, head 8368e7dcc9) amender la doc pour aligner claim/code :

    • MUH.lean (FR) + MUH.lean.en (EN sibling pair) : « preuve Sheffer ↔ 4 gen » → « exemples canoniques ; équivalence hors-scope, voir lean(#16753): suivi Concerns #1+#2 Hermes sur tegmark_muh_lean (PR #16942) #16958 ». « algorithme énumératif haltant » → « squelette énumératif documenté ; code livré est un stub ».
    • MUH/Boolean.lean : retire « vérifie que les deux encodages sont équivalents » ; ajoute « ne prouve pas l'équivalence ; hors-scope ».
    • MUH/Decidable.lean : marque explicitement ClosedUnderComp, boolBinaryTableCount, decideEq comme « Stub. » en tête de docstring.

    Doc-only (+37 / −23, 4 fichiers, aucun code modifié). Sibling pair i18n #4980 respecté. Concern #1 laissé en observation (déjà réglé sur main).

    Closes #16958.

    Tell c.625 ★★★★ dissipation ×1 c.802 : Concern #2 dissipé first-hand.

    🤖 Generated with Claude Code

  7. myia-ai-01
    added a commit that references this issue on Sep 23, 2026

    fix(lean,#16958): align MUH/Boolean/Decidable docstrings to scope rée…

    48e8b0b
  8. myia-ai-01
    closed this as completedin #17431on Sep 23, 2026
  9. myia-ai-01
    added a commit that references this issue on Oct 5, 2026

    feat(lean,#16753): ClosedUnderCompSet + Fin.pi helper + generation mu…

    71514d5
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions