From eacb29b98c3ae7900bfe0e12c3136867b2aff0b3 Mon Sep 17 00:00:00 2001 From: "Claude Haiku 4.5 (1M context)" Date: Thu, 24 Sep 2026 11:55:36 +0200 Subject: [PATCH] fix(lean,#17570): docstring hashlife_correct -- status 2026-08-15 + renvoi evolveHashlifeFastAtN_correct_uncond MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit L.6369-6372 du docstring /-- theorem hashlife_correct ... -/ datait du 2026-06-13 et affirmait « inductive step remains open (the sorry below) ». Clos depuis #5998 (p5_inductive_step fermé en 2026-07). Pire : la nouvelle analyse de #17570 montre que `hashlife_correct` est *vacuously true* sur le régime `n >= jumpSize = 8` car `BoxAssezGrand g n` est unsatisfiable sur grilles non-vides (`p5_large_n_hyps_unsat`). La docstring dit maintenant l'exact : `hashlife_correct` est fermé mais vide dans le régime du saut ; la garantie pleine, inconditionnelle et `non-vacuous` vit dans `evolveHashlifeFastAtN_correct_uncond` (l. 7202 du même fichier, sur main depuis #11781). Les consommateurs ICT doivent citer ce dernier. Aucun changement de preuve. Scope : 1 fichier, +11/-4 lignes, docstring uniquement. See #17570 --- .../Conway/Life/HashlifeCorrectness.lean | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean index e386ae63f2..3affd5ec60 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/conway_lean/Conway/Life/HashlifeCorrectness.lean @@ -6366,10 +6366,17 @@ theorem p5_inductive_step (n : Nat) (g : Grid) (h : BoxAssezGrand g n) : the recursion because the jump preserves bounding box up to light-cone expansion. - **Status (2026-06-13)**: base case `n = 0` proven above - (`hashlife_correct_base_zero`). The inductive step remains open (the - `sorry` below). See `hashlife_correct_implies_block_4` / - `hashlife_correct_implies_glider_8` for sanity witnesses. -/ + **Status (2026-08-15, #17570)** : proven via `p5_inductive_step` (closed + #5998, 2026-07) under the fixed-frame hypothesis `BoxAssezGrand g n`. But + that hypothesis is `unsat` for non-empty grids once `n ≥ jumpSize = 8` + (`p5_large_n_hyps_unsat`), so `hashlife_correct` is *vacuously true* on + the large-`n` regime where the Hashlife jump actually fires — it does NOT + certify a non-vacuous equality between `evolveHashlifeFast` and `evolve`. + The **non-vacuous, unconditional** large-`n` correctness statement is + `evolveHashlifeFastAtN_correct_uncond` (l. 7202 of this file, on `main` + since #11781, 2026-08-15): ICT series consumers should cite that theorem. + `hashlife_correct` here stays for historical continuity and is named only + to declare its vacuity. See #17570. -/ theorem hashlife_correct (n : Nat) (g : Grid) (h : BoxAssezGrand g n) : evolveHashlifeFast n g = evolve n g := by -- P5 TARGET: main theorem, composition of P2-P4