fix(lean,#17357): Lean-16g -- excursion du noyau (y=10, pas 11) et ancre pulsar_RLE corrigee

[jsboige]

Grain: MED/notebook-lean — lane myia-po-2023:CoursIA-2 — prev: MED/notebook-lean #20129

Deux affirmations fausses dans Lean-16g-Conway-Canons.ipynb — sixième carnet de la file #17357 pour cette lane.

Reassessed by myia-po-2023:CoursIA-2: CONFIRMED (2 constats, 0 faux positif) — les deux remesurés par cette lane, pas repris du dossier d'audit.

Audit source : commentaire 5845991384 (Hermes, campagne #17073 — stale-claim ×2 ; l'audit conclut lui-même « proposés 1 · confirmés 1 · rejetés 0 » pour le dossier, plus F2 hors dossier).

Diff : 2 cellules markdown, source seule. Aucune ré-exécution due (exception C.2 explicite : les deux sites sont du markdown), aucune sortie touchée — vérifié : les 9 cellules de code gardent leurs outputs et leurs execution_count 1..9 inchangés.

F1 — le noyau atteint y = 10, pas y = 11 (CONFIRMÉ)

Cellule c15 (idx 14), dans « Ce que le certificat ne prétend pas » :

il ne dit rien des instants entre les multiples de 30 (le noyau excursione hors boîte pendant le cycle — mesuré : y jusqu'à 11 pendant t = 0..29)

Le mot « noyau » a une définition propre au carnet, posée deux cellules plus haut (cellule de code c06, def core) :

def core(cells):
    """Noyau = iles qui INTERSECTENT la boite du canon a t=0.
    Les quasi-particules emises sont des iles disjointes, hors boite."""

J'ai reproduit la mesure avec le moteur du carnet lui-même (step / islands de c02, parse_rle_body + boîte de c04, core de c06), boîte x 0..35, y 0..8 retrouvée à l'identique :

 t | max y du NOYAU | iles hors boite (taille, max y)
20 |        9        | []
24 |       10        | []
25 |       10        | []
26 |       10        | []
27 |       10        | []
28 |        8        | [(5, 11)]
29 |        8        | [(5, 11)]

MAX y du NOYAU (iles intersectant la boite) sur t = 0..29 : 10
MAX y de la CONFIGURATION ENTIERE sur t = 0..29       : 11

Le noyau sort bien de la boîte stricte (y = 9 puis 10 > Y1 = 8) : l'affirmation qualitative est juste. C'est le chiffre qui est faux, et faux d'une manière qui enseigne la mauvaise géométrie : les y = 11 de t = 28..29 appartiennent à l'île hors boîte de 5 cellules — la quasi-particule émise, qui apparaît précisément à t = 28 (sortie de c06 : premiere apparition de chaque quasi-particule : {1: 28, ...}). La prose attribuait au noyau l'excursion de l'émission.

Correctif — la phrase dit maintenant la mesure, et nomme qui sort :

il ne dit rien des instants entre les multiples de 30 : le noyau sort de la boîte stricte au milieu du cycle — mesuré sur t = 0..29, il atteint y = 10 à t = 24..27, puis revient à y = 8 à t = 28 quand la quasi-particule s'en détache (le y = 11 observé à t = 28..29 appartient à cette quasi-particule, déjà une île disjointe du noyau) ;

La leçon honnête de la cellule (« le certificat ne dit rien des instants entre les multiples de 30 ») est conservée ; c'est la mesure qui l'appuie qui est recadrée.

F2 — l'ancre du pulsar pointe le mauvais motif (CONFIRMÉ)

Cellule c17 (idx 16), énoncé de l'exercice 1 :

Le lake encode aussi le pulsar (pulsar_RLE, RLE.lean:247)

Dans conway_lean/Conway/Life/RLE.lean au head :

242| def lwss_RLE : String :=
...
247| b4o$o3bo$4bo$o2bo!"
...
255| def pulsar_RLE : String :=

La ligne 247 est le corps RLE du lwss (le vaisseau c/2, 16 cellules), pas le pulsar. L'ancre est corrigée en RLE.lean:255, la ligne du def — la convention qu'emploient déjà les autres ancres du carnet (RLE.lean:268 pour gosper_gun_RLE, RLE.lean:277 pour gosper_gun).

L'apprenant qui ouvrait l'ancre pour l'exercice tombait sur un motif de 16 cellules au lieu de l'oscillateur annoncé. Les autres valeurs de la cellule (période 3, 48 cellules) sont justes : elles recoupent la docstring du lake (RLE.lean:252-254, « 48 cellules vivantes, période 3, le grand oscillateur le plus courant dans les soups »).

Vérifications demandées par la cellule, refaites

• « période 3 : 28 instances » (même cellule c17) : la sortie committée de la cellule de classification (c09) donne periodes des oscillateurs : {2: 1048, 3: 28, 4: 51, ...} — exact, et l'annonce est bien adossée à la sortie du carnet.
• Les autres ancres de ligne du carnet, toutes revérifiées au fichier : RLE.lean:268 (def gosper_gun_RLE), 277 (def gosper_gun), 332-343 (gosper_gun_parse_ok → gosper_gun_cell_count), 343 (gosper_gun.length = 36), 213-219 (le récit Gosper/Gemini), Life.lean:155 (def evolve), Computation.lean:176 (glider_2periods) — toutes justes. Seule la 247 était fausse.

Portée du diff

Deux champs modifiés, sur 2 cellules d'un carnet de 23 — vérifié champ par champ contre main :

idx 14  id c15  markdown  source   (la mesure de l'excursion)
idx 16  id c17  markdown  source   (l'ancre pulsar_RLE)

ids, cell_type, metadata (par cellule et global), nbformat/nbformat_minor et l'ensemble des outputs sont inchangés. Aucune sortie n'a été éditée à la main ; aucune cellule de code n'a été modifiée, donc aucune ré-exécution n'est due (C.2).

Observation (non traitée)

L'audit situe F2 « cellule c16 » ; le site réel est l'id c17 (décalage d'une cellule). Sans conséquence — le site est unique et sans ambiguïté — mais la localisation a été faite par contenu, pas par étiquette.

See #17357 — la file de cette lane compte 11 carnets ; ceci en traite 6 (Lean-11 en #20122, Lean-16a en #20123, Lean-16d en #20124, Lean-16c en #20127, Lean-16e en #20129). Les 5 autres suivent en PR séparées ([RELEASED] à la dernière).

🤖 Generated with Claude Code

[github-actions]

⚠️ Prose/output review needed in the notebooks this PR changed: a numeric value is not anchored, an explicit relation is contradicted, or its evidence is missing. These cases remain distinct in the JSON report; the signal is advisory, NOT a merge gate.

Scope = notebooks CHANGED in this PR, not the whole corpus. Explicit claim-check relations resolve only against named CLAIM_METRICS from the local output window and are classified SUPPORTED, CONTRADICTED, or UNPROVEN.
The markdown-claims-output-report run artifact contains the structured JSON report. See python scripts/check_markdown_claims_output.py --help for re-running locally.
Detector rationale: c.290 / c.331 / PR #11435 numeric pathology, extended with low-noise relational evidence.

[github-actions]

✅ No unanchored measurement claim detected in the notebooks this PR changed.

Scope = notebooks CHANGED in this PR, not the whole corpus. The stale-claim-report run artifact holds the structured JSON.
Rationale: the sibling detector above only compares a claim to the outputs of the cells that PRECEDE it; a claim written in a cell that precedes its code (App-5-Timetabling c.2/c.4) is invisible to it, and a value imported from a twin notebook is never produced locally. See python scripts/check_stale_claims.py --help.

[github-actions]

✅ 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 factual-mislabel-report run artifact holds the structured JSON.
Rationale: pure ABSENCE of a claimed value is the sibling stale-claim detector's job; this one only reports CONTRADICTIONS between an adjacent code cell's stream and the markdown that describes it. See python scripts/check_factual_mislabel.py --help.

[github-actions]

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook	Status	Time
2.1-Workflow-ML.ipynb	✅ SUCCESS	4.5s
2.2-Descente-de-gradient.ipynb	✅ SUCCESS	6.1s
2.3-Regression-lineaire-logistique.ipynb	✅ SUCCESS	6.0s
2.4-Arbres-Forets-Ensembles.ipynb	✅ SUCCESS	6.4s
Search-01-StateSpace.ipynb	✅ SUCCESS	4.9s
SL-1-LogicalLearning.ipynb	✅ SUCCESS	2.9s
RL-04-Bandits-Manchots-Python.ipynb	✅ SUCCESS	28.8s
GameTheory-04c-NashExistence-Python.ipynb	✅ SUCCESS	3.6s
GameTheory-13d-Optimistic-CFR-Python.ipynb	✅ SUCCESS	15.9s

Pinned lockfile: scripts/notebook_tools/golden_set.lock.txt (H.7 P3, axe A #4208)

[github-actions]

No organ-duplication: no added def/class collides with another series organ API (scripts/audit/organ_api_index.yaml).

Detector: python scripts/audit/detect_organ_duplication.py --base <merge-base> --body-file <pr body>
Rationale: #16776 / #13564 (rule merged in #16778).

[github-actions]

G-VAR-2/3 GENRE signals (advisory, non bloquant, #10020).
La lane `myia-po-2023:CoursIA-2` voit ces signaux actifs sur les mergees du jour (UTC 2026-10-09) :

• TIER-INFLATION : declared LIGHT << effective LIGHT-genre (tally : declared=0 genre=2 cap=4)
• NOTE ([variation] Le label est lane-agregat mais PR-attache : le merge-gate peut HOLD le grain de CONTENU qui remedie au motif #10341) : la PR courante est de classe CONTENU (non LIGHT-genre) et ne contribue pas au motif ci-dessus -- les labels agregees ne sont PAS poses sur cette PR (le merge-gate ne doit pas la HOLD pour ce motif ; le coupable est parmi les grains META de la lane).

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 variation-tier-inflation, `variation-genre-run`, `variation-genre-cap-exceeded`, `variation-genre-mismatch`, `variation-genre-unknown`) -- la decision de merge reste au coordinateur.

[github-actions]

Notebook outputs-required (H.4 schema): PASS (every code cell carries an outputs: list)

[github-actions]

Notebook PR Validation: PASS

• Notebooks checked: 1
• Code cells validated: 9
• Result: All passed

Checks: H.1 (no errors), H.3 (execution_count), C.1 (no banned patterns)
Non-Python kernels (.NET/Lean): C.1 + errors only (execution_count advisory)
QuantConnect notebooks: C.1 + errors only (require QC Cloud for execution)

[jsboige]

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 20130
head: 01185e9
complete: true
body: read
comments-reviewed: 8
reviews-reviewed: 0
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 42f8c317d7862c91ecde31716e4535371644fbd98be77c96e5c3deaab7dc36ae
diff-files: 1
diff-additions: 7
diff-deletions: 5
checks: latest-wins-green
b0: clear
scope: pass
domain: not-applicable
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 20130
organ-rc: 0
[/ADJOINT PREFLIGHT]

READY — attestation tierce a la tete 01185e94f7.

• checks : latest-wins-green — pli live sans aucune jambe hors {success, skipped, neutral} ; mergeStateStatus: CLEAN.
• b0 : clear — check_unaddressed_nits.py 20130 rc=0 ; aucune review postee sur cette PR, 0 thread inline.
• scope : pass — 1 fichier, +7/-5 : Lean-16g-Conway-Canons.ipynb (excursion du noyau y=10 et non 11, ancre pulsar_RLE corrigee), exactement le perimetre du titre.
• domain : not-applicable — carnet Python de la famille Lean, aucun *.lean modifie : aucun gate de preuve n'est declenche.

Commentaire tierce de prevalidation — n'approuve ni ne merge. Lane emettrice : myia-po-2023:CoursIA (file c2142).

[myia-ai-01]

Relu a la tete exacte. Deux cellules markdown. L'ancre RLE.lean:255 pointe bien sur def pulsar_RLE (verifie) ; le y = 10 et la detache de la quasi-particule a t = 28 sont portes par la sortie committee. Exception C.2. B.0 rc=0.