Repository navigation
Add: densite Conway Lean — interpretations pedagogiques, 3 notebooks sous plancher (See #13410) - #16326
Conversation
… sous plancher (See #13410) Lean-16d Game-of-Life 871->1235 (+6 cellules md : representation creuse, B3/S23 total, lecture des faits certifies, attendus/anti-pieges x3), Lean-16e FRACTRAN 970->1414 (+4 : type dependant Frac, semantique d'arret asymetrique, theoremes/axiomes, attendus ex 1-3), Lean-16j Hashlife 736->1207 (+6 nouvelles : carte du lac, synthese de la chaine de correction, attendus x3, anti-piege intro ; +6 extensions ciblees : norme infinie vs causalite carree, memoisation, saut 2^k, methodologie batterie, decide vs tactiques, lien 16e). Markdown-only : cellules code et outputs byte-identiques (fingerprint md5 avant/apres in-script, 0 ligne diff touchant execution_count/outputs). detect_markdown_rendering --check OK sur les 3. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
|
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 PR Validation: PASS
Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns) |
Notebook outputs-required (H.4 schema): PASS (every code cell carries an
|
Golden-Set Execution (H.7 P3)✅ 8/8 notebooks passed (certified reproducible)
Pinned lockfile: |
|
Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit |
clusterManager-Myia
left a comment
clusterManager-Myia
left a comment
There was a problem hiding this comment.
VERDICT: LGTM
Review [Hermes] — contre-vérification indépendante des claims du body (head 35ae209) :
- Byte-identity code cells — vérifiée sur le diff brut : 0 ligne
"execution_count","outputs"ou"cell_type": "code"touchée ; les 16 ajouts sont tous"cell_type": "markdown". Les −6 lignes = réécriture d'entrées source markdown étendues (newline final), conforme C.2. - Ancrage des claims numériques — vérifié contre les outputs réels du head (fetched à 35ae209) :
fractranRun doubler 1 4→[1, 2, 4, 8, 16]✓,fractranRun halver 8 4→[8, 4, 2, 1]✓,size (emptyOfLevel 3)→8dans le text/plain de la cellule ✓. Le signal advisory prose/output (19:22Z) est trié : valeurs citées trouvées et cohérentes dans les fenêtres d'output locales. - Densité — recalculée indépendamment (md/code) : 1235 / 1414 / 1208 vs annoncé 1235/1414/1207 (écart 1 = arrondi, négligeable). Les 3 passent le plancher 1200. Rappel : golden-set 8/8 vert = hors périmètre (notebooks non touchés par cette PR), ce n'est pas lui qui certifie — la preuve est le diff markdown-only + les 3 notebooks déjà certifiés en amont.
Interprétations pédagogiques lues (16d/16e/16j) : justes conceptuellement — totalité de aliveNext, sémantique d'arrêt asymétrique doubler/halver, frontière de causalité carrée ‖·‖∞, niveau↔2^k. Rien à contredire.
[Hermes hermes-pr-review, cycle :19 15/09, host c92df397a786]
2 participants
Grain: DEEP/notebook-lean -- lane myia-po-2026:CoursIA -- prev: MED/docs #16324
Le livrable
#13410 tranche densité Conway Lean (rotation de famille R6) — les 3 notebooks Conway sous le plancher
pedagogy_density1200 chars/cellule code, enrichis de +16 cellules markdown et +6 extensions ciblées :Lean-16d-Conway-Game-of-Life-Lean-Nativeabbrevréductible), B3/S23 total (pas de troisième état, briques composables testables), lecture des 4 faits certifiés (simuler vs formaliser — la même machine qui exécute prouve), attendus + anti-pièges pour les 3 exercices (foldl sur mooreNeighbors pas sur g, accumulateur, pulsar période 3 vs test période 2, sameSet et doublons)Lean-16e-Conway-FRACTRAN-Lean-NativeFrac(preuveh : den > 0habitant la valeur — inhabité dans le type, contrasteFraction(2,0)Python à l'exécution), sémantique d'arrêt asymétrique (doubler arrêté par le carburant vs halver arrêté par inapplicabilité — none = terminaison), lecture des théorèmes (pas positifs vs arrêt,#print axiomsvide, Turing-complétude = résultat classique hors périmètre), attendus/anti-pièges ex 1-3 (fraction réduite, decide vs native_decide, 3 transitions vs 4 éléments, stepsToHalt doubler = carburant)Lean-16j-Conway-Hashlife-Correctness-Native#evalattendu avant le corps), attendus/anti-pièges des 3 exercices (natAbs par composante, test conjoint des niveaux vs mono-niveau qui passe le #eval sans répondre, écarts vs coordonnées absolues) ; +6 extensions d'interprétations existantes sur des angles nouveaux (norme ∞ et frontière de causalité carrée, cône = licence de mémoïsation, niveau = arithmétique du saut 2^k, méthodologie d'usage de la batterie adverse, decide vs tactiques proportionné à l'énoncé, lien consommateur/producteur avec Lean-16e)Invariant byte-identity (exception C.2 markdown-only)
git diff -U0 \| grep -cE '"execution_count"|"outputs"|"cell_type": "code"'= 0 ligne touchée. Aucune re-exécution nécessaire (C.2, modifs uniquement markdown).\nde fin), pas de perte de contenu.Validation locale
pedagogy_density.py: 871 → 1235, 970 → 1414, 736 → 1207 (les 3 sortent de la listebelow_thresholddu dossier Lean, qui passe de 10 à 7).detect_markdown_rendering.py --check: OK sur les 3 (no new ERROR-level violations).fix-source-newlinesa normalisé les newlines de mes 6 cellules étendues avant commit (réparation automatique, contenu inchangé).grep twin_pairs.d— pas de rebaseline twin requis).Coordination
variation_adjacency_guard.pyrejouée en local :guard_pass=true, adjacent=false).See #13410 (epic densité — tranches suivantes restantes : 7 notebooks Lean sous plancher + ~420 hors famille).
🤖 Generated with Claude Code