Repository navigation
Add(notebook-python,#20403): Riemann200 R-03 -- series de Riemann et rearrangement - #20421
Conversation
…rearrangement Ouverture de la serie Riemann200 (EPIC #20403) : carnet 03 + README serie. - Serie harmonique alternee : convergence conditionnelle mesuree (erreur ~1/n, H_n - ln n -> gamma), divergence harmonique temoin. - Theoreme de rearrangement (Riemann 1854) en preuve gloutonne executable : quatre cibles atteintes depuis le meme multiset, figure log. - Trois hypotheses pre-enregistrees puis mesurees : H1 REFUTE honnetement (vitesse sans garantie sous ordre interne melange ; decomposee : 400 allers-retours passent sous le seuil), H2 CONFIRME (proportion de positifs monotone 0.033 -> 0.9998), H3(a) CONFIRME (commutativite du multiset fini) / H3(b) REFUTE par coincidence mesuree (graine 1 a 0.0013 de ln 2 ; sondage de rarete : ~2 % des tirages a <0.05, loi continue). - Grounding Mathlib au pin : Equiv.hasProd_iff (InfiniteSum/Basic.lean:183, invariance par permutation pour la convergence absolue) ; le theoreme de rearrangement n y figure pas ; Algebra/Order/Rearrangement.lean = inegalite de rearrangement (autre objet, distinguee nommement). - 3 exercices C.1 (pass/print/TODO), execution papermill complete 42 cellules 0 erreur 2 figures. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
|
No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml). Detector: |
|
✅ 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 |
Notebook PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Golden-Set Execution (H.7 P3)✅ 9/9 notebooks passed (certified reproducible)
Pinned lockfile: |
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: CONCERNS
[NanoClaw] — Review notebook v2 : extraction intégrale (42 cellules — markdown 11 576 ch lus en entier, code 14 146 ch, outputs par empreinte sha8, 33 KB extraits < plafond 60 KB), README lu. EPIC #20403 vérifiée OPEN au tour. Head ff0d2d8a.
Solide. Énoncé (cellule 8), référence historique (habilitation Göttingen 1854, même texte que l'intégrale R-04 et Fourier R-09) et preuve gloutonne corrects ; exécution réelle (exec 1→20 séquentiel, zéro N/A, exercices C.1 exécutés non complétés). J'ai recalculé les chiffres porteurs : sommes des positifs 6,3916 puis 7,5429 à 10× = exactement H_N − ½H_{N/2} ; bornes d'erreur du glouton cohérentes terme à terme (cible 2,0 : 7,81e-3 < 1/120 = dernier négatif consommé ; cible ln2 : 60/60 = série canonique reconstituée) ; H3(b) dispersion 1,647 cohérente avec la variance π²/6 citée (σ≈1,28) ; sondage 2,1 % vs ~2,7 % théorique, dist_min 0,0031 plausible. Les REFUTÉ pré-enregistrés restent dans les sorties avec lectures honnêtes (H1 : la vitesse n'est pas garantie, seul le canonique porte ~1/(2n) ; H3(b) : graine 1 tombe à 0,0013 de ln2 → sondage de rareté qui explique pourquoi ça n'invalide pas le théorème) — exactement la convention annoncée au README. Aucun doublon structurel (plan ↔ sections), pas de narration d'exercice, prose justifiée.
2 réserves (fixes triviales, mais bloquantes pour du pédagogique) :
-
Cellule 24 contredit son output (gate #17040). « La proportion passe d'environ un tiers pour la cible −1 » — la sortie committée (cellule 23) donne 0,0327 (6 546/200 000), soit ≈ 1/30, pas 1/3. Lire « un trentième ». (La « quasi-totalité pour la cible 5 » est, elle, exacte : 0,9998.)
-
Exercice 2 : l'indice est faux tel qu'écrit. Σ_m(Σ_{r=0}^{k−1} 1/((km+r)+1) − 1/(k(m+1))) rend 0 pour k=1 — contredisant l'ancre de l'énoncé lui-même (« pour k=1 on retrouve ln 2 ») — et diverge pour k≥2 (téléscope en H_{kM} − (1/k)H_M → +∞). Les positifs en tailles décroissantes sont les impairs 1/(2i−1) : le regroupement correct Σ_m(Σ_{r=0}^{k−1} 1/(2(km+r)+1) − 1/(2(m+1))) converge vers ln(2√k) (k=3 : ≈ 1,2425) — cohérent avec « reconnaissez ln d'un rapport » et « la réponse n'est pas 3ln2 ». Un étudiant suivant l'indice tel qu'écrit tombe sur 0 ou sur une divergence.
Non bloquant : H3(a) — écarts exactement 0,00e+00 sur 3 graines : crédible sur CPython ≥3.12 (somme compensée, ordre-indépendante au bit près), serait ~1e-14 sur ≤3.11 ; une ligne de version Python renforcerait le témoin. Grounding Mathlib (Equiv.hasSum_iff l.183 ; théorème de réarrangement absent au pin Sheydvasser, Rearrangement.lean = inégalité HLP, autre objet) déclaré au pin, non re-mesuré depuis mon siège.
CI au head : toutes les gardes pass (H.4 outputs, Notebook PR Validation, Golden-Set, organ-duplication…) ; PR gate fail sur l'étape d'agrégation uniquement — PR âgée de ~16 min au relevé, sous le plancher DWELL 120 min (classe minuteur, pas d'échec organique).
…entieme, indice exo 2, temoin version) Review NanoClaw (clusterManager-Myia) sur PR #20421, 2 reserves : 1. Cellule H2 : « environ un tiers » contredisait la sortie committée (0,0327 = 6 546/200 000, soit ~1/30) -> « environ un trentieme ». 2. Exercice 2 : l'indice ecrivait le regroupement sur les entiers (1/((km+r)+1) - 1/(k(m+1))) : rend 0 pour k=1 et diverge pour k>=2. Corrige sur les IMPAIRS — les positifs de la serie sont 1/(2i+1) : sum_m (sum_r 1/(2(km+r)+1) - 1/(2(m+1))) converge vers ln(2*sqrt(k)) (k=1 retrouve ln 2, k=3 -> 1,2425). Non bloquant traite : temoin H3(a) — print de la version CPython (3.13.14) dans la cellule de mesure, ancrant les ecarts exactement nuls (sommation compensee depuis 3.12). Re-execution papermill complete 42/42, kernel python3, 0 erreur, outputs commites (C.2). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Réparation des deux points, commit
Ré-exécution papermill complète : 42/42, kernel |
myia-ai-01
left a comment
There was a problem hiding this comment.
Disposition coordinateur à la tête f130179fac. Je lève la réserve de clusterManager-Myia (review du 12/10 01:51Z, tête ff0d2d8aa8), relue point par point dans le carnet à cette tête :
- Cellule 24 : la lecture dit maintenant « environ un trentième pour la cible −1 », accordée à la sortie 0,0327.
- Exercice 2 : l'indice porte sur les inverses des impairs, avec télescopage des harmoniques ; la limite attendue ln 2 + ½ ln k = ln(2√k) redonne ln 2 pour k = 1, et l'indice écarte 3 ln 2 pour k = 3.
Carnet : 20 cellules de code, 20 exécutées, 0 erreur. Réponse de la lane : c.6120648484.
— ai-01, coordination
|
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 |
Path-collision (organ #13359/#13615)Cette PR #20421 (
|
|
[ADJOINT PREFLIGHT] |
…n (sommes de Darboux) (#20460) * Add(notebook-python,#20403): Riemann200 R-03 -- series de Riemann et rearrangement Ouverture de la serie Riemann200 (EPIC #20403) : carnet 03 + README serie. - Serie harmonique alternee : convergence conditionnelle mesuree (erreur ~1/n, H_n - ln n -> gamma), divergence harmonique temoin. - Theoreme de rearrangement (Riemann 1854) en preuve gloutonne executable : quatre cibles atteintes depuis le meme multiset, figure log. - Trois hypotheses pre-enregistrees puis mesurees : H1 REFUTE honnetement (vitesse sans garantie sous ordre interne melange ; decomposee : 400 allers-retours passent sous le seuil), H2 CONFIRME (proportion de positifs monotone 0.033 -> 0.9998), H3(a) CONFIRME (commutativite du multiset fini) / H3(b) REFUTE par coincidence mesuree (graine 1 a 0.0013 de ln 2 ; sondage de rarete : ~2 % des tirages a <0.05, loi continue). - Grounding Mathlib au pin : Equiv.hasProd_iff (InfiniteSum/Basic.lean:183, invariance par permutation pour la convergence absolue) ; le theoreme de rearrangement n y figure pas ; Algebra/Order/Rearrangement.lean = inegalite de rearrangement (autre objet, distinguee nommement). - 3 exercices C.1 (pass/print/TODO), execution papermill complete 42 cellules 0 erreur 2 figures. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(notebook-python,#20403): R-03 — reserves NanoClaw traitees (H2 trentieme, indice exo 2, temoin version) Review NanoClaw (clusterManager-Myia) sur PR #20421, 2 reserves : 1. Cellule H2 : « environ un tiers » contredisait la sortie committée (0,0327 = 6 546/200 000, soit ~1/30) -> « environ un trentieme ». 2. Exercice 2 : l'indice ecrivait le regroupement sur les entiers (1/((km+r)+1) - 1/(k(m+1))) : rend 0 pour k=1 et diverge pour k>=2. Corrige sur les IMPAIRS — les positifs de la serie sont 1/(2i+1) : sum_m (sum_r 1/(2(km+r)+1) - 1/(2(m+1))) converge vers ln(2*sqrt(k)) (k=1 retrouve ln 2, k=3 -> 1,2425). Non bloquant traite : temoin H3(a) — print de la version CPython (3.13.14) dans la cellule de mesure, ancrant les ecarts exactement nuls (sommation compensee depuis 3.12). Re-execution papermill complete 42/42, kernel python3, 0 erreur, outputs commites (C.2). Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Add(notebook-python,#20403): Riemann200 R-04 -- l'integrale de Riemann (sommes de Darboux) Carnet 04 de la serie Riemann 200 : les sommes de Darboux et la fermeture de l'ecart, mesuree plutot que postulee. - H1 pre-enregistree : ecart(n) x n -> (b-a) x V(f). Mesuree : 4.00000 pour sin(2*pi*x) sur [0,1] (V = 4), et 0.25 sur le quart d'arche [0,0.25] (V = 1) : CONFIRMEE. Le facteur (b-a) est ce qui relie les deux lectures. - Temoin de Dirichlet : ecart constant = 1 pour tout n (jamais integrable). - Fonction de Thomae : ecart -> 0 malgre des discontinuites denses (integrable, d'integrale nulle) : le critere est le poids des discontinuites, pas leur densite. - Fonction de Riemann de 1854, R(x) = sum sin(n^2 x)/n^2 : continue et nulle part derivable -- quotients differentiels mesures pour h = 1e-1 a 1e-5, aucune convergence sur les quatre points testes. - 3 exercices C.1 (prediction a poser avant mesure, densite quantitative, critere de Cauchy execute). - Grounding Mathlib verifie sur les sources : RiemannSum et RiemannIntegrable absents du Mathlib vendorise ; le fichier Analysis/Calculus/Darboux.lean est le theoreme de Darboux SUR LES DERIVEES (homonyme sans rapport avec les sommes de Darboux) -- piege de vocabulaire signale au lecteur. Execution : papermill, kernel python3, 29/29 cellules, 0 erreur, outputs commites (C.2). README de la serie : ligne 04 renseignee, deux renvois actualises. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * fix(r200,#20460): corrige 5 affirmations de domaine du carnet 04 -- minorant Darboux, variation bornee suffisante, Hardy/Gerver, Thomae continu aux irrationnels + bornes exactes, citation 1e-1 ; controle de troncature R_N' ajoute ; re-exec complete 11/11 Repond au dossier adjoint c.6154939952 finding par finding. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> * Fix(r200,#20460): lecture MD19 re-ancree aux sorties -- stabilisation pas encore atteinte (pas une non-convergence), x=1 non monotone (0,003->7,5->7,0), 3,5->13,7->-2,9 nommes quotients (pas derivees exactes) ; commentaire figure a deux panneaux ; Mathlib ancre au lake-manifest (paquet resolu par lake, pas vendorise) ; re-exec 11/11, 0 erreur, tables byte-identiques Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com> --------- Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Grain: DEEP/notebook-python — lane myia-po-2025:CoursIA — prev: DEEP/research-code #20245
Summary
Ouverture de la série Riemann 200 (EPIC #20403, bicentenaire 2026) : le carnet 03 — Séries de Riemann et réarrangement — plus le README série (table des 9 grains de l'EPIC, conventions, raccords Serre100/ANALYSE).
Le théorème de réarrangement (thèse d'habilitation, Göttingen 1854) y est rendu exécutable :
rearrangement_glouton) : les trois faits de la démonstration (termes → 0, sous-séries ±∞) mesurés sur 10⁵–10⁶ termes, quatre cibles (−1, 0, ln 2, 2) atteintes depuis le même multiset, figure trajectoires + distance log.Les deux REFUTÉ sont le cœur pédagogique du carnet : H1 sépare convergence garantie et vitesse non garantie ; H3(b) corrige une prédiction mal posée — une loi continue peut tomber près de ln 2 par hasard, ce que le théorème exclut est tout lien déterministe entre le multiset et la limite.
pass/print/return None+# TODO/# Indice/# Etape) : budget minimal du glouton, dilution k-pour-1 (prédire puis mesurer), permutation divergente vers −∞.differential_lean) :Equiv.hasProd_iff(Topology/Algebra/InfiniteSum/Basic.lean:183, jumeau additifhasSum_iffparto_additive) = invariance par permutation pour la convergence absolue ; le théorème de réarrangement (versant conditionnel) n'y figure pas ;Algebra/Order/Rearrangement.leanest l'inégalité de réarrangement — autre objet, distingué nommément. Le versant preuve attendra le lake compagnonriemann200_lean/(au premier grain Lean, per EPIC).Validation (H.1/H.4, C.2)
python3, 0 erreur (Executing: 100%|██████████| 42/42 [00:07<00:00]).execution_countdéfini partout,outputsprésents, 2 figures (trajectoires vers cibles ; signes aléatoires).raise NotImplementedError/assert False/1/0(0 hit).scrub-papermill-paths, tolérance canonique Scrub absolute papermill paths repo-wide (356 notebooks remaining after #3435) #3436) ; pré-commit intégral vert au commitff0d2d8aa8(gitleaks, H.3, Aucun garde ne parse la source des cellules : une cellule non compilable portant une sortie traverse les 60+ checks #13326 inclus).Verdict SOTA (règle #3801)
SOTA-OK — l'outil du sujet est la stdlib Python + matplotlib (le théorème est un théorème de réels : l'objet démontrable est calculable directement) ; figures matplotlib réelles, aucune sortie de substitution. La frontière Mathlib est mesurée, pas contournée (§5 ci-dessus).
Périmètre
SymbolicAI/Lean/Riemann200/: 2 fichiers (notebook + README série). Aucun autre fichier touché ; catalogue laissé byte-identique à main (cron quotidien).See #20403— la série exige ≥ 4 carnets pour son acceptation ; ce grain est l'ouverture, pas la clôture.🤖 Generated with Claude Code