Import the disproof of the Köthe conjecture (Krempa's matrix form)

LeanPool.lean

@@ -2284,6 +2284,27 @@ import LeanPool.KasamiCyclicAdditive.Prelude
 import LeanPool.KasamiCyclicAdditive.Statement.CoefficientForm
 import LeanPool.KasamiCyclicAdditive.Statement.Definitions
 import LeanPool.KasamiCyclicAdditive.Statement.ParameterReduction
+import LeanPool.Koethe
+import LeanPool.Koethe.Counterexample
+import LeanPool.Koethe.Disproof
+import LeanPool.Koethe.Linearization.Basic
+import LeanPool.Koethe.Linearization.Nil
+import LeanPool.Koethe.Linearization.Pencil
+import LeanPool.Koethe.MaskSequence.Basic
+import LeanPool.Koethe.MaskSequence.Chain
+import LeanPool.Koethe.MaskSequence.Universal
+import LeanPool.Koethe.Mortality.Degree
+import LeanPool.Koethe.Mortality.FormalWord
+import LeanPool.Koethe.Mortality.Homogeneous
+import LeanPool.Koethe.Mortality.Mask
+import LeanPool.Koethe.Mortality.MaskMortality
+import LeanPool.Koethe.Mortality.Minors
+import LeanPool.Koethe.MultiProjective
+import LeanPool.Koethe.Pencil
+import LeanPool.Koethe.ShiftWitness.Band
+import LeanPool.Koethe.ShiftWitness.Eigenvector
+import LeanPool.Koethe.ShiftWitness.Endpoint
+import LeanPool.Koethe.ShiftWitness.Witness
 import LeanPool.KrafftSieve
 import LeanPool.KrafftSieve.Basic
 import LeanPool.KrafftSieve.Defs

LeanPool/Koethe.lean

@@ -0,0 +1,68 @@
+/-
+Copyright (c) 2026 Tom Adamczewski and Epoch AI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: GPT-6 Astra, Tom Adamczewski
+-/
+
+import LeanPool.Koethe.Disproof
+
+/-!
+# Disproof of the Köthe conjecture (Krempa's matrix form)
+
+Source: arxiv:2609.07996, url:https://github.com/tadamcz/koethe
+Authors: Tom Adamczewski
+Status: verified
+Main declarations: `Koethe.KotherConjecture.variants.general_matrix.disproof`
+Tags: ring-theory, nil-ideals, koethe-conjecture, counterexample, matrix-rings
+MSC: 16N40, 16S50
+-/
+
+/-!
+## Mathematical overview
+
+Köthe's conjecture (1930) asks whether the sum of two nil left ideals of a ring is nil. Krempa
+(1972) showed that it is equivalent to the statement that `M_n(I)` is a nil ideal of `M_n(R)`
+for every ring `R` and every nil two-sided ideal `I`, already for `n = 2`. This development
+refutes that matrix form: `Koethe.KotherConjecture.variants.general_matrix.disproof` is
+exactly the negation of the research-open statement `KotherConjecture.variants.general_matrix`
+of Google DeepMind's Formal Conjectures (copied verbatim, see `LeanPool.Koethe.Disproof`), and
+`KoetheCounterexample.counterexample` exhibits, in every universe, a ring with a nil two-sided
+ideal `I` and a non-nilpotent matrix in `M_2(I)`.
+
+The witness ring is the unitization of the non-unital algebra `A` generated by three weighted
+backward shifts `(aᵢ u)(n) = vₙ(i) u(n + 1)` on the sequence space over `K = k(t)`, where
+`k = \overline{𝔽₂}` and `vₙ ∈ k³` are nonzero weights; the nil ideal is `A` itself. The
+operator `a₀ + t a₁ + t² a₂` fixes an explicit nonzero vector, which yields a companion matrix
+`H ∈ M₂(R)` with a nonzero eigenvalue, so `H² ∈ M₂(A)` is not nilpotent
+(`LeanPool.Koethe.ShiftWitness`). The bulk of the development shows that the weights can be
+chosen so that `A` is nil:
+
+* `LeanPool.Koethe.Linearization`: every element of `A` is linearized into a one-row matrix
+  pencil whose nilpotence implies nilpotence of the element
+  (`KoetheCounterexample.nil_of_all_pencils_nil`);
+* `LeanPool.Koethe.MultiProjective`: a multiprojective common-zero theorem, namely that at most
+  `2N` polynomials multihomogeneous of a common positive degree in `N` blocks of three
+  variables have a common zero with no zero block, proved with the Segre cone, the
+  Nullstellensatz and Krull's height theorem (`KoetheMultiProjective.exists_common_zero`);
+* `LeanPool.Koethe.Mortality`: mask mortality, namely that a periodic mask with more than half
+  of its residues free admits a compatible word of nonzero letters killing any given pencil,
+  by determinantal rank reduction (`KoetheCounterexample.maskMortality`);
+* `LeanPool.Koethe.MaskSequence`: a diagonal construction over the countably many pencils
+  gives a universal mortal sequence (`KoetheCounterexample.exists_universalMortalSequence`).
+
+The implication from Köthe's original formulation to the matrix form (each column ideal of
+`M_n(I)` is a nil left ideal) is standard and is not part of the formal development.
+
+## Provenance
+
+Imported from <https://github.com/tadamcz/koethe> at commit
+`a94a72aec957cb28d76aa30fb97a01d440990d7f` (Apache-2.0). The Lean proof was written
+autonomously by a pre-release version of GPT-6 Astra (OpenAI) in Epoch AI's LeanOpenProblems
+evaluation harness, starting from the Formal Conjectures statement, and was packaged by Tom
+Adamczewski; an informal write-up is arXiv:2609.07996 (Adamczewski, Böhmler, Marczinzik). The
+port splits the single upstream file into modules along its original part boundaries,
+replaces the broad `import Mathlib` by minimal imports, removes the per-part
+`set_option autoImplicit false` lines, renames the pencil field `constant` to `scalar`, and
+repairs the Mathlib API drift from v4.28.0 to the pool's toolchain. No statement was
+weakened; three auxiliary lemmas were generalized from `Fintype` to `Finite` index types.
+-/

LeanPool/Koethe/Counterexample.lean

@@ -0,0 +1,67 @@
+/-
+Copyright (c) 2026 Tom Adamczewski and Epoch AI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: GPT-6 Astra, Tom Adamczewski
+-/
+import Mathlib.Algebra.AlgebraicCard
+import Mathlib.Algebra.Field.ULift
+import Mathlib.Algebra.Field.ZMod
+import Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
+import Mathlib.Tactic.Ring
+import LeanPool.Koethe.Mortality.MaskMortality
+import LeanPool.Koethe.MaskSequence.Universal
+import LeanPool.Koethe.Linearization.Nil
+import LeanPool.Koethe.ShiftWitness.Witness
+
+/-!
+# The counterexample: a nil ideal with a non-nilpotent `2 × 2` matrix
+
+This file assembles the whole development. The scalar-linearization theorem
+`KoetheCounterexample.nil_of_all_pencils_nil` discharges the explicit hypothesis of
+`KoetheCounterexample.ShiftWitness.exists_nilideal_nonnil_matrix`, and the ground field
+`GroundField = AlgebraicClosure (ULift (ZMod 2))` is countable and algebraically closed, so
+`exists_universalMortalSequence` and `maskMortality` apply to it. The result is a ring `R`
+in an arbitrary universe, a nil two-sided ideal `I ⊆ R`, and a matrix in `M_2(I)` that is
+not nilpotent.
+-/
+
+noncomputable section
+
+universe u
+
+namespace KoetheCounterexample
+
+/-- A universal mortal sequence over any field produces a nil two-sided ideal
+in a unital ring, with a nonnilpotent two-by-two matrix over that ideal. -/
+theorem exists_nilideal_nonnil_matrix_of_universal_mortal
+    {k : Type u} [Field k] (v : ℕ → Triple k) (hv : UniversalMortalSequence k v) :
+    ∃ (R : Type u) (_ : Ring R) (I : TwoSidedIdeal R),
+      (∀ x ∈ I, IsNilpotent x) ∧
+        ∃ W : Matrix (Fin 2) (Fin 2) R,
+          W ∈ TwoSidedIdeal.matrix (Fin 2) I ∧ ¬ IsNilpotent W :=
+  ShiftWitness.exists_nilideal_nonnil_matrix v hv nil_of_all_pencils_nil
+
+/-- The countable algebraically closed ground field `\overline{𝔽₂}`, lifted to an arbitrary
+universe so that the counterexample exists in every universe. -/
+abbrev GroundField : Type u := AlgebraicClosure (ULift.{u} (ZMod 2))
+
+instance countable_groundField : Countable (GroundField.{u}) :=
+  Set.countable_univ_iff.mp <|
+    (Algebraic.countable (ULift.{u} (ZMod 2)) (GroundField.{u})).mono
+      fun x _ => Algebra.IsAlgebraic.isAlgebraic x
+
+/-- **A counterexample to nilness of finite matrix ideals.** In every universe there is a
+ring `R` with a nil two-sided ideal `I` such that the matrix ideal `M_2(I)` of `M_2(R)`
+contains a non-nilpotent matrix. -/
+theorem counterexample :
+    ∃ (R : Type u) (_ : Ring R) (I : TwoSidedIdeal R),
+      (∀ x ∈ I, IsNilpotent x) ∧
+        ∃ W : Matrix (Fin 2) (Fin 2) R,
+          W ∈ TwoSidedIdeal.matrix (Fin 2) I ∧ ¬ IsNilpotent W := by
+  obtain ⟨v, hv⟩ := exists_universalMortalSequence (GroundField.{u})
+    (maskMortality (GroundField.{u}))
+  exact exists_nilideal_nonnil_matrix_of_universal_mortal v hv
+
+end KoetheCounterexample
+
+end

LeanPool/Koethe/Disproof.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2026 Tom Adamczewski and Epoch AI. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: GPT-6 Astra, Tom Adamczewski
+-/
+import Mathlib.Algebra.GroupWithZero.Basic
+import Mathlib.Data.SetLike.Basic
+import Mathlib.RingTheory.Ideal.Defs
+import Mathlib.RingTheory.TwoSidedIdeal.Basic
+import Mathlib.RingTheory.TwoSidedIdeal.Lattice
+import LeanPool.Koethe.Counterexample
+
+/-!
+# Disproof of the Köthe conjecture in Krempa's matrix form
+
+Köthe's conjecture (1930) asks whether the sum of two nil left ideals of a ring is always
+nil, equivalently whether every ring has a largest nil left ideal. Krempa (1972) showed it
+equivalent to several other statements, among them that for every ring `R` and nil two-sided
+ideal `I` the matrix ideal `M_n(I)` is nil in `M_n(R)` (already for `n = 2`).
+
+This file states that matrix form exactly as Google DeepMind's Formal Conjectures does and
+proves its negation from `KoetheCounterexample.counterexample`. The definitions `Koethe.IsNil`
+and `Koethe.KotheRadical` and the bracketed conjecture inside
+`Koethe.KotherConjecture.variants.general_matrix.disproof` are copied verbatim from
+`FormalConjectures/Wikipedia/Koethe.lean` in
+[Formal Conjectures](https://github.com/google-deepmind/formal-conjectures) at commit
+`9cbe1d3c12998c786b7c2cd99ce28a21b6631f66` (Copyright 2025 The Formal Conjectures Authors,
+Apache-2.0), where `KotherConjecture.variants.general_matrix` is registered as a research-open
+statement.
+
+Since `M_n(I)` is the sum of its `n` column left ideals, each of which is nil when `I` is,
+Köthe's original statement implies the matrix form; the counterexample therefore also refutes
+the conjecture as originally stated. That implication is a standard argument and is not part
+of this formal development.
+-/
+
+open Ideal TwoSidedIdeal Polynomial
+
+open Matrix
+
+variable {R : Type*}
+
+variable [Ring R]
+
+namespace Koethe
+
+/-- Say a subset `I` of a ring `R` is nilpotent if all its elements are nilpotent. -/
+def IsNil {S : Type*} [SetLike S R] (I : S) := ∀ i ∈ I, IsNilpotent i
+
+variable (R) in
+/-- The *Kothe Radical* of a ring `R` is the sum of all (two-sided) nil ideals of `R`.
+Tags: Kothe Radical, upper nilradical -/
+def KotheRadical : TwoSidedIdeal R := sSup {I : TwoSidedIdeal R | IsNil I}
+
+end Koethe
+
+open scoped Classical in
+/--
+**Disproof of the Köthe conjecture in Krempa's matrix form** (the
+`KotherConjecture.variants.general_matrix` statement of Formal Conjectures): it is not the case
+that for every ring `R`, every nil two-sided ideal `I` and every finite index type `n`, the
+matrix ideal `M_n(I)` is nil.
+-/
+theorem Koethe.KotherConjecture.variants.general_matrix.disproof :
+    ¬ (∀ {R : Type*} [Ring R] {I : TwoSidedIdeal R},
+      IsNil I → ∀ (n : Type*) [Fintype n], IsNil (matrix n I)) := by
+  classical
+  intro h
+  obtain ⟨S, hS, I, hI, W, hW, hn⟩ := KoetheCounterexample.counterexample
+  let _ : Ring S := hS
+  have ht := @h S hS I hI (ULift (Fin 2)) inferInstance
+  let _ : DecidableEq (ULift (Fin 2)) := Classical.decEq _
+  let e := Matrix.reindexAlgEquiv ℕ S (Equiv.ulift.symm : Fin 2 ≃ ULift (Fin 2))
+  apply hn
+  apply (IsNilpotent.map_iff e.injective).mp
+  apply ht (e W)
+  rw [TwoSidedIdeal.mem_matrix] at hW ⊢
+  intro i j
+  exact hW i.down j.down