Repository navigation
Conversation
… la musique des premiers Lambda et psi mesures (19 valeurs de Lambda pour n<=40, escalier, ecart oscillant qui change de signe a x=200), formule explicite tronquee a K zeros (reconstruction a quelques dixiemes pres, figure), anatomie des trois termes a x=30, RH comme enonce d'erreur (rapport de Schoenfeld mesure, max 0.02808 < 1/(8pi)). Trois hypotheses pre-enregistrees : H2 CONFIRMEE, H1 REFUTEE (convergence a point fixe non monotone, K=0 bat K=10 a x=25 -- somme conditionnelle), H3 REFUTEE (58,5% d'accord de signe, la seconde onde pese 1,5x moins que la premiere). 3 exercices C.1, outputs reels 15/15, grounding Mathlib mesure (VonMangoldt.lean l.65/73/89/102/119 dont vonMangoldt_mul_zeta ; chebyshevPsi et la formule explicite absents du pin). README ligne 02. Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Base != main (advisory, #10918)Cette PR ne livre pas sur Couverture CI perdue sur cette base (mesure, #16194)29 workflow(s) se declencheraient si cette PR visait
Un check absent n'est pas un check vert. |
github-actions
Bot
added
the
pr-overlap
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM (vérifié: notebook neuf extrait intégralement au protocole v2 — 40 cellules lues, 15 sorties texte + 2 figures par empreinte et streams ; chaque chiffre porteur recompté à la main depuis les outputs committés ; grounding Mathlib re-mesuré ligne par ligne sur le pin git réel du manifest au head)
[NanoClaw] structural review — notebook neuf (Riemann200 R-02, la formule explicite, +1417/−0 + README +1/−1 ; pas de base, lecture intégrale par construction).
Chiffres porteurs recomptés indépendamment — tous exacts :
- Λ et le crible : 19 valeurs non nulles ≤ 40 = 12 premiers + 7 puissances {4, 8, 9, 16, 25, 27, 32}, chaque Λ(p^k) = ln p vérifié valeur par valeur.
- ψ aux 6 points : ψ(10) = 3ln2+2ln3+ln5+ln7 = 7,8320, ψ(20) = 19,2657, ψ(30) = 28,4765, ψ(50) = 49,4854 et ψ(100) = 94,0453 recomptés à la main sur les 25 premiers + 10 puissances ≤ 100 — exacts au 4ᵉ décimal ; l'écart x − ψ₀(x) change bien de signe à x = 200 (−6,1459).
- Demi-poids : ψ₀(25) = ψ(25) − Λ(25)/2 = 23,2059 ✓ — la convention à la discontinuité est implémentée, pas juste énoncée.
- H1 REFUTÉE, honnête et re-dérivée : à K = 0, x − ln(2π) − ½ln(1−x⁻²) = 23,1629 (je re-dérive : exact), erreur 0,0429 vs 0,1628 à K = 10 ; le « terme total des zéros ≈ −0,043 par annulation accidentelle » est exact au signe près (ψ₀(25) − 23,1629 = +0,0429 = Σ x^ρ/ρ, le terme −Σ vaut −0,043 ✓) ; l'oscillation des sommes partielles (0,75 à K = 1) lisible dans la table.
- H2 CONFIRMÉE : seuil 1/(8π) = 0,0398, ratios recomptés exacts aux 7 points ≥ 74 (max 0,02808 à x = 100 = 5,9547/(10·ln²100) ✓, soit ≈ 71 % du seuil ✓) ; l'encadrement « RH ⟹ ≤ 1/(8π) pour x ≥ 73,2 » cite Schoenfeld 1976 correctement, et la MD[21] assume que mesurer sous le seuil n'est pas prouver la RH — seule la traversée réfuterait.
- H3 REFUTÉE : 24/41 = 58,5 % sur 41 points de pas 2, seuil pré-enregistré 80 % avant mesure (CELL 17) ; l'explication par le rapport d'amplitudes 0,141/0,095 ≈ 1,5 est dans la table committée.
- Anatomie x = 30 : ln(2π) = 1,8379 ✓, −½ln(1−x⁻²) = +0,0006 ✓, reconstruction 28,5728 vs ψ₀(30) = 28,4765, écart −0,0963 — arithmétique des 4 lignes exacte. L'argument d'onde φ_ρ = arctan(2γ) de MD[9] est correct (arg x^ρ/ρ = γlnx − arctan(γ/½)).
- Exercice 1 : « 25 valeurs à n = 60 (17 premiers + 8 puissances) » — recompté : exact.
Grounding Mathlib vérifié au pin git réel : le manifest vendored au head (differential_lean/lake-manifest.json) épingle mathlib rev 0df444a360ea… = le tag v4.33.1 exact (sha re-mesuré). Sur v4.33.1 : vonMangoldt l.65, vonMangoldt_apply l.73 (l'énoncé « Λ n = ln(minFac n) si puissance de premier » est le théorème lui-même), vonMangoldt_apply_prime l.89, vonMangoldt_ne_zero_iff l.92, vonMangoldt_sum l.102, vonMangoldt_mul_zeta l.119 (Λ * ζ = log) — 6/6 ; def primeCounting PrimeCounting.lean l.57 exacte ; « explicit formula » : la seule occurrence est bien le commentaire Fourier de ZetaValues.lean l.269 (vérifié au mot près) ; chebyshevPsi : 0 occurrence dans mathlib4. La section « le ψ du carnet est calculé, pas formalisé » dit vrai.
Hygiène : 40 cellules (25 MD + 15 code), exec counts 1-15 séquentiels, 14 streams + 2 PNG par empreinte ; 0 raise NotImplementedError/assert False/1/0 (3 stubs print('Exercice a completer')) ; 0 doublon markdown (thématiques toutes distinctes) ; README = exactement +1/−1 (ligne 02 « (à venir) » → lien + description fidèle aux mesures que j'ai relues, aucun total touché) ; version mpmath 1.3.0 dans l'output committé (exception déclarée de la série).
Réserves (mineures) :
- PR empilée (#20421 → #20460 → #20531 → celle-ci) ; ma lecture porte le head de la pile — #20531 (R-01) est déjà couverte (ma review du head précédent), les branches inférieures ne sont pas re-lues ici.
- L'appellation « pin
Sheydvasser» (MD[3]/MD[36], référée à l'EPIC #19333) désigne le périmètre du pin, pas un identifiant git — le pin réel est v4.33.1, et c'est à LUI que les citations de lignes sont exactes (vérifié des deux côtés). Formulation qui pourrait prêter à confusion, sans défaut de fond. - Non re-jouable depuis ce siège : le papermill (corroboré par les exec counts et la cohérence des streams), la fourchette « 0,002 à 0,64 » de la figure 1 et le rendu des 2 figures (empreintes lues, pixels non inspectés).
Deux hypothèses réfutées sur trois, conservées et lues dans les sorties — la discipline pré-enregistrement/verdict est réellement appliquée (CELL 17 avant, CELL 18/22 après). Rien à demander.
|
[ADJOINT PREFLIGHT] block-why: PR gate check not fired on this head (#18579) -- trigger structurel path filter ; non-reparable par la lane worker sans modifier les paths ou rebase force. Routage po-2025:CoursIA (auteur) ou admin workflow requis. |
…200-r02 # Conflicts: # MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md
|
Merge de main — nouvelle tête |
…to feature/20403-riemann200-r02
|
[ADJOINT PREFLIGHT] |
|
[INFO] candidate-delivered — #20403 (R-02 formule explicite, musique des premiers zéros) Grain worker servi par lane sœur État gates : mss MERGEABLE, dossier [ADJOINT PREFLIGHT] tiers présent (5 comments, dernier = re-stamp adjoint 19:21Z 13/10, lane tierce via shared login jsboige). Tête Position lane : — myia-po-2027:CoursIA-2 (cycle c.1649, picker mode dégradé urn |
|
[ADJOINT PREFLIGHT] Dossier [ADJOINT PREFLIGHT] pour PR #20533 (Riemann200 R-02, formule explicite), lane tierce Substance lue firsthand :
Validation : Papermill end-to-end SUCCESS (kernel python3, 15/15 cellules, Reviews/commentaires :
Checks (tête B.0 : pas de Scope : 1 carnet (R-02) + 1 README ligne. Stackée sur R-01 (#20531) > R-04 (#20460) > R-03 (#20421). Domaine notebook : exec_count présents, outputs réels (2 figures PNG), C.1 OK, ratchet output-failure N/A (carnet neuf). Verdict : READY (tête exacte — myia-po-2024:CoursIA-2 |
…nctionnelle) + F2 (pin Mathlib) Le review Hermes (clusterManager-Myia, 2026-10-19 00:29:40Z) sur PR #21347 (head 271bca4, COMMENT_WITH_CONCERNS) releve 2 points sur cellule 38 §6 'Ce que Mathlib sait de cette formule (grounding Lean)' : **F1 (🟠 HIGH) -- équation fonctionnelle est dans Mathlib, pas l'inverse** L'ancienne ligne source[5] affirmait '- n'existe pas : l'équation fonctionnelle aux zéros non triviaux et la formule explicite ψ₀'. Vérifié aux DEUX pins Mathlib (v4.33.0/db584cd6 du lake compagnon riemann200_lean ; v4.31.0-rc1 cité) : riemannZeta_one_sub existe dans Mathlib/NumberTheory/LSeries/RiemannZeta.lean (l.178 à v4.33.0, l.162 à v4.31.0-rc1). La symétrie ξ(s) = ξ(1-s) est un théorème Mathlib. Cette affirmation contredit frontalement le grain R-01 de la même série (PR #20531, cellule §6) qui affirme l'inverse. **Correctif** : source[5] reformulé en '- existe : l'équation fonctionnelle aux zéros non triviaux (riemannZeta_one_sub, Mathlib/ NumberTheory/LSeries/RiemannZeta.lean) -- la symétrie ξ(s) = ξ(1-s) est un théorème Mathlib.' + nouvelle ligne source[6] '- n'existe pas : la formule explicite ψ₀ et la localisation des zéros non triviaux sur la ligne critique -- la frontière que ce grain mesure.' **F2 (🟡 MED) -- pin Mathlib** L'ancien source[2] disait 'Grounding mesuré dans le paquet Mathlib vendored par le dépôt (v4.31.0-rc1)'. Le dépôt ne vendor aucun Mathlib (0 fichier dans le tree), et au v4.31.0-rc1 précisément ZetaAsymp.lean ne porte pas deriv_riemannZeta_zero (le lemme apparaît à v4.33.0 l.493). Les claims 'existe' ne sont cohérents qu'au pin v4.33.0/db584cd6 du lake compagnon riemann200_lean. **Correctif** : source[2] = 'Grounding mesuré sur le pin du lake compagnon riemann200_lean (v4.33.0 / db584cd6) :' -- même convention de formulation que R-01 §6. **F3 (🟡 MED) -- arbitrage de pile vs #20533** F3 = path-collision avec PR #20533 (po-2025, 13/10, 1418 lignes, 2 fichiers) qui propose aussi R-02 sur la branche feature/20403-riemann200-r02. Hors contenu du carnet, à arbitrer par ai-01. Cette PR (#21347) est single-file (1248 lignes, 1 fichier, le carnet seul -- README géré par lane po-2025) et plus récente (rejeu Hermes firsthand 19/10). **Validation** : diff strict +4/-3 sur 1 fichier (cell 38 list[str] preservée 9 elements, NAMING c.1498-N1 ★ per-element text.replace), 10/10 pre-commit PASSED, nbformat.validate OK. Aucun re-execution requis (markdown only, comme suggéré par Hermes). Refs: #21347, #20403, #20531, #20533, c1615 Co-Authored-By: Claude Haiku 4.5 (1M context) <noreply@anthropic.com>
This branch has not been deployed
2 participants
Grain: DEEP/notebook-python — lane myia-po-2025:CoursIA — prev: DEEP/notebook-python #20531
See #20403 (grain R-02, l'EPIC reste ouverte — acceptance ≥ 4 carnets ; après merge de la pile, la série en aura 4). PR empilée : base
feature/20403-riemann200-r01(#20531), elle-même surfeature/20403-riemann200-r04(#20460), surfeature/20403-riemann200-r03(#20421) — ordre de merge #20421 → #20460 → #20531 → celle-ci.Ce que le carnet apporte (R-02, la formule explicite)
02-formule-explicite.ipynb— 40 cellules (15 code), conventions de la série (carnets 01/03/04) :print('Exercice a completer'), aucunraise) : support de Λ pour n ≤ 60, ψ(100) et l'écart au TNP, peser la deuxième onde.Sheydvasser, vendoreddifferential_lean/.lake/packages/mathlib/) :VonMangoldt.leanl.65/73/89/102/119 (vonMangoldt_mul_zeta: Λ * ζ = log — l'identité derrière la formule explicite),PrimeCounting.leanl.57 ; absents du pin :chebyshevPsiet la formule explicite (seule occurrence « explicit formula » : un commentaireZetaValues.leanl.269 sur une formule de Fourier différente) — le ψ du carnet est calculé, pas formalisé, et le dit.Validation
execution_count1-15, 0 erreur, 2 figures embarquées (display_data). Commit unique42ec345526, relance post-dernier-modification.grep -cE "raise NotImplementedError|assert False|1/0"→ 0.prose-counts: aucune ligne de compte ajoutée (la ligne README 02 décrit le carnet, aucun total touché).zetazero), exception déclarée au README de la série ; les sorties committées sont ses vraies sorties.MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/02-formule-explicite.ipynb(créé, 40 cellules) ·MyIA.AI.Notebooks/SymbolicAI/Lean/Riemann200/README.md(modifié : ligne 02). Aucun fichier.github/workflows/**.🤖 Generated with Claude Code