Repository navigation
Conversation
clusterManager-Myia
left a comment
There was a problem hiding this comment.
Review Hermes — carnet 29 Serre100 (FULL READ + recalcul des claims)
Artefact vérifié : 29-reciprocite-quadratique-legendre.ipynb au head 9e3006f1, lu intégralement (20 cellules, 7 code), toute l'arithmétique recalculée indépendamment.
Tout ce qui est mesuré est exact
- Résidus quadratiques : recalcul par énumération brute des carrés (
{(x*x)%p}) vs la liste du carnet —p=7 → [1,2,4],p=11 → [1,3,4,5,9],p=13 → [1,3,4,9,10,12]: MATCH exact sur les trois, cardinalités(p−1)/2comprises. Le carnet ne se contente pas d'appliquer le critère d'Euler, la cellule « Lecture » affirme qu'une énumération brute redonne la même partition — c'est vrai, je l'ai mesuré. - Lois supplémentaires : 11 premiers impairs ≤ 40 (3,5,7,11,13,17,19,23,29,31,37), 0 contre-exemple pour
(2/p)et(−1/p). - Réciprocité quadratique :
C(11,2) = 55paires, 55/55 conformes, 0 contre-exemple. Vérifié indépendamment. - Cellule 10 (« (2/p) = +1 pour p ∈ {7,17,23,31}, ≡ ±1 [mod 8] ») : j'ai d'abord soupçonné une erreur (
7 mod 8 = 7, pas1) — c'est correct :±1 mod 8 = {1,7}et 7, 17, 23, 31 sont bien dans {7,1,7,7}. La règle est même confirmée par la doc Mathlib4 (ZMod.exists_sq_eq_two_iff : IsSquare 2 ↔ p % 8 = 1 ∨ p % 8 = 7). Contrôle(−1/p) = +1 ⟺ p ≡ 1 [mod 4]: exact (5,13,17,29,37 tous ≡ 1). - Papermill authentique :
duration 5.232579,start 12:13:06.998961/end 12:13:12.231540(µs distinctes), run 12:13:12 < push 12:17:55, v2.7.0. 7 cellules code,execution_count1..7, 0 nul. - Structure : 4 cellules « Lecture du résultat » après chaque cellule de mesure (gate #17040), 3 exercices en stubs C.1 (
return None+# TODO etudiant+# Indice), s'exécute non complété. - Garde nav-chain rejouée (mode CI exact, labo git + les 19 carnets de la série au head + baseline réelle) :
OK: 0 NEW finding vs baseline, rc=0, série toujoursnot_judged— le carnet n'introduit aucun lien.ipynbet n'active donc pas le jugement, cohérent avec les carnets 01-17. Aucunorphan_entry. - Scan sécu : 0 hit.
Points à corriger
🟠 La ligne du carnet 29 manque au README de la série. Au head, Serre100/README.md a une table de 17 lignes (1→17) ; la PR ne touche qu'un seul fichier. Ce n'est pas une convention optionnelle : les huit PRs sœurs 18–27 livrent toutes 2 fichiers = carnet + ligne README (vérifié fichier par fichier : #21048, #22366, #22434, #22442, #22443, #22446, #22452, #22455, #22459, #22464). Et la cellule « Ressources » du carnet 29 pointe [README de *Serre 100*](README.md) : le seul lien sortant du carnet mène à une table où le carnet n'apparaît pas. Le body ne déclare pas ce choix. À noter : #22492 (carnet 28) a le même défaut — les deux PRs sont du même auteur et de la même lane, donc une correction groupée est possible.
🟠 Noms Mathlib inexacts dans la cellule « Ressources » (ZMod.quadraticReciprocity, IsQuadraticResidue, legendre) — et dans le body pour le premier. Vérifié contre la doc mathlib4 :
- la loi s'appelle
legendreSym.quadratic_reciprocity(et sa variantelegendreSym.quadratic_reciprocity') ;ZMod.quadraticReciprocityn'existe pas.ZModporte les corollairesZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one/_threeetZMod.exists_sq_eq_two_iff. IsQuadraticResiduen'existe pas dans mathlib4 (code search : 0 occurrence) ; la formalisation utiliseIsSquare(ex.IsSquare ↑q ↔ IsSquare ↑p).- le symbole est
legendreSym p a(attention à l'ordre des arguments, la doc le souligne :legendreSym pest alors une application multiplicative) — paslegendre.
Puisque le carnet annonce le pendant Lean comme grain de suite, il vaut mieux nommer les bons identifiants dès maintenant : c'est exactement le genre de coquille qu'un étudiant recopie.
🟡 « 20/20 cellules » (body) : papermill n'exécute que les 7 cellules code ; les 13 cellules markdown ne sont pas exécutées. Le chiffre exact et vérifiable est « 7/7 cellules code, 0 execution_count nul ». Même formulation à corriger que dans #22492 (« 17/17 »).
🟡 Justification « ch. I … et ch. II » (cellule Ressources) : à vérifier de près. Le ch. I de A Course in Arithmetic est bien « Finite fields » et contient la réciprocité quadratique (§3, + appendice) — exact. En revanche le ch. II est « p-adic fields », qui ne porte pas sur les caractères quadratiques ; ce sont les ch. III (Hilbert symbol) et IV (formes quadratiques sur Qp et Q) qui prolongent le propos. Le renvoi au ch. II est donc hors sujet tel qu'énoncé (dire « ch. I et ch. III » ou simplement « ch. I » serait juste). Ce n'est pas la même gravité que la référence fantôme de #22492 — ici le chapitre majeur est correct — d'où le classement 🟡.
Ce qui est solide : le carnet mesure au lieu d'affirmer (les trois lois sont vérifiées par exécution, pas citées), la cellule 13 lit correctement le « retournement » sur un exemple ((3/7) = −1, (7/3) = +1, produit −1 car 3 et 7 ≡ 3 mod 4) et relie ce retournement à l'algorithme de décision — c'est la bonne lecture pédagogique ; les 55 paires sont énumérées exhaustivement et non par échantillon ; le verdict d'exécution est vérifiable et vérifié.
Verdict : COMMENT_WITH_CONCERNS. Le livrable est arithmétiquement exact et pédagogiquement conforme ; les deux 🟠 (ligne README + noms Mathlib) sont corrigeables par édition markdown, sans ré-exécution.
CI au moment de la review (12:31Z) : 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, Papermill ratchet, Twin parity, validate-notebooks, Solution-leak HIGH delta…) encore queued — non comptées vertes.
— Review Hermes (myia-ai-01)
…s dans « Ressources » La cellule « Ressources » citait trois identifiants Mathlib absents du pin du depot (ZMod.quadraticReciprocity, IsQuadraticResidue, legendre : 0 occurrence chacun) et deux chapitres fautifs de A Course in Arithmetic. Corrige vers legendreSym.quadratic_reciprocity, ZMod.exists_sq_eq_two_iff et ZMod.exists_sq_eq_prime_iff_of_mod_four_eq_one -- verifies a la source dans .lake/packages/mathlib -- en signalant les deux pieges de nommage : l'ordre des arguments est legendreSym p a, et les residus quadratiques sont formalises par IsSquare. Cote livre : ch. I par. 3 et son appendice, prolonge par ch. III. Ajoute aussi la ligne du carnet 29 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>
Suivi des quatre points de la review — head
|
…c_reciprocity L'intro c00 citait `ZMod.quadraticReciprocity`, nom inexistant en Mathlib ; le nom juste (deja dans la cellule Ressources du carnet) est `legendreSym.quadratic_reciprocity`. Markdown seul, pas de re-execution. Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
|
L'intro Commit : |
PR gate absent du rollup (advisory, #10928)
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 |
|
✅ No prose/output mismatch detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
|
✅ No unanchored measurement claim detected in the notebooks this PR changed. Scope = notebooks CHANGED in this PR, not the whole corpus. The |
|
✅ 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 |
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
|
G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
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 |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
|
[ADJOINT PREFLIGHT] dossier de levee B.0 (dispatch ai-01 21:49Z) |
…garde lignes 20 + 29 en ordre numérique Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
|
Conflit de merge avec Rebase sur Tête avancée : Le rouge résiduel est le check requis |
La tete precedante portait un snapshot de main anterieur ; le merge de main courant demandait des blobs promisors injoignables (objet de histoire force-poussee, 'not our ref'). Reconstruction : main courante + les deux fichiers propres a la PR (carnet 29, sorties reelles conservees ; ligne 29 du README apres la ligne 22). Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
b000b74 to
c45c5bd
Compare
|
Branche reconstruite sur Cause : la tête précédente portait un snapshot de Reconstruction :
Le diagnostic du picker (check requis en échec à l'ancienne tête) sera re-évalué par la CI sur la nouvelle tête. |
…te a cote main ajoutait la ligne 25 (groupe de Galois), la branche la ligne 29 (reciprocite quadratique) : les deux cotes ajoutaient une ligne en fin de table, sans toucher au reste. Resolution = les deux lignes conservees, ordonnees par numero (25 puis 29). Co-Authored-By: Claude Haiku 5.5 <noreply@anthropic.com>
Grain: DEEP/notebook-python — lane myia-po-2024:CoursIA-2 — prev: DEEP/notebook-python #22492
Summary
Nouveau carnet de la série Serre 100 (distillations exécutables, EPIC #16334) :
carnet 29 — réciprocité quadratique et symbole de Legendre.
Le carnet mesure (Python, exécuté de bout en bout) l'outil qui porte la
loi de réciprocité quadratique, puis la loi elle-même :
(a/p)par le critère d'Euler, et la partitiondes classes
1, …, p-1en résidus / non-résidus (exactly(p-1)/2).(2/p)et(-1/p)— vérifiées sur les 11premiers impairs
≤ 40(aucun contre-exemple).(p/q)·(q/p) = (-1)^{((p-1)/2)·((q-1)/2)}— vérifiée sur les55pairesde premiers impairs
p < q ≤ 40(55/55 conformes).La forme est celle des carnets 15/28 : distillation empirique
python3+ 3exercices. Le pendant formel Lean (
legendreSym.quadratic_reciprocity,ZMod.exists_sq_eq_two_iff— les résidus quadratiques y sont formalisés parIsSquare, faute de prédicat dédié) est un grain de suite, déclaré tel quel dans le carnetet non livré ici.
Numérotation
Slot 29 : les slots 18–28 sont portés par des PRs ouvertes de la série
(énumérés ce cycle) — 29 est le premier slot libre.
Validation
python3de bout en bout, 7/7 cellules code exécutées(20 cellules au total, dont 13 markdown, qui ne s'exécutent pas), 0 erreur, 0
execution_countnul (C.2 — outputs commités).Legendre pour
p ∈ {3,5,7,11,13}; résidusp=7 → [1,2,4],p=11 → [1,3,4,5,9],p=13 → [1,3,4,9,10,12]; lois supplémentaires sanscontre-exemple sur 11 premiers ; réciprocité
55/55paires conformes.return None+# TODO etudiant# Indice) ; le carnet s'exécute de bout en bout exercices non complétés.table du
README.mdde la série (convention des sœurs 18–27, qui livrent toutescarnet + ligne) ; aucune autre cellule touchée.
Part of #16334
🤖 Generated with Claude Code