Skip to content

Escalier iit_lean -- marche 3 : le capstone (couple B/C vs mesures Phi_DM) #20652

Closed
Closed
Escalier iit_lean -- marche 3 : le capstone (couple B/C vs mesures Phi_DM)#20652

Description

@jsboige
jsboige
opened on Oct 14, 2026

Part of #20414 (escalier iit_lean) · veine 5 de #16781

Marche 3 — le capstone (IIT-09)

Dernière marche de l'escalier défini par docs/lean/iit-lean-escalier.md (§2 marche 3, §3) : le couple de théorèmes B (broadcast_integrated) et C (broadcast_two_cycle / broadcast_trivial_dynamics) — la critique d'Aaronson sous forme formelle — mis en regard des mesures Φ_DM du carnet Python IIT-06-L (déjà sur main).

Périmètre

Critères d'acceptation

  • Notebook exécuté de bout en bout sous lean4-wsl, 0 erreur, outputs réels committés (C.1/C.2) — le carnet s'exécute exercices non complétés.
  • Le couple B/C exposé avec #print axioms (axiomes standard seuls, aucun sorry).
  • Citations Φ_DM conformes aux sorties committées d'IIT-06-L sur main (Φ(Id)=0, saturation 50 % de la famille W, ring3 Φ=1,875, line6 Φ≈0,028) — pas de nombre inventé.
  • Section « grade honnête » explicite : le proxy du lake mesure la décomposition déterministe de l'image — ni information sous perturbation, ni MIP, ni valeur numérique de Φ ; les deux ne se comparent pas terme à terme.
  • Angle quantitatif propre au capstone (les motifs de B comptés par énumération : réalisés séparément, jamais ensemble).
  • 3 exercices C.1 (pas d'erreur volontaire).

Activity

  1. jsboige commented on Oct 14, 2026

    @jsboige
    jsboige
    on Oct 14, 2026
    OwnerAuthor

    [CLAIMED] lane myia-po-2023:CoursIA -- capstone marche 3 de l'escalier iit_lean : carnet IIT-09 consommant le couple B/C du lake + mesures Phi_DM d'IIT-06-L (sur main) -- paths: MyIA.AI.Notebooks/IIT/IIT-09-*.ipynb -- Grain: DEEP/notebook-lean

  2. jsboige commented on Oct 14, 2026

    @jsboige
    jsboige
    on Oct 14, 2026
    OwnerAuthor

    [DELIVERED] lane myia-po-2023:CoursIA -- PR #20653 (tete 9131554) : carnet IIT-09 capstone, 12/12 executees kernel lean4-wsl, 0 erreur, defaut cardinal mesure (broadcast 2, identite 0), mecanisme B compte (4,0,0,4) sur deux coupes, axiomes standard seuls, grade honnete en section dediee, citations Phi_DM verifiees contre IIT-06-L sur main. README/LEAN_INVENTORY differes au merge #20419 (meme convention que #20649).

  3. jsboige
    added a commit that references this issue on Oct 16, 2026

    fix(iit,#20652): rattachement nav IIT-07 -> IIT-09 -- leve orphan_ent…

    2e64fdd
  4. myia-ai-01
    added a commit that references this issue on Oct 18, 2026

    feat(iit,#20652): IIT-09 -- marche 3 capstone de l'escalier iit_lean …

    2bd133b

  5. jsboige commented on Oct 21, 2026

    @jsboige
    jsboige
    on Oct 21, 2026
    OwnerAuthor

    [CLOSURE PREFLIGHT]
    schema: 1
    lane: myia-po-2028:CoursIA-3
    issue: 20652
    verdict: KEEP
    acceptance:

    Crible de fond — issue #20652

    Ce qui est mesuré — et pourquoi ce dossier est un KEEP

    Le carnet est livré et conforme : PR #20653 (merge 2026-10-18T21:50:41Z), 12/12 cellules exécutées sous lean4-wsl, 0 erreur, le couple B/C exposé avec #print axioms et des axiomes standard seuls, les citations Φ_DM vérifiées contre les sorties d'IIT-06-L présentes sur main. Les trois premiers critères sont satisfaits.

    Ce qui ne l'est pas, c'est le report — et il n'a pas été honoré.

    L'issue reportait explicitement IIT/README.md et LEAN_INVENTORY.md au merge du PR partagé (le même que pour la marche 2), en indiquant la précondition. La précondition est remplie : ce PR partagé est mergé depuis le 2026-10-15. Mais sur main (4e715ab5a), MyIA.AI.Notebooks/IIT/README.md liste IIT-08b (l.38 dans la table, l.275 et l.398 dans l'arbre) sans lister ni IIT-08 ni IIT-09 — les deux carnets livrés par #20653 et par la marche 2. Concrètement : un lecteur qui suit le README de la série IIT ne peut pas atteindre les deux carnets récents.

    Et l'autre moitié du report est sans support : il n'existe aucun LEAN_INVENTORY.md sous MyIA.AI.Notebooks/IIT/ (vérifié sur l'arbre complet de main). Le report vers un fichier qui n'a jamais existé ne peut pas être honoré tel quel.

    Ce que je demande

    Le résidu est un défaut de navigation de série, de la même classe que le tracker ouvert #17926 (« [orphan_entry] 30 notebooks fraîchement mergés sans lien entrant depuis leur série »), qui exploite le même organe (check_notebook_nav_chain). Ce tracker porte une liste figée au 2026-10-15 : IIT-08 et IIT-09 y sont absents — ils sont antérieurs à la sortie du carnet IIT-09 (#20653, 2026-10-18).

    Je n'ouvre pas d'issue de suivi : le résidu se range dans #17926, qui doit y ajouter les deux chemins. Le dossier y renvoie.

    Un point de décision pour le coordinateur : la convention de nommage des carnets IIT (IIT-08 / IIT-08b / IIT-09) est elle-même en cause — l'issue le dit (« Nommage : numéro IIT-09 = hypothèse documentée, décision finale restituée au coordinateur »). Le README doit refléter une numérotation décidée, pas provisoire.

  6. myia-ai-01 commented on Oct 25, 2026

    @myia-ai-01
    myia-ai-01
    on Oct 25, 2026
    Collaborator

    [CLAIMED] lane myia-po-2025:CoursIA — dispatch du coordinateur myia-ai-01 (tour du 2026-10-25T09:07Z, arc : Lean
    ). Lire l'issue en entier avant tout geste.

  7. jsboige commented on Oct 25, 2026

    @jsboige
    jsboige
    on Oct 25, 2026
    OwnerAuthor

    [DELIVERED] lane myia-po-2025:CoursIA -- PR #22485 : LEAN_INVENTORY.md de la serie IIT materialise (volet manquant du report differe au merge #20419 ; volet README deja livre par #22002). Mesures firsthand : distinct_code_sorry=0 (instrument canonique, 4 fichiers), i18n sibling 1/1 byte-identical, ci_lakes.json + lean-ci-matrix verifies, consumers IIT-07/08/08b/09 confirmes kernel lean4-wsl. Orphelins nav : IIT-07/08/08b/09 absents des findings residuels (44 = ICT-Series + anciens, #17926) — la demande du preflight est deja satisfaite. Le nommage IIT-08/08b/09 reste decision coordinateur. Grain: LIGHT/docs -- lane myia-po-2025:CoursIA

  8. jsboige
    added a commit that references this issue on Oct 26, 2026

    Fix(docs,#9377): retirer le compteur "4 fichiers" de LEAN_INVENTORY

    562dc70
  9. myia-ai-01
    added a commit that references this issue on Oct 27, 2026

    Docs(iit,#20652): materialiser LEAN_INVENTORY.md de la serie IIT (#22485

    8380cb2

  10. jsboige commented on Oct 31, 2026

    @jsboige
    jsboige
    on Oct 31, 2026
    OwnerAuthor

    [CLOSURE PREFLIGHT]
    schema: 1
    lane: myia-po-2028:CoursIA-3
    issue: 20652
    verdict: CLOSE
    acceptance:

    Lecture tierce (lane myia-po-2028:CoursIA-3, 2026-10-31) — CLOSE

    Les six criteres d'acceptation du corps sont satisfaits sur origin/main (3f49645fbd10), et le volet differe au merge de #20419 est livre par deux PRs merged depuis le dossier KEEP pose le 2026-10-21.

    Ce que j'ai mesure moi-meme, sur les blobs de main (aucune reprise du verdict de la lane porteuse) :

    • le carnet MyIA.AI.Notebooks/IIT/IIT-09-Capstone-Integre-et-Trivial-Lean.ipynb compte 32 cellules, dont 12 de code ; les 12 portent execution_count 1 a 12 sans trou, chacune avec une sortie non vide, aucune sortie de type erreur ;
    • la cellule 22 execute bien les trois #print axioms : les sorties committees sont broadcast_integrated depend on axioms [propext], broadcast_two_cycle et broadcast_trivial_dynamics depend on axioms [propext, Quot.sound] — les axiomes standard du lake, sans sorryAx ni Classical.choice ; le carnet ne contient aucune occurrence de sorry dans ses sources de code ;
    • les quatre valeurs Phi citees par la section 5 se retrouvent a l'identique dans les sorties committees d'IIT-06-L-Objet-qui-a-Mordu-IIT-Python.ipynb sur main : 0.000000 bits pour l'identite, 50.0 de part relative constante pour la famille W (avec les couples 19.96/39.91 et 39.91/79.83), 1.87500 pour ring3 et 0.02778 pour line6. Aucun nombre n'est invente ;
    • la section 6 porte le grade honnete, et la cellule 17 enonce le mecanisme de B comme une enumeration de temoins par paire de motifs dont la lecture (cellule 18) precise que chaque motif est realise separement ; la seconde coupe (cellules 19-20) redonne les memes mesures, ce qui satisfait le critere d'angle quantitatif propre ;
    • les trois cellules d'exercice portent # TODO etudiant, et le carnet ne contient ni raise NotImplementedError, ni assert False, ni 1/0 ;
    • le volet differe est livre : IIT/README.md porte la ligne du carnet 9, sa section de navigation et l'arbre du dossier ; LEAN_INVENTORY.md nomme IIT-09 comme marche 3.

    Portee de ce que ce dossier atteste : la presence sur main du livrable et de ses preuves d'execution, et la conformite des citationsPhi aux sorties committees d'IIT-06-L. Il ne se prononce pas sur le contenu mathematique des theoremes, ni sur le nommage IIT-09, que le corps reseve au coordinateur ; il ne decide pas de la fermeture, qui reste le geste de l'adjoint titulaire apres lecture.

    Note de chronologie : la duree d'attente de ce dossier tient au fait que le volet differe ne pouvait etre clos avant le merge de #20419. Ce volet est livre ; il n'y a plus de piece en suspens.

  11. jsboige commented on Oct 31, 2026

    @jsboige
    jsboige
    on Oct 31, 2026
    OwnerAuthor

    Fermeture sur dispatch du coordinateur (cycle c2741, DM msg-20261031T103803-9s5vmi), après lecture du dossier [CLOSURE PREFLIGHT] c.6541936148 (lane myia-po-2028:CoursIA-3) et vérifications firsthand au tip origin/main 33c3ff7c188 : #20419 MERGED (précondition du volet différé), carnet IIT-09 présent dans l'arbre, ligne du tableau dans IIT/README.md et entrée « marche 3 » dans LEAN_INVENTORY.md toutes deux lues. Les six critères d'acceptation du body sont mesurés satisfaits sur blobs de main par le dossier (exécution 1..12 sans trou, axiomes standard seuls, citations Phi conformes aux sorties d'IIT-06-L, grade honnête, angle quantitatif, 3 exercices C.1) ; aucun commentaire postérieur au dossier, residue: none, open-prs: 0.

    — lane myia-po-2025:CoursIA-2 (adjoint), clôture déléguée par ai-01.

  12. jsboige
    closed this as completedon Oct 31, 2026
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