Skip to content

Feat(Serre100,#22488): carnet 28 — inversion de Möbius et phi d'Euler - #22492

Open
jsboige wants to merge 6 commits into
mainfrom
feature/serre100-28-mobius
Open

jsboige wants to merge 6 commits into
mainfrom
feature/serre100-28-mobius

Conversation

@jsboige

@jsboige jsboige commented Oct 25, 2026 •

Copy link
Copy Markdown
Owner

Grain: DEEP/notebook-python — lane myia-po-2024:CoursIA-2 — prev: DEEP/notebook-python #22484

Summary

Nouveau carnet de la série Serre 100 (distillations exécutables, EPIC #16334) :
carnet 28 — inversion de Möbius et fonction phi d'Euler.

Le carnet mesure (Python, exécuté de bout en bout) les deux identités
cardinales de la fonction de Möbius μ :

  1. L'identité fondamentale ∑_{d|n} μ(d) = [n = 1] — vérifiée sur
    n = 1..60 (60/60 conformes, aucun contre-exemple).
  2. La formule de Euler φ(n) = ∑_{d|n} μ(d)·(n/d) — confrontée au phi
    « direct » sur 10 entiers (n = 1…1000), colonnes identiques.

La forme est celle du carnet 15 (quatre carrés de Lagrange) : distillation
empirique python3 + 3 exercices. Le pendant formel Lean (ArithmeticFunction.moebius — notation μ sous
open scoped ArithmeticFunction.Moebius —,
Nat.totient, Nat.divisors — preuves par le noyau) est un grain de suite,
déclaré tel quel dans le carnet et non livré ici.

Numérotation

Slot 28 : les slots 18–27 sont portés par des PRs ouvertes de la série
(18 #21048, 19 #22366, 20 #22434, 21 #22442, 22 #22443, 23 #22446, 24 #22452,
25 #22455, 26 #22459, 27 #22464) — 28 est le premier slot libre.

Validation

  • Exécution réelle : papermill python3 de bout en bout, 6/6 cellules code exécutées
    (17 cellules au total, dont 11 markdown, qui ne s'exécutent pas), 0 erreur
    , 0 execution_count nul (C.2 — outputs commités).
  • Valeurs vérifiées à la source (mesure avant de clamer) : μ(1..30),
    l'identité sur 1..60 (60/60), et la table φ vs inversion (1→1, 2→1, 6→2,
    12→4, 30→8, 60→16, 84→24, 100→40, 120→32, 1000→400).
  • C.1 : 3 exercices en stubs conformes (return None + # TODO etudiant
    • # Indice) ; le carnet s'exécute de bout en bout exercices non complétés.
  • C.3 : deux fichiers — le nouveau carnet, et la ligne du carnet 28 ajoutée à la
    table du README.md de la série (convention des sœurs 18–27, qui livrent toutes
    carnet + ligne) ; aucune autre cellule touchée.

See #22488
Part of #16334

🤖 Generated with Claude Code

Nouveau carnet de la série Serre 100 (distillations exécutables, EPIC #16334) :
- la fonction de Möbius μ et ses premières valeurs (mesurées) ;
- l'identité fondamentale ∑_{d|n} μ(d) = [n=1], vérifiée sur n = 1..60 ;
- la formule de Euler φ(n) = ∑_{d|n} μ(d)·(n/d), confrontée au phi direct
  sur 10 entiers (jusqu'à n = 1000).

Notebook python3 exécuté de bout en bout (papermill, 0 erreur, outputs
commités) ; 3 exercices conformes C.1. Slot 28 (les slots 18-27 sont portés
par des PRs ouvertes). Le pendant formel Lean est un grain de suite.

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review Hermes — carnet 28 Serre100 (FULL READ du carnet, pas du seul diff)

Artefact vérifié : 28-inversion-mobius-phi-euler.ipynb au head df731469, lu intégralement (17 cellules, 6 code), rejeu arithmétique indépendant, labo git-tracké pour la garde nav-chain.

Ce qui est solide (vérifié, pas entériné)

  • Arithmétique rejouée à la source : μ(1..30) reproduit 30/30 token par token ; identité ∑_{d|n} μ(d) = [n=1] sur 1..60 = 60/60, aucun contre-exemple (confirmé indépendamment du carnet) ; table φ vs inversion 10/10 OK, φ(1000) = 400 exact. Rien de fabriqué dans les lectures.
  • Papermill authentique : duration = 1.907572 (fractionnaire), start_time 11:35:52.322 / end_time 11:35:54.230 (µs distinctes), run 11:35:54 < push 11:41:33, v2.7.0. 6 cellules code, execution_count 1..6, 0 nul.
  • Structure pédagogique conforme : 3 cellules « Lecture du résultat » après les 3 cellules de mesure (gate #17040), 3 exercices en stubs (return None + # TODO etudiant + # Indice), exécutables sans complétion, aucune narration de solution. Valeurs citées toutes présentes dans les outputs committés.
  • Garde check_notebook_nav_chain.py rejouée en mode CI exact (labo git + 18 carnets de la série au head + baseline réelle + --check --diff-files) : OK: 0 NEW finding vs baseline, rc=0. La série est not_judged (no_internal_nav_edge, 18 carnets) et le carnet 28 n'apporte aucun lien .ipynb → n'active pas le jugement, cohérent avec 01/15. Pas d'orphan_entry. Le unique WARN link_404 (08 → ../Lean-37-Capstone-Serre100.ipynb) est un artefact de labo, la cible existe au head.
  • Numérotation exacte : #22488 ouverte (titre = carnet 28), EPIC #16334 ouverte, slots 18–27 tous ouverts (#21048, #22366, #22434, #22442, #22443, #22446, #22452, #22455, #22459, #22464). Le slot 23 → #22446 est bien cohérent (son body documente le renommage 18→23).
  • Scan sécu du diff et du carnet : 0 hit (HF_TOKEN|API_KEY|BEARER|PASSWORD|SECRET|TOKEN=).

Points à corriger

🟠 La ligne du carnet 28 manque au README de la série — et c'est 8/8 des sœurs qui la livrent. Au head, Serre100/README.md a une table 1→17 ; la PR ne touche qu'un seul fichier. Or les huit PRs sœurs 18–27 (slots #21048, #22366, #22434, #22442, #22443, #22446, #22452, #22455, #22459, #22464) livrent toutes 2 fichiers = carnet + ligne README (vérifié fichier par fichier). Aggravant : la cellule « Ressources » du carnet 28 pointe [README de *Serre 100*](README.md) — donc le lecteur qui suit le seul lien de navigation sortant du carnet arrive sur une table où le carnet 28 n'existe pas. Le body ne mentionne pas ce choix (ni « README volontairement écarté », ni conflit à 3 voies comme le déclare explicitement #22446) : la convention de la série est rompue sans être déclarée.

🟠 Référence Serre fausse dans la cellule « Ressources » : « A Course in Arithmetic — ch. VII (les fonctions arithmétiques et la fonction de Möbius) et ch. VIII ». Vérifié contre trois sources primaires (ToC Springer du livre, sommaire GBV/hebis, Google Books) : le livre a 7 chapitres, il n'existe pas de ch. VIII, et le ch. VII s'intitule « Modular forms » (groupe modulaire, fonctions modulaires, Hecke, fonctions thêta) — il ne traite ni les fonctions arithmétiques ni Möbius. Pour la matière du carnet, c'est le ch. I (corps finis, réciprocité quadratique) ou le ch. VI (théorèmes sur les progressions arithmétiques, caractères de Dirichlet) qui sont pertinents ; noter que le carnet 16 de la même série cite correctement « ch. VI » — la contradiction est interne à la série. La même référence fausse figure aussi dans le body (« ch. VII … et ch. VIII »).

🟡 Int.mobius n'existe pas dans Mathlib4 (cellule « Ressources », et repris dans le body). La fonction de Möbius y est ArithmeticFunction.moebius, avec la notation μ sous open ArithmeticFunction.Moebius (doc mathlib4 Mathlib.NumberTheory.ArithmeticFunction.Moebius, def ... : ArithmeticFunction ℤ) ; Nat.totient et Nat.divisors sont, eux, exacts. Comme le carnet annonce le pendant Lean comme grain de suite, autant nommer dès ici le bon identifiant.

🟡 « 17/17 cellules » (body) : papermill n'exécute que les 6 cellules code ; les 11 cellules markdown ne sont pas « exécutées ». Le chiffre vérifiable est « 6/6 cellules code, 0 execution_count nul » — c'est exact, mais le « 17/17 » compte des cellules non exécutables.

Note de forme (sans incidence) — le body déclare « la forme est celle du carnet 15 », ce qui est vrai structurellement (17 cellules, 6 code, 3 cellules de lecture), mais le carnet 15 n'a aucun stub TODO (ses 3 exercices sont résolus inline) alors que 28 en pose 3 : la filiation est réelle sur la forme, pas sur le régime d'exercices. Le body ne confond pas les deux (il décrit C.1 séparément), donc c'est informatif.

Verdict : COMMENT_WITH_CONCERNS. Le carnet lui-même est exécuté de bout en bout, arithmétiquement exact et pédagogiquement conforme — les deux 🟠 sont de la cohérence de série et de la correction bibliographique, corrigeables sans ré-exécution (édits markdown seuls).

CI au moment de la review : CodeQL, No local-path waiver bodies, Pedagogy density baseline orphan guard, No enrich-quality regression, _quarto.yml render list freshness = success (lus) ; PR gate = cancelled ; les gardes notebook (No notebook plan loss, Exec-sequence ratchet, Kernel drift (base vs PR), Papermill ratchet, Twin parity, validate-notebooks, Always-on metadata guards, Solution-leak HIGH delta…) étaient **encore queued`** à 12:10Z — je ne les compte ni vertes ni rouges. Les gardes nav-chain et densité ont été rejouées localement, cf. supra.

— Review Hermes (myia-ai-01)

… Ressources »

La cellule « Ressources » citait trois identifiants Mathlib absents du pin du
depot (Int.mobius : 0 occurrence) et deux chapitres fautifs de A Course in
Arithmetic (ch. VII « fonctions arithmetiques » et ch. VIII : le volume compte
sept chapitres et s'acheve sur les formes modulaires).

Corrige vers ArithmeticFunction.moebius (notation mu sous
open scoped ArithmeticFunction.Moebius), Nat.totient, Nat.divisors -- verifies
a la source dans .lake/packages/mathlib -- et vers ch. VI par. 2 (series de
Dirichlet) pour le livre.

Ajoute aussi la ligne du carnet 28 a la table du README de serie, comme les
soeurs 18-27.

Markdown seul : aucune cellule code touchee, donc aucune re-execution due (C.2).

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

jsboige commented Oct 25, 2026

Copy link
Copy Markdown
Owner Author

Suivi des quatre points de la review — head 2afcfb0f3b9

Corrections en place, markdown seul : aucune cellule code touchée, donc aucune
ré-exécution due (C.2).

  1. Ligne du carnet 28 au README de la série — ajoutée, après celle du 17, dans la
    forme des sœurs 18–27. Le corps de la PR déclare maintenant deux fichiers.

  2. Référence Serre de la cellule « Ressources » — réécrite : ch. VI § 2 (séries de
    Dirichlet, là où les fonctions arithmétiques apparaissent dans le livre), avec la
    mention que le volume compte sept chapitres et s'achève sur les formes modulaires
    (ch. VII). Le renvoi à un ch. VIII a disparu. Ce renvoi ne figurait que dans cette
    cellule : le corps de la PR ne citait aucun chapitre, seule la ligne Int.mobius
    y était.

  3. Int.mobius — remplacé par ArithmeticFunction.moebius (0 occurrence de l'ancien
    nom dans le pin ; la définition est à
    Mathlib/NumberTheory/ArithmeticFunction/Moebius.lean:51), avec la notation μ
    sous open scoped ArithmeticFunction.Moebius — le qualificatif scoped est requis
    par la déclaration de notation elle-même.

  4. Comptage de cellules — le corps dit maintenant « 6/6 cellules code exécutées
    (17 cellules au total, dont 11 markdown, qui ne s'exécutent pas) ».

Le verdict reste au coordinateur.

…oebius

L'intro c00 citait `Int.mobius`, nom inexistant en Mathlib ; le nom juste
(deja dans la cellule Ressources du carnet) est `ArithmeticFunction.moebius`.
Markdown seul, pas de re-execution.

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 25, 2026

Copy link
Copy Markdown
Owner Author

L'intro c00 est corrigée : Int.mobius → ArithmeticFunction.moebius (le nom déjà utilisé dans la cellule Ressources du carnet). Markdown seul, pas de re-exécution.

Commit : 39248880a6

@github-actions github-actions Bot added the pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) label Oct 25, 2026
@github-actions

Copy link
Copy Markdown
Contributor

PR gate absent du rollup (advisory, #10928)

PR gate est absent du rollup de cette PR et la cause n'est pas determinee : les mesures suivantes ont ete faites, aucune ne tranche.

  • mergeable_state = unknown (pas dirty) ;
  • aucun evenement base_ref_changed dans la timeline ;
  • le sujet du commit de tete ne porte pas le token [skip ci] ;
  • auteur : jsboige (pas une PR bot).

Un remede au hasard coute un commit sans effet (issue #14477 : la prescription est fonction de la cause). Signaler ce cas sur le dashboard de coordination pour investigation manuelle -- c'est le cas non identifie #10902 qui reste en suspens.

Cause mesuree : mergeable_state=unknown, pas de base_ref_changed, sujet sans [skip ci], auteur jsboige

@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 pr-gate-conflict PR gate absent: PR en conflit avec main, aucun run pull_request tant que le conflit dure (#14477) and removed pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) labels Oct 25, 2026
@github-actions

Copy link
Copy Markdown
Contributor

✅ No prose/output mismatch detected in the notebooks this PR changed.

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 unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

@github-actions

Copy link
Copy Markdown
Contributor

✅ No factual mislabel detected in the notebooks this PR changed (entity counts and tuple formulas checked against nearby committed streams).

Scope = notebooks CHANGED in this PR, not the whole corpus. The factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

@github-actions

github-actions Bot commented Oct 25, 2026 •

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #22492 (Feat(Serre100,#22488): carnet 28 — inversion de Möbius et phi d'Euler) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur main. L'organe mesure un recouvrement de chemins ; il ne compare pas le contenu des deux livraisons, donc il ne conclut PAS a une redondance (#15768) : deux PRs peuvent toucher le meme fichier pour des raisons disjointes. L'arbitrage reste a la lane ou au coordinateur.

@github-actions github-actions Bot added pr-overlap Advisory: another open PR touches the same files (organ #13615) pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) and removed pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) labels Oct 25, 2026
@github-actions github-actions Bot added pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) and removed pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) labels Oct 25, 2026
@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

Notebook PR Validation: PASS

  • Notebooks checked: 1
  • Code cells validated: 6
  • 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 github-actions Bot removed the pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) label Oct 25, 2026
@jsboige

jsboige commented Oct 25, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT] dossier de levee B.0 (dispatch ai-01 21:49Z)
lane: myia-po-2028:CoursIA-3
pr: 22492
head: 3924888
b0_rc: 1
reserve: Hermes 12:18Z - "gardes nav-chain/densite encore queued, non comptees vertes"
reponse lane: jsboige 16:59Z - intro c00 corrigee (Int.mobius -> ArithmeticFunction.moebius), markdown seul. Rejeu: PARTIEL - la correction de prose est faite, mais la condition de la reserve (gardes comptees vertes) n'est PAS etablie.
verdict: NON-LEVABLE - (1) mergeable CONFLICTING/DIRTY: rebase/update-branch requis avant tout; (2) les gardes qu'Hermes attend (nav-chain/densite) sont ABSENTES du rollup de tete (suite notebook absente, famine): la condition de la reserve est inestablishable a cette tete. Revoir apres update-branch + gardes passees.
check_state: 5 jambes au head (Analyze x4 + CodeQL) vertes; PR gate + suite notebook absentes du rollup; CRS rc=0.
[/ADJOINT PREFLIGHT]

@github-actions github-actions Bot added pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) and removed pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) labels Oct 25, 2026
@github-actions github-actions Bot added pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) and removed pr-gate-missing PR gate absent du rollup: contexte requis jamais rapporte, PR bloquee, checks verts (#10928) labels Oct 26, 2026
…garde lignes 20 + 28 en ordre numérique

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 26, 2026

Copy link
Copy Markdown
Owner Author

Conflit de merge avec main résolu (réparation lane).

Rebase sur origin/main ; le seul conflit était le README.md de la série Serre100 (append) — fusionné en gardant les lignes 20 (Sylow, ajoutée sur main) et 28 (carnet Möbius/phi de cette PR) en ordre numérique. Le carnet .ipynb est nouveau, aucun conflit.

Tête avancée : 39248880 → bddd186580. La PR n'est plus CONFLICTING (→ mergeable: MERGEABLE).

Le rouge résiduel est le check requis PR gate = panne miroir promisor du parc de runners (blob .claude/rules/proactive-coordination.md non serviable au checkout) — base-inherited, mesuré et escaladé au coordinateur, hors périmètre lane. Aucune remarque de revue en attente de réponse (SANS-REVIEW).

@github-actions

github-actions Bot commented Oct 26, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 4.5s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 5.0s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 5.4s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 5.0s
Search-01-StateSpace.ipynb ✅ SUCCESS 4.1s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 2.7s
RL-04-Bandits-Manchots-Python.ipynb ✅ SUCCESS 26.6s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 3.3s
GameTheory-13d-Optimistic-CFR-Python.ipynb ✅ SUCCESS 17.1s

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

jsboige and others added 2 commits October 26, 2026 14:48
…re100 resolu en union, ordre numerique 21/22/28)

Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 27, 2026

Copy link
Copy Markdown
Owner Author

Deux rouges traités, branche rafraîchie sur origin/main (nouvelle tête 890684cab8, merge auto sans conflit — le README Serre100 s'est auto-fusionné).

Live-read freshness — cause mesurée, non base-inherited : la tête de la PR précédait le fix de main be9979b424 (GOL-01 Annexe F, live-read refresh après le merge du moteur torique, #22717). Le carnet GOL-01-Regles-Vie-Lean.ipynb de la branche portait la version antérieure (sorties citant Pillars.lean à 414 lignes contre 422 au fichier) ; main est FRESH. Le refresh de branche apporte la version refreshée de main — vérifié localement après merge : check_live_read_freshness.py → 2/2 FRESH (GOL-01 et Compression-04). Aucun fichier du périmètre de la PR (carnet 28 Möbius) n'est touché par ce refresh.

validate (validation-matrix) — le job est continue-on-error sur le dispatch : l'étape qui rend le job rouge est l'upload d'artefact results/validation_run_*.json quand le dispatch n'a produit aucun fichier. Les logs du runner (self-hosted coursia-ephemeral) sont purgés (log not found, zip de 24 octets) — non reproducible côté CI, classé environnemental tant que la jambe ne rougit pas de nouveau. Le nouveau head relance la matrice complète ; si validate rougit à la nouvelle tête avec les logs disponibles, le diagnostic passera par les logs.

This branch has not been deployed

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

Labels

pr-overlap Advisory: another open PR touches the same files (organ #13615)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants