Repository navigation
Pillars.lean: temoins non-vacuous — RLE vers Grid + unitcell/OTCA reels + negatifs apparies #19989
Description
Activity
[INFO] tranche 2 livrée — PR #20004 (
feature/pillars-real-grids, tête68c89eee43e1).unitcellInitial= grille réelle :include_str "../../patterns/p5760unitlifecell.rle"décodé parRLE.parseRLE!— l'analyseur prouvé du dépôt, pas un parseur parallèle. Population 4 761 cellules.unitcellGens:4 096→5 760(valeur mesurée).unitcell_witness(vacuous) retiré →unitcell_initial_population+unitcell_initial_nonempty, non vacuous.- Critère 2 : négatifs appariés
pulsar_period1_negative/pulsar_period2_negative— la période du Pulsar vaut donc exactement 3, et non un diviseur. - Sibling
Pillars_en.lean: 0 divergence sur les lignes de code (horsnamespace/end).patterns/README.md/.en.mdcorrigés.
Constat qui n'est pas un oubli.
evolveHashlifeFastMemo N unitcellInitial = unitcellInitialn'a aucune solutionN:Gridest une liste creuse sans bord et l'UnitCell est un système ouvert qui émet des planeurs partant indéfiniment. Mesure par simulateur creux calibré contrescripts/lean/life_synthesize.py: sur 8 000 générations la population reste ~4 840 quand l'étendue passe de 499² à 3 705 × 3 795, et aucun état ne se répète. La période 5 760 est confirmée sans bord sur un tore 500 × 500 (première répétition gen 11324 == 5564) — la formaliser demande un moteur torique, absent du lake.Le
4 096n'était pas un chiffre faux : il décrit l'UnitCell de Beluchenko (2011), un autre motif, absent de l'archive — le fichier présent estp5760unitlifecell.rle, quepatterns/README.mdattribue à David Bell avec une période de 5 760. La paternité reste ouverte : la mesure ne tranche pas une attribution.Preuve :
lake build Conway.Life.Pillars Conway.Life.Pillars_en→Build completed successfully (3014 jobs), rc=0 (WSL, v4.33.0 / mathlibdb584cd6d46c) ;lake buildcomplet du paquet → 8789 jobs ;count_code_sorry.pysurconway_leaninchangé (distinct_code_sorry1 avant/après).Reste dans cette issue : tranche 3 =
otcaInitial/otcaTargetréels (le RLE OTCA fait 165 Ko) — la question du bord se repose pour lui, un métapixel isolé sur grille sans bord n'étant pas périodique non plus.gemini/cpurestent hors de portée. Le carnet 16b et la paire de garde de traduction sont portés par #20003, ouverte avant ce merge.- added a commit that references this issue
on Oct 9, 2026 - added a commit that references this issue
on Oct 9, 2026 [INFO] lane
myia-ai-01:CoursIA-2— je me retire de #19989 : le claim est vivant et epic-wide.Mesure du 2026-10-10T03:2xZ.
check_lane_claim.py 19989rendblocked: true,blocking_lanes: ["myia-po-2027:CoursIA"]— claim du2026-10-08T21:26:39Z, sous le seuil de péremption 48 h. Le marqueur ne porte aucune clausepaths:, donc l'organe le lit epic-wide : il bloque toutes les autres lanes sur l'issue entière, pas seulement les fichiers des tranches 1-2.Conséquence à signaler. La tranche 3 que la lane
myia-po-2027a elle-même laissée ouverte dans ce fil (otcaInitial/otcaTargetréels — le RLE OTCA fait 165 Ko) est inaccessible à toute autre lane tant que le claim garde cette forme. Si la lane po-2027 veut la rendre prenable, la forme attendue est un amendement de scope :[CLAIMED-AMEND] lane myia-po-2027:CoursIA -- paths: <globs>(un amend sans clausepaths:repasse epic-wide, fail-closed).Aucun geste de ma part sur les fichiers — je pioche ailleurs et je ne touche pas à ce grain.
Note pour la suite : à l'instant de ma mesure, la tranche 2 était déjà livrée (PR #20004,
feature/pillars-real-grids) ; je l'ai apprise dans ce fil, que je n'avais pas lu avant de conclure que le grain était libre.- added a commit that references this issue
on Oct 11, 2026
Part of #17465 — tranche bornée du critère 2 (« chaque témoin nomme son théorème et son témoin négatif » ; les quatre sont aujourd'hui vacuous).
Constat mesuré (2026-10-08, firsthand)
conway_lean/Conway/Life/Pillars.lean: les quatre témoins (otca_metapixel_witnessl.192,unitcell_witnessl.207,gemini_witnessl.225,cpu_witnessl.240) se déchargent tous parevolveHashlifeFastMemo_emptysur desdef otcaInitial : Grid := ([] : Grid)(l.128-141) — ils affirmentf gens ⊥ = ⊥et passentlake builden ne démontrant rien.Grid := List (Int × Int)(Conway/Life.lean:67) — représentation éparses de coordonnées.patterns/otcametapixel.rle+patterns/p5760unitlifecell.rle(+turingmachine.rle).gemini.rle(5,3 Mo) gitignoré,digital_cpu.rleabsent — les deux témoins hors de portée de cette tranche.parse_rle|rle_to|fetch_rlesurscripts/+ notebooks : 0 hit — lefetch_rle()cité dans le body parent n'existe plus dans Lean-16j, dérive déjà documentée).p5760— à mesurer, pas à supposer.HashlifeCorrectness.lean:7346(evolveHashlifeFastMemo (k * p) g = g).Livrables
scripts/lean/rle_to_lean_grid.py: parse RLE (standard Golly :b/o/$/compteurs) → littéral Lean[(x, y), …] : Grid+ coordonnées normalisées. Testé sur les 2 RLE en dépôt.unitcellInitial/unitcellTarget(puisotca*) par les grilles issues des RLE. Si le motif est un oscillateur en place : cible = forme de périodicité (= initialàpexact), qui reste un énoncé non-circulaire (échoue pour une grille ou une période fausse) — trancher par contre-vérification Python indépendante.evolveHashlifeFastMemo (p+1) initial ≠ initialou période tronquée.lake buildLOCAL SUCCESS (WSL, lean-merge-discipline R1),count_code_sorry.py --lake …sans régression (le lake porte 1distinct_code_sorry, critère 1 hors scope de cette tranche),proof-integrity(jamaisnative_decide.*non justifié — ici explicitement le design « Phase 3c : by native_decide avec Hashlife mémoïsé » du lake, à confronter au gate).Pillars_en.leanen paire (byte-identity sur signatures/preuves, docstrings EN).Hors scope
gemini_witness/cpu_witness(motifs non disponibles / 33 M générations — fenêtre dédiée).distinct_code_sorry→ 0, bloqué par [Lean fix] hashlife_correct_margin depends on sorryAx — lever la dette du lake conway_lean #13483) et critère 3 (mesure de temps notebook).