Repository navigation
feat(lean,#13483): maillon 3 -- tour dyadique complete des unions periodiques (HashlifeMarginFragment FR+EN) - #19363
Merged
Merged
Conversation
Ajoute quatre items a HashlifeMarginFragment (FR + sibling _en, preuves
byte-identiques) :
1. gridToMacroCellWithOffset_level_ge_of_span : l'etendue en distance de
Chebyshev de deux cellules vivantes borne INFERIEUREMENT le level du
macro-cell (reciproque de gridToMacroCellWithOffsetN_level_gt_n).
2. evolve_ne_of_period_ne : une grille non vide de periode T > 0 reste non
vide a tout temps t (decomposition t = (t/T)*T + t%T).
3. hcap_of_union_periodic_dyadic : hcap pour T = 2^i quelconque, la fenetre
geometrique max 3 (2^i) etant fournie par le temoin d'etendue (1), ce qui
leve la restriction T in {1,2,4} du maillon 2 sans hypothese de non-vacuite
sur la fenetre.
4. hashlife_correct_margin_of_union_periodic_dyadic : assemblage L2 miroir,
correction Hashlife pour une union scindee de periodes dyadiques.
Empile sur la tete de #19324 (maillon 2), consomme son moteur
(mem_evolve_union_sep, hcap_of_union_periodic, evolve_mulF_of_period).
Push retenu jusqu'au merge de #19324 (consigne de dispatch).
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
github-actions
Bot
added
the
lean-visibility-drift
Contributor
Path-collision (organ #13359/#13615)Cette PR #19363 (
Le verdict terminal (#15578) signale qu'un cote de la paire est deja sur |
Owner
Author
|
[ADJOINT PREFLIGHT] |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Grain: DEEP/lean — lane myia-po-2024:CoursIA — prev: MED/refactor #19347
See #13483 — maillon 3 de la séquence Hashlife : tour dyadique complète des unions périodiques,
HashlifeMarginFragment.lean+ sibling_en. Deux fichiers,361 insertions(+),0 deletion— aucune cellule de notebook touchée, aucun autre fichier.Ce que ce maillon ajoute
L'assemblage P4.4 annoncé par la décomposition du 2026-09-04 (c.5539811910) : la tour dyadique complète des unions périodiques dans le fragment de marge — le bloc de preuve
sorry-free qui ferme la partie constructive du maillon (les briques L1/L2 étaient posées, ce commit livre la tour). Paire FR/_enselon la convention #4980 : docstrings FR + sibling_enbyte-identique hors docstrings.Compte de
sorry— instrument canonique, avant/aprèspython scripts/lean/count_code_sorry.py --json, champdistinct_code_sorry, lakeMyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean:origin/main(base)68bff205d391 → 1, inchangé, et c'est l'état attendu. Le
sorrysurvivant est l'énoncé-cadrehashlife_correct_margin(HashlifeMarginFragment.lean:170+ miroir_en) — cœur de recherche ouvert P4/P5, verdict INTRINSIC documenté, acceptance B (voir le module doc etlean-conway.yml:12: « conway has 1 real tactic sorry (HashlifeMarginFragment.lean framework sorry) »). Ce maillon ne le touche pas : il ajoute de la preuve complète autour de lui. Jamaisgrep -c sorry: 194 naïfs pour 1 réel sur ce lake.Preuves d'élaboration (locales, tête
68bff205d39)lake env leandepuis le lake dans WSL, contenu committé :Le
lake buildcomplet du lake est porté par la CIlean-conway.yml(déclenchée par le filtre de cheminconway_lean/**.lean).B.3 — proof-integrity : câblage vérifié, portée exacte
lean-conway.ymlappelle bienlean-axiom.yml(câblage :grep -ln lean-axiom .github/workflows/*.yml). La jambe bloquanteproof-integritycibleConway.KochenSpecker, Conway.FreeWillTheorem— le module modifié ici n'en fait PAS partie ; l'audit advisory couvre les fondations Life (Conway.Life.HashlifeCorrectness+ MacroCell/Hashlife). Écrit ici au lieu d'être sauté en silence, conformément à §B.3 du précis de review : le vert bloquant attendu ne prouve pas ce module, et l'audit advisory en couvre le voisinage.Le piège
omegaréparé (et sa sonde)Les deux branches
Or.inrde la disjonction de marge échouaient suromegaavec un goal contaminé par une métavariable :Int.natAbs_of_nonneg : 0 ≤ a → natAbs a = ane peut pas unifier le but de branchenatAbs (q - p) = p - q(la conclusionnatAbs a = adiffère), l'unification diffère?m, etomegaéchoue sur le but pollué.Int.natAbs_of_nonposetInt.natAbs_sub_commn'existent pas dans ce Mathlib (vérifié par sonde). Réparation :Isolée par une sonde minimale à 4 variantes (V1/V2 absentes, V3/V4 compilent) avant de toucher les fichiers réels. Miroir identique sur
p.2/q.2danshcolabs, et dans le sibling_en.Provenance de la branche
Construit sur le commit maillon 2 (
1902d8d06e8) ; #19324 a été squash-mergé (f8f3443b33fc, parent unique — mesuré), donc le parent n'est pas ancêtre demain:git rebase --onto origin/main 1902d8d06e8. Vérifié : blobs du parent == blobs deorigin/main(ac11c8bb78b/211633911e5), et le diff deux-points tête vsmain= exactement les 361 insertions de ce maillon — aucun résidu du maillon 2, aucune collision add/add.Garde i18n
python scripts/lean/check_i18n_siblings.py --all:327/333 paires byte-identical | 6 consumer | 0 drift | 0 orphan— la paire FR/_ende ce maillon est byte-identique hors docstrings (gate #4980).Portée écrite
HashlifeMarginFragment.lean/HashlifeMarginFragment_en.lean.sorry-cadre INTRINSIC (hashlife_correct_margin) n'est ni touché ni affaibli.check_lane_claim.py 13483 --paths <2 fichiers>→CLEAR, aucune autre lane.MERGEDà 18:17:38Z avant ce push.🤖 Generated with Claude Code