From ed0f032109adc0ed14c33387aeef9ea9b297d327 Mon Sep 17 00:00:00 2001 From: jsboige Date: Wed, 4 Nov 2026 08:32:04 +0100 Subject: [PATCH] Fix(i18n,#24143): aligner le miroir EN de Knots.Invariant sur le canonique FR (22 -> 0 HARD) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Le lac `knot_lean` portait 22 findings HARD de l'organe de fidelite des jetons i18n sur le couple `Invariant.lean` / `Invariant_en.lean`. Les 22 ont ete relus FIRSTHAND et se repartissent en 5 mecanismes : 1. un span de code melangeant code et prose FR (`d₂.edges = d₁.edges ++ (labels de c₁, c₂)`) — la prose est sortie du span des deux cotes ; 2. un span EN unique (`simp only [triColorConditionAt, hcol*]`) ou le FR porte deux spans distincts sur deux lignes — re-pose 1 span par ligne ; 3. un bloc de commentaire EN comptant 10 lignes pour 9 au FR (le « mur R2 »), qui decalait l'appariement par rang et faisait porter `r2_append_only_wall` et le nombre `2` aux mauvaises paires ; 4. un `R1` ecrit une ligne trop haut cote EN, et un `4_1` ASCII cote EN la ou le FR ecrit `4₁` (le `1` ASCII etait un nombre en trop) ; 5. un groupe de 10 lignes FR pour 11 lignes EN (le corollaire `trefoil_not_unknot`) : le miroir EN nommait les deux pieces que le FR laissait en prose. Le point 5 traite dans les DEUX sens : le FR est **enrichi** (les deux pieces sont nommees comme spans de code) et le miroir EN est complete (`sorry` mentionne comme au FR). Aucune suppression : rien n'est retire ni d'un cote ni de l'autre. Mesures (meme organe avant et apres) : | organe | avant | apres | |-----------------------------------|-----------------|----------------| | #24584 (fence corrigee) | 22 HARD / 267 A | 0 HARD / 240 A | | compose #24584 + #24591 | 22 HARD / 267 A | 0 HARD / 240 A | | `main` / #24591 (avant fence) | 152 HARD / 458 A| 130 HARD / 431 A| Les 130 residuels sous l'organe de `main` sont les **artefacts de fence** (c.828), deja corriges par la PR #24584 ; aucune variante d'organe ne **gagne** un finding, et le lac passe de 68 a 46 HARD. Preuves : `check_i18n_siblings.py` 24/24 paires byte-identiques (0 drift, 0 orphan, 0 unbuilt) ; `count_code_sorry.py --json` : `distinct_code_sorry` du lac = 8 avant et 8 apres ; `lake build` / `Proof integrity` **inchanges par construction** (code byte-identique). Diff 2 fichiers, 16+/16-, commentaires uniquement. See #24143 Co-Authored-By: Claude Haiku 5.5 --- .../Lean/KNOTS/knot_lean/Knots/Invariant.lean | 5 ++-- .../KNOTS/knot_lean/Knots/Invariant_en.lean | 27 +++++++++---------- 2 files changed, 16 insertions(+), 16 deletions(-) diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant.lean index fe76848578a..dad873f66b6 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant.lean @@ -790,7 +790,7 @@ theorem tricolorable_forward_r1 {d₁ d₂ : KnotDiagram} `numEdges + 4`), l'autre les retire. Le bras ASCENDANT (d₂ = d₁ ++ [c₁, c₂]) admet un transfert avant complet et simple : sous `wf`, chaque label ancien apparaît déjà exactement 2× dans `d₁.edges` (clause b) et exactement 2× dans -`d₂.edges` — or `d₂.edges = d₁.edges ++ (labels de c₁, c₂)` — donc les +`d₂.edges` — or `d₂.edges = d₁.edges` ++ (labels de c₁, c₂) — donc les croisements appendés n'utilisent QUE les 4 labels fraîches `{n+1..n+4}`. Le témoin : les 4 arêtes fraîches reçoivent TOUTES `TriColor.red` ; chaque croisement appendé lit alors `(red, red, red, red)` — bornes par wf (a), @@ -3693,7 +3693,8 @@ theorem trefoil_not_unknot : ¬ KnotEquiv trefoil unknot := by -- trefoil ≈ unknot ⇒ trefoil tricolorable ↔ unknot tricolorable (invariant). -- trefoil IS tricolorable, unknot IS NOT ⇒ contradiction. -- The sketch that was left as `sorry` now type-checks: `tricolorable_invariant` - -- is proven, and the two pieces are proven, so the corollary composes them. + -- is proven, and the two pieces (`trefoil_tricolorable`, `unknot_not_tricolorable`) are + -- proven, so the corollary composes them. -- -- The `Knot`-level wrappers (`KnotEquiv`, `Knot.isTricolorable`) are opaque -- `def`s that delta-reduce on demand to the `KnotDiagram` level diff --git a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant_en.lean b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant_en.lean index 1d328d51521..3dc214674cc 100644 --- a/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant_en.lean +++ b/MyIA.AI.Notebooks/SymbolicAI/Lean/KNOTS/knot_lean/Knots/Invariant_en.lean @@ -1,5 +1,5 @@ /- - Knots.Invariant — Knot invariants (3-colorability, crossing number) + Knots.Invariant — Knot invariants (tricolorability, crossing number) ==================================================================== Knot invariants distinguish knots. This file scaffolds: @@ -538,8 +538,8 @@ theorem triColorConditionAt_newKink {d₁ d₂ : KnotDiagram} (d₁.numEdges + 2) he_lo he_hi -- Closure (resolved c.987): `simp only [triColorConditionAt]` unfolds the -- condition WITHOUT unfolding `colorAtNat` (not marked `@[simp]`), so the `_hcol` - -- match the un-unfolded form — this was the c.986 pitfall (the mixed - -- `simp only [triColorConditionAt, hcol*]` unfolded `colorAtNat` before the hcol match). + -- match the un-unfolded form — this was the c.986 pitfall (the mixed `simp only` + -- `triColorConditionAt, hcol*` unfolded `colorAtNat` before the hcol match). -- After the 2 `simp only`, the 4 slots reduce to `d₁.colorAtNat coloring₁ a`: -- continuity `c2=c4` → `True`, Fox left `(=a ∧ =a)` → `True ∧ True`, Fox -- right `(≠a ∧ …)` remains as an opaque `TriColor ≠` atom. The residual is thus @@ -739,7 +739,7 @@ theorem tricolorable_forward_r1 {d₁ d₂ : KnotDiagram} `numEdges + 4`), the other removes them. The ASCENDING arm (d₂ = d₁ ++ [c₁, c₂]) admits a complete and simple forward transfer: under `wf`, every old label already appears exactly 2× in `d₁.edges` (clause b) and exactly 2× in -`d₂.edges` — and `d₂.edges = d₁.edges ++ (labels of c₁, c₂)` — so the appended +`d₂.edges` — and `d₂.edges = d₁.edges` ++ (labels of c₁, c₂) — so the appended crossings use ONLY the 4 fresh labels `{n+1..n+4}`. The witness: all 4 fresh edges receive `TriColor.red`; each appended crossing then reads `(red, red, red, red)` — bounds by wf (a), continuity `red = red`, Fox @@ -1049,10 +1049,9 @@ theorem r2_append_only_wall : -- `Reidemeister2` — was false for the append-only constructor. This counterexample -- has been **removed** (Stage 2, #2874): re-anchoring `r2`/`r3` onto the -- **connected** relations (`Reidemeister2Connected`/`Reidemeister3Connected`) closes --- the door on the free moves, the master is proven (§2-Ω), and --- `not_tricolorable_invariant_current` becomes false by construction. The wall --- `r2_append_only_wall` (below) remains valid: it speaks of the FREE move, not of --- the `ReidemeisterEquiv` closure. +-- the door on the free moves, the master is proven (§2-Ω), and `not_tricolorable_invariant_current` +-- becomes false by construction. The wall `r2_append_only_wall` (below) remains +-- valid: it speaks of the FREE move, not of the `ReidemeisterEquiv` closure. -- theorem not_tricolorable_invariant_current : ⊥ -- removed: see comment above. /-! ### R2 cure foundation — cardinality is the only obstruction @@ -2111,7 +2110,7 @@ theorem unknot_not_tricolorable : ¬ Knot.isTricolorable unknot := by /-! ## 4b. The figure-eight is NOT tricolorable -The figure-eight (4_1) has 4 crossings and determinant 5, so it is NOT +The figure-eight (4₁) has 4 crossings and determinant 5, so it is NOT 3-colorable in the Fox sense. Under **Path B** (the `c₂ = c₄` over-strand continuity conjunct), this is the canonical distinguishing witness: the earlier permissive model admitted a spurious tricoloring `(0,0,0,1,0,0,1,2)` (README @@ -2861,8 +2860,8 @@ theorem Reidemeister1Connected.tricolorable_backward {d₁ d₂ : KnotDiagram} · -- All-distinct kink mode: VACUOUS (cycle #11211). The kink -- `C = ⟨a, b, c, c⟩` has `e3 = e4 = c`: over-strand continuity -- (`c2 = c4`, Path B conjunct) reads `col₂(b) = col₂(c)` = `c3`, - -- while the all-distinct Fox mode requires `c2 ≠ c3`. An R1 - -- self-crossing is only Fox-colourable in all-equal mode — no + -- while the all-distinct Fox mode requires `c2 ≠ c3`. An + -- R1 self-crossing is only Fox-colourable in all-equal mode — no -- `IsTricolorable d₂` witness reaches this branch. The earlier -- col₂→col₁ lifts (projective / single-swap / σ∘col₂, withdrawn -- register) were searching for an inhabitant of an empty branch; @@ -3597,9 +3596,9 @@ theorem trefoil_not_unknot : ¬ KnotEquiv trefoil unknot := by intro h -- trefoil ≈ unknot ⇒ trefoil tricolorable ↔ unknot tricolorable (invariant). -- trefoil IS tricolorable, unknot IS NOT ⇒ contradiction. - -- `tricolorable_invariant` is now proven, so the corollary composes it with - -- the two pieces (`trefoil_tricolorable`, `unknot_not_tricolorable`), both - -- proven under the real Fox condition. + -- The sketch left as `sorry` now type-checks: `tricolorable_invariant` + -- is proven, and the two pieces (`trefoil_tricolorable`, `unknot_not_tricolorable`) are + -- proven under the real Fox condition, so the corollary composes them. -- -- The `Knot`-level wrappers (`KnotEquiv`, `Knot.isTricolorable`) are opaque -- `def`s that delta-reduce on demand to the `KnotDiagram` level