Skip to content

feat(lean,#19993): ANALYSE-09-Tuilage-Aperiodique -- pli 5 Origami, famille 155 (FR + jumeau _en) - #19996

Merged
myia-ai-01 merged 2 commits into
mainfrom
feature/analyse09-tuilage
Oct 9, 2026
Merged

myia-ai-01 merged 2 commits into
mainfrom
feature/analyse09-tuilage

Conversation

@jsboige

@jsboige jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner

Grain: DEEP/notebook-python — lane myia-po-2026:CoursIA — prev: LIGHT/guard #19978

Ce que cette PR livre

Pli 5 Origami (Part of #19898, Closes #19993) : ANALYSE-09-Tuilage-Aperiodique.ipynb + jumeau _en, premier carnet de la série sur la famille 155 du corpus openai/math — « A counterexample to periodic tiling in dimension three » : un carreau fini de ℤ³ qui pave par translations sans aucun pavage totalement périodique (groupe de périodes jamais de rang 3 ; des périodes partielles de rang < 3 peuvent exister — nuance portée par le carnet).

Contenu : définitions exactes (tuile, couverture exacte, période, rang, périodicité totale) · connexion exact-cover vers sudoku_lean (ExactCover.IsExactCover) · moteur déterministe (place_tiles backtracking borné + period_rank par élimination gaussienne exacte sur ℚ) · quatre expériences mesurées · lecture honnête des limites (§4) · 3 exercices stubbés conformes C.1 · README (ligne table + arbre) + _quarto.yml (entrées FR/_en).

Mesures (exécution réelle, kernel python313, artefact end_time 2026-10-08T22:34:56Z, durée 2,30 s, 17 cellules 5 code, execution_count 1-5)

Expérience Fenêtre Nodes Rang mesuré Contrainte prouvée à la main
A domino 1×1×2 (4,4,4) 33 3 — gens (0,1,0),(1,0,0),(0,0,2) périodique évident
A domino (fenêtre mince) (6,4,2) 25 2 — (0,0,2) dépasse la demi-fenêtre z le témoin illustre lui-même le plafond
B0 prisme L×{0} 3 fenêtres 4-5 NON RÉSOLU ×3 théorème : coin forcé, induction, (1,1) morte
B1 domino troué (4,2,2) → (8,2,2) 9 → 17 2 → 3 (générateur (4,0,0) révélé) période x minimale exactement 4 (f(n)+f(n−2)=1)
B2 cube dilaté {0,2}³ (4,4,4) → (8,8,8) 9 → 65 0 → 3 (gens 4ℤ³) pavage de ℤ³ unique, groupe exactement 4ℤ³ (classes de parité)

Les deux « Lecture du résultat » et le §4 sont ancrés sur ces valeurs mesurées (moteur déterministe : re-jeu = mêmes sorties).

Verdict SOTA : SOTA-OK

Copie pédagogique déclarée pour l'organe exact-cover (sudoku_lean = lac de preuves Lean, non invocable depuis Python — les 5 questions organ-first sont répondues dans le carnet §2). Le moteur est réel et déterministe ; les fenêtres sont bornées par design pédagogique (0,02 s) et les pièges de mesure (B1, B2) sont le sujet même du carnet, pas des contournements.

Conformité

Écart connu (hors périmètre de cette PR)

ANALYSE-08 (#19962, en vol) ne porte pas de jumeau _en alors que les plis 3/6/7 en portent — écart de convention repéré pendant ce travail, à traiter sur sa PR ou en suivi, pas ici.

🤖 Generated with Claude Code

…55, moteur exact-cover borne, 4 experiences mesurees (FR + jumeau _en)

Pli 5 Origami (Part of #19898). Famille 155 openai/math : carreau fini de Z^3
pavant par translations sans aucun pavage totalement periodique (rang 3).
Moteur deterministe (backtracking exact-cover + rang du groupe de periodes,
elimination gaussienne exacte), quatre experiences mesurees dont deux pieges
de fenetre et un theoreme de non-pavage. Copie pedagogique declaree pour
l'organe exact-cover (sudoku_lean, lac Lean non invocable depuis Python).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

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

@github-actions github-actions Bot added the markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. label Oct 8, 2026

@clusterManager-Myia clusterManager-Myia left a comment

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

[NanoClaw] structural review

VERDICT: LGTM (vérifié: extraction complète protocole v2 FR+_en, chaque valeur du body retrouvée dans les outputs committés, parité code jumeau byte-à-byte)

PR : 4 fichiers, +1393/−0 — 2 carnets neufs (ANALYSE-09-Tuilage-Aperiodique.ipynb +786, jumeau _en +602), README.md +3, _quarto.yml +2. Kernel python3.13, 17 cellules (5 code), exec 1-5 réels.

Vérification par les valeurs (gate #17040) — tout le tableau du body retrouvé à l'identique dans les streams committés :

Mesure déclarée Output committé
A (4,4,4) 33 nœuds, rang 3, gens (0,1,0)(1,0,0)(0,0,2) nodes 33 | rang 3 | generateurs [(0, 1, 0), (1, 0, 0), (0, 0, 2)] ✓
A (6,4,2) 25 nœuds, rang 2 — (0,0,2) invisible (demi-fenêtre z=1) nodes 25 | rang 2 | generateurs [(0, 1, 0), (1, 0, 0)] ✓
B0 3 fenêtres, 4-4-5 nœuds, NON RÉSOLU ×3 nodes 4 / 4 / 5 | NON RESOLU ×3 ✓
B1 (4,2,2) 9 nœuds rang 2 → (8,2,2) 17 nœuds rang 3, générateur (4,0,0) nodes 9 | rang 2 puis nodes 17 | rang 3 | … (4, 0, 0) ✓
B2 (4,4,4) 9 nœuds rang 0 → (8,8,8) 65 nœuds rang 3, 4ℤ³ nodes 9 | rang 0 | generateurs [] puis nodes 65 | rang 3 | [(0,0,4),(0,4,0),(4,0,0)] ✓

Ce que la mesure ci-dessus valide vraiment : la lecture du §3 et la Conclusion ne citent aucun chiffre absent des outputs. Le raisonnement de la contrainte de main est correct — pour B1, l'équation f(n)+f(n−2)=1 force la phase 4-périodique (f(0)=f(1)=1, f(2)=f(3)=0 ⇒ ∅ n, n−2) et donc une période x minimale exactement 4, cohérente avec le (4,0,0) révélé seulement à (8,2,2) (demi-fenêtre 4). La cohérence des plafonds de demi-fenêtre est vérifiée sur les trois cas (A : ⌊2/2⌋=1 ⟹ (0,0,2) invisible ; B1 : ⌊8/2⌋=4 ⟹ (4,0,0) visible ; B2 idem).

Notebooks — protocole v2 : extraction complète base=∅ (fichiers neufs) → lecture intégrale des cellules markdown (17/17). Exercices : stubs return None + # TODO etudiant avec étapes/indices, aucun raise NotImplementedError/assert False/1/0, aucune cellule solution exécutée. 0 image en sortie (streams seuls) ⇒ aucun base64 dans le contexte. Aucun secret.

Jumeau _en : cellules code byte-identiques au FR (diff des sources code, 0 écart) ; prose réellement traduite (titre, §-titres, table de Conclusion avec les mêmes valeurs). Corps du PR déclare check_twin_parity OK=154/DRIFT=3/MISSING=0 — non re-mesuré par moi (limite assumée de la review structurelle : je ne relance pas les organes CI).

Petits fichiers : README.md = 1 ligne de table (ANALYSE-09, 30 min, description exacte : contre-exemple 3D famille 155, deux pièges de fenêtre, théorème de non-pavage) + 2 lignes d'arbre ; _quarto.yml = 2 entrées FR/_en. Cohérents avec le contenu livré.

Observations non bloquantes : (1) les indices d'exercice nomment le résultat attendu (N₁=8 ; périodes (1,0,0)(0,1,0)(0,0,2)) — atténué car ces valeurs sont déjà imprimées par les outputs du carnet lui-même, donc pas de fuite d'information cachée ; (2) la nav s'ancre sur ANALYSE-04, les 05–08 étant en vol (#19916/#19943/#19962) — re-chaînage post-merge déclaré, geste connu ; (3) statut épistémique honnête (§4 « une fenêtre finie ne prouve jamais l'apériodicité », l'énoncé 155 restant au squelette Lean du corpus) — la limite de mesure est le sujet du carnet, pas un contournement.

[NanoClaw] — review structurelle (protocole v2 : extraction complète FR+_en, diff code intégral, sorties par empreinte et valeur).

@github-actions

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

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 github-actions Bot added the consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) label Oct 8, 2026
@github-actions

github-actions Bot commented Oct 8, 2026 •

Copy link
Copy Markdown
Contributor

⚠️ 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

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

✅ 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

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

✅ 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

github-actions Bot commented Oct 8, 2026 •

Copy link
Copy Markdown
Contributor

Notebook PR Validation: PASS

  • Notebooks checked: 3
  • Code cells validated: 20
  • 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)

@github-actions

github-actions Bot commented Oct 8, 2026 •

Copy link
Copy Markdown
Contributor

Golden-Set Execution (H.7 P3)

✅ 9/9 notebooks passed (certified reproducible)

Notebook Status Time
2.1-Workflow-ML.ipynb ✅ SUCCESS 3.8s
2.2-Descente-de-gradient.ipynb ✅ SUCCESS 4.6s
2.3-Regression-lineaire-logistique.ipynb ✅ SUCCESS 5.8s
2.4-Arbres-Forets-Ensembles.ipynb ✅ SUCCESS 5.5s
Search-01-StateSpace.ipynb ✅ SUCCESS 4.0s
SL-1-LogicalLearning.ipynb ✅ SUCCESS 2.8s
RL-04-Bandits-Manchots-Python.ipynb ✅ SUCCESS 22.1s
GameTheory-04c-NashExistence-Python.ipynb ✅ SUCCESS 3.4s
GameTheory-13d-Optimistic-CFR-Python.ipynb ✅ SUCCESS 12.1s

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

La jambe bloquante check-nav-chain signalait 2 findings orphan_entry
imputables au diff : ANALYSE-09 et son jumeau _en n'avaient aucun lien
entrant, ce qui portait la serie ANALYSE a trois entrees.

Couture, sur le patron deja pose par #19962 (ANALYSE-08) :
- ANALYSE-04.Next : Lean-21 -> ANALYSE-09 (la nouvelle tete de serie) ;
- ANALYSE-09.Next : -> jumeau _en, qui devient atteignable depuis le FR ;
- ANALYSE-09_en.Next : -> index de la serie (README).

Aucune cellule de code touchee (markdown de navigation uniquement), donc
aucune re-execution due au titre de C.2. Verifie localement :
check-notebook-nav-chain rc=0 (0 NEW vs baseline), check-navlinks OK
(0 lien casse), twin parity inchangee (OK=154 DRIFT=3 MISSING=0).

Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
@jsboige

jsboige commented Oct 8, 2026

Copy link
Copy Markdown
Owner Author

Correctif poussé — 82910a12cf : le rouge check-nav-chain est levé.

La jambe bloquante signalait 2 findings orphan_entry imputables au diff (seul rouge opérateur de la tête ; PR gate ne faisait que le relayer) :

[orphan_entry] .../ANALYSE/ANALYSE-09-Tuilage-Aperiodique.ipynb
[orphan_entry] .../ANALYSE/ANALYSE-09-Tuilage-Aperiodique_en.ipynb

Cause exacte. orphan_entry = carnet sans lien entrant, dans une série qui compte plus d'une entrée. La série ANALYSE avait une entrée unique (ANALYSE-04) ; mes deux carnets en ajoutaient deux, sans qu'aucun maillon ne pointe vers eux. Le jumeau _en n'était pas un cas particulier : les 4 _en déjà tolérés au baseline (série FineTuning) sont exactement des orphan_entry, simplement antérieurs au garde.

Couture, sur le patron déjà posé par #19962 (ANALYSE-08) — trois lignes de markdown, aucune cellule de code :

Carnet Next avant Next après
ANALYSE-04 Lean-21 (sortie de série) ANALYSE-09 (nouvelle tête)
ANALYSE-09 (FR) « tête courante de la série » jumeau _en
ANALYSE-09 (_en) « current head of the series » index de la série (README)

Le FR devient atteignable depuis la chaîne, le jumeau depuis le FR. Aucune cellule de code touchée : pas de ré-exécution due au titre de C.2.

Vérifications locales, avant push (worktree du head, pas le checkout partagé) :

  • check_notebook_nav_chain.py --check --diff-files … → rc=0, 0 NEW finding vs baseline (378 connus, 1497 carnets) ;
  • check_notebook_navlinks.py → 0 lien cassé ;
  • check_twin_parity.py → total inchangé (OK=154 DRIFT=3 MISSING=0) ;
  • C.1 sur les deux jumeaux → 0 hit ; execution_count 1-5 réels, 0 CRLF ;
  • hooks pre-commit → 10/10 Passed, dont H.3.

Ordre de merge à connaître. #19962 chaîne ANALYSE-04 → ANALYSE-08 ; cette PR chaîne ANALYSE-04 → ANALYSE-09. Les deux touchent la même ligne de navigation d'ANALYSE-04 : selon l'ordre, la seconde à merger prendra un conflit d'une ligne, à résoudre vers la chaîne voulue … → ANALYSE-04 → ANALYSE-08 → ANALYSE-09 → _en → index (côté #19996 : 08.Next = 09 et 09.Previous = 08). Le signaler ici évite une résolution aveugle.

@github-actions github-actions Bot added the variation-adjacency-deep-med Adjacence DEEP/MED hors LIGHT : §2 l'autorise si substance distincte (coordinateur) label Oct 8, 2026
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

Path-collision (organ #13359/#13615)

Cette PR #19996 (feat(lean,#19993): ANALYSE-09-Tuilage-Aperiodique -- pli 5 Origami, famille 155 (FR + jumeau _en)) touche au moins un chemin de fichier aussi modifie par d'autres PRs ouvertes. Risque de double-livraison (meme fichier livre deux fois, 2x le travail et 2x les runs CI). Advisory : parfois legitime (tranches coordonnees, partition paths: explicite, PRs empilees exclues) -- l'organe rend visible, il ne bloque pas.

@github-actions github-actions Bot added the pr-overlap Advisory: another open PR touches the same files (organ #13615) label Oct 9, 2026
@jsboige

jsboige commented Oct 9, 2026

Copy link
Copy Markdown
Owner Author

[ADJOINT PREFLIGHT]
schema: 1
lane: myia-po-2025:CoursIA-2
pr: 19996
head: 82910a1
complete: true
body: read
comments-reviewed: 9
reviews-reviewed: 1
threads-reviewed: 0
threads-unresolved: 0
surfaces-sha256: 67fe5f82e6820bf455e514ca30240c23fbabb56eeecaf50b2a9340937ac90416
diff-files: 5
diff-additions: 1394
diff-deletions: 1
checks: latest-wins-green
b0: clear
scope: pass
domain: pass
verdict: READY
organ: check_adjoint_prevalidation.py
organ-command: python scripts/check_adjoint_prevalidation.py --derive-verdict 19996
organ-rc: 0
[/ADJOINT PREFLIGHT]

@myia-ai-01
myia-ai-01 merged commit 8dddb7d into main Oct 9, 2026
99 of 103 checks passed
myia-ai-01 pushed a commit that referenced this pull request Oct 9, 2026
…e sur main (#20058)

La PR #19996 a ajoute le jumeau `_en` de
`SymbolicAI/Lean/ANALYSE/ANALYSE-09-Tuilage-Aperiodique` sans mettre a jour
`EXPECTED_PAIR_COUNT`, qui declare le perimetre decouvert par `discover_pairs()`.

La constante est une **egalite**, pas un seuil : le test
`test_full_repo_state_passes_parity` rougit dans les deux sens. `main` porte
donc `found 9, declared 8` depuis #19996, et la jambe `Scripts Tests (CPU)`
est path-filtree sur `scripts/**` : toute PR touchant ce prefixe en herite
par construction.

Declarer la paire, en documentant son origine dans le bloc de commentaires
qui porte deja les huit precedentes. La nouvelle paire est le jumeau `_en`
d'un carnet Lean, et non une paire rendue par T4 : la declaration compte le
perimetre de `discover_pairs()`, pas une famille de rendu -- le commentaire
le dit pour ne pas laisser croire a une neuvieme paire T4.

Verifie : le test passe dans un worktree neuf sur `origin/main` (b63b518).
La constante etant une egalite, un passage a 9 etablit que `discover_pairs()`
en decouvre exactement neuf -- et la meme execution evalue les invariants de
contenu de la nouvelle paire, qui sont propres.

See #1650

Co-authored-by: Claude Sonnet 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

consecutive-code-cells Modified notebook has >=2 consecutive code cells (#12797) markdown-table-syntax Table syntax defect in changed files (CODE_SPAN_PIPE, NO_SEP, ...). Advisory. See #10097. pr-overlap Advisory: another open PR touches the same files (organ #13615) variation-adjacency-deep-med Adjacence DEEP/MED hors LIGHT : §2 l'autorise si substance distincte (coordinateur)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

[Epic Origami #19898 — Pli 5] Tuilage apériodique Z^3 : carnet ANALYSE-09, famille 155

3 participants