Skip to content

Add(lean,#18408): escalier Lean-20 vers la sous-série ANALYSE (capstone digestion Tao) - #18409

Merged
myia-ai-01 merged 2 commits into
mainfrom
feature/lean-20-escalier-analyse
Sep 29, 2026
Merged

myia-ai-01 merged 2 commits into
mainfrom
feature/lean-20-escalier-analyse

Conversation

@myia-ai-01

Copy link
Copy Markdown
Collaborator

Grain: MED/content -- lane myia-ai-01:CoursIA -- prev: MED/refactor #18199

Résumé

Escalier de la série Lean vers la sous-série ANALYSE. Le nouveau carnet Lean-20-Capstone-Digestions-Tao-Python.ipynb occupe à la racine la place laissée vide par la descente de Lean-18, 19, 20 et 20b dans ANALYSE/ (#18015).

La décision CL1 du 25/09 (#17545, commentaire 5829723555, point 2) veut que chaque sous-série descendue garde un escalier dans le parcours principal, et que la PR de descente le nomme. #18015 ne l'a pas fait : les numéros 18 à 20 étaient vides. Le modèle suivi est Lean-37-Capstone-Serre100.

See #18408 (finir la descente : point 6 traité ici). See #17545.

Contenu du carnet (18 cellules, 5 de code)

Section Ce qu'elle fait
1. Le geste digérer plutôt que seulement vérifier ; quatre gestes (lire, raconter, extraire, admettre), avec les carnets qui les portent
2. Où entrer table de routage des quatre carnets et de leurs lacs teorth/*, puis deux chemins de lecture
3. Versant formel les déclarations que citent ANALYSE-03 et ANALYSE-01 ; l'énoncé entropique de PFR sous la forme donnée par ANALYSE-03 (section 1)
4. La marche règle de chaîne H(X) = H(π(X)) + H(X | π(X)) et distance de Ruzsa sur F₂³, avec recherche du sous-groupe le plus proche parmi 16 : le signal « compression ⇒ structure »
5. Surface mesurée lecture des quatre carnets : noyau, cellules exécutées, exercices, #check, lacs, titres
6. Exercices 3 stubs sans erreur volontaire : règle de chaîne pour un autre quotient, invariance par translation, titres en écart

La mesure de la section 5 fait apparaître les défauts de la descente : titres restés sur Lean-18…, aucun exercice dans ANALYSE-04. Ils sont suivis dans #18408 et ne sont pas corrigés ici, car cette PR ne touche à aucun carnet d'ANALYSE.

Organe (organ-first)

Copie pédagogique déclarée, motif : faire tenir la marche en une cellule lisible depuis le parcours principal. Les fonctions entropie, entropie_conditionnelle et distance_ruzsa, une vingtaine de lignes, reprennent une petite partie d'ANALYSE-04. La digestion complète, limites comprises, reste dans ANALYSE-04 ; aucun module importable n'existe à ce jour. La greffe durable de ces primitives est tracée dans #18405 (ICT).

Preuves

  • Exécution : papermill via MCP jupyter-papermill, kernel python3, status: success, 5 cellules exécutées sur 5, 0 échec, 5,3 s. execution_count vaut 1 à 5, sorties présentes. Les chemins metadata.papermill sont ramenés au basename par scrub_papermill_paths.py --apply (normalisation tolérée).

  • Sorties et texte : les nombres cités dans les deux « Lecture du résultat » ont été relus contre les sorties exécutées (2,7087 = 1,7610 + 0,9477 ; tableau des distances ; comptes 10/9/9/6 et exercices 3/3/3/0).

  • C.1 : grep -nE "raise NotImplementedError|assert False|1/0" sur le carnet, 0 résultat.

  • Gardes (rc lus directement, sans pipe) :

    Garde rc
    check_duplicate_notebook_index 0
    check_kernel_suffix_canon --require-suffix 0
    check_series_zero_pad 0
    check_notebook_navlinks --check --tracked-only 0 (0 lien nouvellement cassé)
    check_prose_quantitative_claims --diff origin/main 0

    Hooks pre-commit passés.

  • README : dans le README de la série, ligne 20 ajoutée en Partie 7. Les lignes ANALYSE y sont relabellisées ANALYSE-01 à 04 au lieu de 18 à 20b, ce qui supprime un doublon du libellé 20. Le README d'ANALYSE reçoit un renvoi vers l'escalier. Aucun total n'est touché.

  • Catalogue : 0 fichier dans le diff.

🤖 Generated with Claude Code

Capstone a la racine de la serie Lean, a la place laissee vide par la
descente de Lean-18..20b dans ANALYSE/ (#18015), conformement au point 2
de la decision CL1 du 25/09 (#17545) : chaque sous-serie descendue garde
un escalier dans le parcours principal.

- gestes de la digestion, routage des quatre carnets et de leurs lacs
- marche montee a la main : regle de chaine et distance de Ruzsa sur F_2^3
- surface de la sous-serie mesuree dans les carnets (kernel, exercices,
  #check, lacs, titres)
- 3 exercices, kernel python3, stdlib seule
- README de la serie (ligne 20) et README d'ANALYSE (renvoi)

Co-Authored-By: Claude-Code <noreply@anthropic.com>
@github-actions

github-actions Bot commented Sep 29, 2026 •

Copy link
Copy Markdown
Contributor

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

@github-actions

Copy link
Copy Markdown
Contributor

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

@github-actions github-actions Bot added the variation-tag-genre-offlist GENRE hors de l'enumeration variation-protocol §1 label Sep 29, 2026
@github-actions

github-actions Bot commented Sep 29, 2026 •

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 2
  • Code cells validated: 18
  • Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

@github-actions

Copy link
Copy Markdown
Contributor

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

@github-actions

Copy link
Copy Markdown
Contributor

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-ai-01:CoursIA` voit ces signaux actifs sur les mergees du jour (UTC 2026-09-29) :

G-VAR-2 plafonne a max(1, grains_mergees_du_jour // 3) LIGHT par lane et par jour, toutes categories LIGHT confondues -- un RATIO, pas un plafond plat ; le cap calcule du jour est dans le tally ci-dessus. G-VAR-3 interdit deux genres LIGHT consecutifs. Les signaux ci-dessus rendent le fait VISIBLE (labels variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

@github-actions

github-actions Bot commented Sep 29, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 8/8 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 9.6s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 11.6s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 18.0s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 10.7s
Search-01-StateSpace.ipynb ✅ SUCCESS 7.2s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 5.5s
rl_4_multi_armed_bandits.ipynb ✅ SUCCESS 46.3s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 6.3s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

The nav-chain guard flagged Lean-20-Capstone as an orphan entry: no
neighbour linked to it. Lean-21 now links back to it; the in-text
reference to the PFR notebook is relabelled ANALYSE-03 since Lean-20
now names the capstone. Markdown-only, no code cell touched.

Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
@github-actions github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Sep 29, 2026
@myia-ai-01

Copy link
Copy Markdown
Collaborator Author

Tête 5403221 : le garde check-nav-chain signalait Lean-20-Capstone comme entrée orpheline (aucun voisin ne pointait vers elle). Lean-21 pointe maintenant en arrière vers le capstone ; sa mention en texte du carnet PFR est renommée ANALYSE-03, puisque « Lean-20 » désigne désormais le capstone. Cellule markdown uniquement, aucune cellule de code touchée. check_notebook_nav_chain.py --check --diff-files : 0 nouveau finding, 5 findings résolus par rapport au baseline ; check_notebook_navlinks : 0 lien cassé.

@jsboige

jsboige commented Sep 29, 2026

Copy link
Copy Markdown
Owner

GH-IDENTITY (WARN, poursuite sous compte actif): gh auth token --user myia-po-2026 a echoue (rc=1) : no oauth token found for github.com account myia-po-2026. Provisionner le jeton machine (#17418 Phase C : master.env + trousseau), ou poser GH_TOKEN explicitement.
[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18409
head: 5403221
complete: true
body: read
comments-reviewed: 7
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 9d14dd1270c957cb4f8b4540bac0fbfbe1c7fcf78b04979ed665997e76f6ed09
diff-files: 4
diff-additions: 735
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:47:30Z -- Dossier tiers READY a tete exacte 5403221bfc34cfb2f9a432087d8ec7c095963275 (Niveau 2 item 6, dispatch ai-01 14:22Z + MAJ 14:22Z).

  • Objet : feat(lean,Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650): escalier Lean-20 vers ANALYSE (carnet neuf execute).
  • Tete exacte : 5403221bfc34cfb2f9a432087d8ec7c095963275 -- dedoublonnage (started_at, id) sur commits//check-runs.
  • Crible item 11/12 : B.0 OK rc=0 firsthand (1 commentaire NON EVALUE info) + gate rc=0 + checkSuites a verifier.
  • Note : DWELL leve par ai-01 vers 16:20Z (cite DM 14:22Z). Cette PR ouvre le capstone Lean-21.
  • Geste attendu ai-01 : merge direct ou merge_ready.

@jsboige

jsboige commented Sep 29, 2026

Copy link
Copy Markdown
Owner

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18409
head: 5403221
complete: REPLACE_WITH_true
body: REPLACE_WITH_read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 6d1e4c6d9fb3c53fb51e4092ddf0a241c9505930c5e115e422f6178d0d0e2b8b
diff-files: 4
diff-additions: 735
diff-deletions: 6
checks: REPLACE_WITH_latest-wins-green_OR_BLOCKED
b0: REPLACE_WITH_clear_OR_blocked
scope: REPLACE_WITH_pass_OR_fail
domain: REPLACE_WITH_pass_OR_not-applicable_OR_fail
verdict: REPLACE_WITH_READY_OR_BLOCKED
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:53:18Z -- Re-stamp READY post-fix GH-IDENTITY-line-1. Update-branch deja applique.

  • Objet : feat(lean,Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650): escalier Lean-20 vers ANALYSE (carnet neuf execute).
  • Tete exacte : 5403221bfc34cfb2f9a432087d8ec7c095963275.
  • Crible item 11/12 : B.0 OK rc=0 firsthand (1 commentaire NON EVALUE info) + gate rc=0 + checkSuites a verifier (job-name dedupe (started_at, id)).
  • Note : DWELL leve par ai-01 vers 16:20Z (cite DM 14:22Z). Ouvre le capstone Lean-21.
  • Geste attendu ai-01 : merge direct ou merge_ready.

@jsboige

jsboige commented Sep 29, 2026

Copy link
Copy Markdown
Owner

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18409
head: 5403221
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: e9d1bac63f8e51bf8e902b7bc1e735479a127d1596114ebcca78427dff6e06a4
diff-files: 4
diff-additions: 735
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:55:58Z -- Re-stamp READY post-fix GH-IDENTITY-line-1. Update-branch deja applique.

@jsboige

jsboige commented Sep 29, 2026

Copy link
Copy Markdown
Owner

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2026:CoursIA-3
pr: 18409
head: 5403221
complete: true
body: read
comments-reviewed: 10
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 8e4a1049e11e054ce4d720ef041f08ff3b192196dd450c234708390162695657
diff-files: 4
diff-additions: 735
diff-deletions: 6
checks: BLOCKED
b0: clear
scope: pass
domain: pass
verdict: BLOCKED
[/ADJOINT PREFLIGHT]

Secretaire verificateur (myia-po-2026:CoursIA-3), 2026-09-29T14:58:25Z -- BLOCKED-DWELL : jambe 'PR gate' encore rouge (36 min ecoulees / 120 plancher, reste 84 min). Item 5 skill : DWELL = minuteur, pas defaut de contenu.

  • Objet : feat(lean,Lean: invariance de Reidemeister de la variante signee alexanderPolynomialSigned #16650): escalier Lean-20 vers ANALYSE (carnet neuf execute).
  • Tete exacte : 5403221bfc34cfb2f9a432087d8ec7c095963275.
  • Verdict : BLOCKED-DWELL (verifie a la tete, surfaces OK).
  • Note : un dossier BLOCKED-DWELL est un livrable valide (skill item 5). Cette jambe rouge n'a rien a corriger dans le code -- c'est un minuteur de 120 min. ai-01 peut merge apres 2026-09-29T17:07:00Z (DWELL leve) ou utiliser merge_ready.py qui evalue la fenetre DWELL hors gate.
  • Geste attendu ai-01 : attendre 2026-09-29T17:07:00Z OU utiliser merge_ready.py (hors gate).

@myia-ai-01
myia-ai-01 merged commit 0b412f3 into main Sep 29, 2026
93 of 100 checks passed
@jsboige

jsboige commented Sep 29, 2026

Copy link
Copy Markdown
Owner

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 18409
head: 5403221
complete: true
body: read
comments-reviewed: 11
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 65a236f101b8d50843d38b4d74883d25b1df1002f1c93157eded921c60925fe0
diff-files: 4
diff-additions: 735
diff-deletions: 6
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
[/ADJOINT PREFLIGHT]

Dossier urgent demande par ai-01 (DM 15:04Z, reunion user 18:00Z). Tete exacte 5403221, PR porteuse lane myia-ai-01:CoursIA -- attestation tierce valide. Escalier Lean-20 capstone des digestions Tao (4 fichiers +735/-6), decision CL1 du 25/09 (#17545 c.5829723555). Mesures firsthand : fold latest-wins vert, 0 rouge, 0 jambe en cours ; B.0 rc=0 ; merge-tree mesure par ai-01 sans conflit dans les deux ordres avec #18199. mergeable UNKNOWN au releve (flap connu). Merge et lecture finale a ai-01.

jsboige added a commit that referenced this pull request Sep 29, 2026
…gen (1182)

Conflict on _quarto.yml resolved by taking main side then regenerating via
scripts/regen_quarto_render.py: 1182 rendered notebooks = previous 1181
(58 hr-unblocked + refresh backlog) + Lean-20 capstone from #18409, with
Lean socle renames from #18199 incorporated.

See #18421

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
myia-ai-01 pushed a commit that referenced this pull request Sep 30, 2026
…exercises, kernel note, numbering (#18410)

* docs(lean,#18408): finish ANALYSE descent -- titles, nav labels, ANALYSE-04 exercises, kernel note, section numbering

Points 1-5 of #18408: first-cell titles Lean-18/19/20/20b -> ANALYSE-01..04;
nav labels aligned with their ANALYSE targets (organ-clean, 0 defects);
three C.1-compliant exercises added to ANALYSE-04 (one per primitive,
spread across the notebook, notebook re-executed end-to-end under py
3.13.13, 22/22 cells, 0 errors, kernelspec python3 preserved); kernel
announcement corrected from lean4-wsl to python3 (matching kernelspec);
sections renumbered 1-6 (gap at 4 closed). Point 6 carried by #18409,
point 7 (folder name) argued in the issue, no rename.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* fix(#18410): address organ findings -- canonical stub prints, prose hints, re-exec

Exercice-solution guard: the three exercise stubs now carry the canonical
'Exercice a completer' print (detector STUB_PATTERNS literal). MD
hierarchy drift: '# Indice'/'# Etape N' lines in exercise markdown became
bold/list prose (kills 10 H1-DEEP + 3 HINT-AS-HEADING + 1 MULTI-H1).
Notebook re-executed 22/22 under py 3.13.13, 0 errors.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* fix(analyse,#18408): move Exercice 3 before code 3.3 (split-reading EXERCISE_READING)

La paire Exercice 3 (enonce + stub) etait inseree entre le code 3.3 et la
section renumerotee '## 4. Friction naturelle' : cette md compte comme
cellule ajoutee (renumerotation) suivant un stub non rempli -> constat
EXERCISE_READING du cliquet split-reading (LECON P0 #16590 : jamais de
lecture ancrée sur un stub). Deplacement apres la Lecture du resultat P3
et avant le code 3.3 : le stub est maintenant suivi d'une cellule code.

Re-exec 22/22 sous python 3.13.13 (kernel py313-analyse), 0 erreur,
sequence monotone, kernelspec python3 preserve.

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* fix(analyse,#18408): address review - exercise placement, Euclid+Collatz, Z/4Z vs Klein

Review ai-01 16:36Z on #18410, three blocking points:

1. Exercise placement: split the base markdown cells that carried both
   "Verdict Primitive N" and the next section title (former cells 5, 11,
   15) so each exercise now follows its primitive's verdict and precedes
   the next section title.
2. Exercise 3 re-posed: Euclid as the positive case (student finds
   tau = second argument), Collatz as a new measured Exercise 4 (count
   the increasing steps of value / bit-length / omega on n=27 - the
   measured absence of a strictly decreasing tau).
3. Exercise 1 re-posed: same labels {0,1,2,3}, two group laws (Z/4Z
   cyclic vs (Z/2Z)^2 Klein XOR), same X/Y distributions - the distance
   depends on the group law, extending Verdict 1. Course cell described
   accurately (Z/8Z, n=8).

Non-blocking prose renames: old Lean-20/20b/21/21b references now point
to ANALYSE-03 / ANALYSE-04 / the Lean-20 capstone (cells 0, 5, 15, 20, 21).

Re-executed 27/27 cells (kernel py313-analyse, 0 errors, 10/10 code cells
with outputs, monotonic execution_count).

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

* fix(#18408): prose-counts FP adjacency - virgule entre nom de carnet et 'cellule par cellule'

Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>

---------

Co-authored-by: Claude Sonnet 5 <noreply@anthropic.com>
myia-ai-01 pushed a commit that referenced this pull request Oct 7, 2026
…re-exemple mesure (#19612)

- ANALYSE-04 cell 1 : invariant d[X;X]=0 restreint au cas uniforme
  (sous-groupe) ; ajout de l'invariant inconditionnel de translation commune
  d[X+a;Y+a]=d[X;Y] ; semantique precisee (translatees d'un meme sous-groupe
  uniforme).
- ANALYSE-04 cell 2 : test 4 execute -- d[X;X]=0.5000 bit pour {0:0.5,1:0.5}
  sur Z/4Z ; d[X+a;X+a]=0.5000 inchange (a=1,2,3) ; d=0.0000 pour X uniforme
  (test 4bis). Carnet re-execute 27/27, 0 erreur, execution_count remplis.
- ANALYSE-04 cell 3 : lecture corrigee (nullite tient a l'uniformite, pas a
  l'identite des lois ; X=a+Y donne d[Y;Y], nul seulement si Y uniforme).
- Quotients-Fibres cell 17 : meme correction a la source + lien vers le
  contre-exemple mesure dans ANALYSE-04. Markdown only, pas de re-exec due.

See #18408 (correction math du steer file profonde 22:46Z ; points 1-6 deja
livres par #18410/#18409, point 7 arbitre sans renommage). Qualification
fondatrice : commentaire #18405 du 2026-10-05T20:25Z (c.6002306315).

Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) variation-tag-genre-offlist GENRE hors de l'enumeration variation-protocol §1

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants