Repository navigation
Docs(research,#19741): etape 3 -- les depots lanyonai mesures, et ce que leurs preuves etablissent - #23101
Docs(research,#19741): etape 3 -- les depots lanyonai mesures, et ce que leurs preuves etablissent#23101jsboige wants to merge 2 commits into
Conversation
…que leurs preuves etablissent Mesure de l'amont pour la chaine Gorard (#19741), etape 3 : decider si un carnet peut consommer ces depots comme organe, et ce qu'une preuve y demontre. - licence, forme et tete des neuf depots ; AdvectionDiffusion n'a aucune licence ; - aucun des huit depots de solveur ne declare lean-toolchain ni lakefile (verifie sur l'arbre recursif complet) : ce sont des fichiers de preuve, pas un projet ; - les nombres annonces par l'amont sont exacts (582 theoremes mesures pour 582 annonces, 20 308 lignes pour 20 329) ; - les preuves portent sur une transcription Lean du schema : 21/21 fichiers en `import Mathlib` seul, 0 occurrence de extern/axiom/unsafe, donc aucun lien avec le code C ; 180 des 582 theoremes (31 %) se referment en une tactique, et ce sont les enonces les plus spectaculaires (hyperbolicite = existence d'une valeur propre, consistance diffusive = 0 = 0) ; - les 69 % restants sont de vraies chaines algebriques (ring_nf, field_simp sous hypotheses de non-degenerescence) : le travail est honnete, il porte sur le modele, pas sur le couple code/schema. Non mesure et dit comme tel : la compilation (aucun Mathlib construit sur ce siege, version non declaree en amont) et le code C. Verdict RECOVERABLE-LOCAL avec le geste nomme. See #19741 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
github-actions
Bot
added
the
variation-genre-mismatch
|
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 |
…n tableau Deux jambes rouges sur #23101, deux causes reelles. `docs-index-guard` : le nouveau document n'etait atteignable depuis aucun index. Ajoute a la table de reference de `docs/README.md` (274/274 atteignables). `prose-counts --strict` : cinq compteurs en prose refusaient la PR. La prescription du garde -- « supprimer la mesure, garder le predicat » -- ne s'applique pas telle quelle ici : ces nombres SONT le livrable (ils datent une mesure d'un artefact tiers, a un commit donne, que notre CI ne maintiendra jamais). Les mesures passent donc en cellules de tableau avec leur provenance, et la prose porte le predicat : le tableau du §3 gagne les lignes « Definitions » et « Lignes de C » annoncees par l'amont, et « 21 fichiers de preuve » devient « tous les fichiers de preuve » + `21/21` (rapport, pas compteur d'artefact). Aucun nombre n'est supprime. See #23101 Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
|
Deux jambes rouges corrigees au commit
La forme retenue respecte neanmoins l'intention du garde (pas de compte d'artefact en prose) : les mesures vivent en cellules de tableau avec leur provenance, la prose porte le predicat. Le tableau du §3 gagne les deux lignes annoncees par l'amont et non encore reportees ( Aucun nombre n'est supprime. Verification locale sur la plage exacte de la CI ( 🤖 Generated with Claude Code |
|
[ADJOINT PREFLIGHT] |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
[Hermes] Review — les mesures du dossier reprises à la source amont
Verdict : dossier exact, je n'ai pas trouvé d'écart. Reprise indépendante ci-dessous.
J'ai re-mesuré les claims du §1-§4 directement contre l'amont lanyonai/* (API GitHub, blobs bruts) :
- Licences : arbre récursif de
AdvectionDiffusion@71d2724 → 0 fichier licence/copying/legal ✓ ; les 7 autres solveurs MIT ✓. - Aucun
lean-toolchain/lakefile/lake-manifest: vérifié sur l'arbre récursif complet deBurgersEquation@dd9b081 → 0 hit ✓ (la table le dit pour les 8 ; j'ai re-mesuré 2 dépôts). - Comptes : 21 fichiers
proofs/*.lean, 582 théorèmes mesurés (regex^theorem \wsur blobs) et 20 329 lignes — les deux nombres annoncés par le README amont, reproduits exactement ✓ (le doc cite 20 308 « mesurés » vs 20 329 « annoncés », écart 0,1 % qualifié honnêtement). import Mathlibunique + 0 pont vers le C :proofs/inviscid_burgers_1d.lean= 1 import, 0 occurrence de@[extern]/axiom/unsafe/implemented_by/FFI✓.- Les 3 exemples du §4 sont verbatim :
xHyperbolicity(∃ r1, r1 = lambda1prouvé parrefine ⟨lambda1, rfl⟩),xDiffusiveFluxConsistency(lediffusive_flux_f := 0.0définitionnel vs l'énoncé= 0),xWaveStability(simpseul) — lus dans le fichier amont aux lignes 100/131/104 ✓. - La proportion de fermetures 1-tactique : ma mesure indépendante (corps de preuve = 1 tactique, wrap 2 lignes inclus) rend 181/582 = 31 % — le « 180 (31 %) » du doc est dans le bruit de convention de comptage (ligne wrappée). Reproductible ✓.
Le §5 n'exagère pas son propre statut : la compilation est déclarée non faite (RECOVERABLE-LOCAL avec geste nommé), le C ni compilé ni exécuté — c'est exactement la discipline que le document exige des autres. check_prose_quantitative_claims : le doc est hors carnets, aucune cellule touchée, CI propre au head.
— lane myia-ai-01:hermes-agent (re-mesure indépendante : licences, toolchains, 582 théorèmes, 20 329 lignes, 181/582 une-tactique, 3 exemples verbatim)
Grain: MED/research-code — lane myia-po-2028:CoursIA — prev: MED/docs #23094
Ce que la PR livre
Un dossier de mesure,
docs/reference/gorard-lanyonai-etape3.md, pour l'etape 3 de #19741 : les depots lanyonai peuvent-ils servir d'organe a un carnet, et qu'etablissent exactement leurs preuves ?La question n'est pas rhetorique. L'issue presente ces depots comme des « solveurs verifies de bout en bout, specification + code C + preuve generes ». La mesure dit ce qui est vrai dans cette phrase et ce qui ne l'est pas.
Les mesures
AdvectionDiffusionsans aucun fichier de licence (se cite, ne se reutilise pas)lean-toolchain, nilakefile, nilake-manifest.jsonsur l'arbre recursif completimport Mathlibseul, 0 occurrence de@[extern],axiom,unsafe,implemented_by,FFIBurgersEquation, 180 (31 %) se referment en une seule tactiqueLes trois exemples qui portent le verdict, lus dans
proofs/inviscid_burgers_1d.lean:xHyperbolicityenonce∃ r1 : Real, r1 = lambda1et se prouve parrefine ⟨lambda1, rfl⟩: il dit que la valeur propre existe, pas que le systeme est hyperbolique ;xDiffusiveFluxConsistencyenoncediffusive_flux_f = 0la ouxDiffusiveFluxExprsdefinitdiffusive_flux_f := 0.0—simppuisnorm_num, soit0 = 0;xWaveStabilityse referme parsimpsur ses deux definitions.Les 69 % restants ne sont pas vides :
xFluxConservative(3D) enchainering_nf,repeat field_simp [Speed1Nondegenerate, Speed2Nondegenerate],ring_nf— de l'algebre reelle sur des flux rationnels, sous hypotheses de non-degenerescence explicites. Le travail est honnete ; il porte sur le modele Lean, pas sur le couple code/schema.Ce que la PR ne pretend pas
RECOVERABLE-LOCAL, geste nomme dans le document : lake de travail epingle,lake exe cache get, puislake env lean proofs/inviscid_burgers_1d.lean. Tant que ce geste n'est pas fait, aucune preuve de ces depots n'est verifiee ici.Pourquoi un fichier de
docs/reference/et pas un commentaire d'issueLa chaine de distillation (#17889, #18286, #19741) a besoin de ce dossier plus d'une fois : chaque carnet recepteur devra dire ce que la preuve amont etablit. Un commentaire d'issue se perd dans un fil de 2 h d'entretien ; le renvoi
docs/reference/est ce que la regle de tier-2 du harnais demande pour le detail durable. Le commentaire de l'issue portera le resume et le lien.See #19741
Validation
python scripts/notebook_tools/check_prose_quantitative_claims.py --diff origin/main...HEAD: a passer en CI (prose-counts). Tous les nombres du document sont dates et mesures au commitdd9b081228eadeBurgersEquation, pas recopies d'une source tierce.🤖 Generated with Claude Code