Wikipedia/Koethe: `matrixOver_KotherRadical` carries an unused `{I}`/`hI`, and its docstring describes a different statement from the (correct) code

## Summary

Low-severity, two small things in
`Koethe.KotherConjecture.variants.matrixOver_KotherRadical`:

1. the hypotheses `{I : TwoSidedIdeal R} (hI : IsNil I)` do **not** occur in the
conclusion — they are spurious, unlike in the two sibling declarations where the same
`I` is the subject;
2. the docstring describes something different from (and weaker than) the code, which is
itself correct.

https://github.com/google-deepmind/formal-conjectures/blob/638da20efd8eeeed2993fc2550fc596dc90c1ce8/FormalConjectures/Wikipedia/Koethe.lean#L74-L81

```lean
open scoped Classical in
/-- The **Köthe conjecture**: for any positive integer `n`, the Köthe radical of `R` is the matrix ideal `M_2(Nil*(R))`. -/
@[category research open, AMS 16]
theorem KotherConjecture.variants.matrixOver_KotherRadical
{I : TwoSidedIdeal R} (hI : IsNil I) (n : Type*) [Fintype n] :
matrix n (Nil* R) = Nil* (Matrix n n R) := by
sorry
```

## Spurious hypotheses

`I` and `hI` appear nowhere in `matrix n (Nil* R) = Nil* (Matrix n n R)`. `I` is
implicit and otherwise unconstrained, so it can never be inferred by unification and can
only ever be supplied by hand at a use site.

This is **not** a vacuity problem: `IsNil I` is satisfiable (`I = ⊥` is nil), so the
declaration is logically equivalent to the same statement with the two binders removed —
it is not accidentally trivially true, it is just carrying dead weight. Hence "low
severity". Still worth fixing, because a reader comparing the three matrix variants sees
`(hI : IsNil I)` in all of them and reasonably assumes it plays the same role, and
because the two siblings

```lean
theorem KotherConjecture.variants.general_matrix {I : TwoSidedIdeal R} (hI : IsNil I)
(n : Type*) [Fintype n] : IsNil (matrix n I)

theorem KotherConjecture.variants.two_by_two_matrix {I : TwoSidedIdeal R} (hI : IsNil I) :
IsNil (matrix (Fin 2) I)
```

*do* use them.

## Docstring does not match the code

The docstring says "for any positive integer `n`, the **Köthe radical of `R`** is the
matrix ideal `M_2(Nil*(R))`". The code says `matrix n (Nil* R) = Nil* (Matrix n n R)`,
i.e. the Köthe radical of the **matrix ring** is the matrix ideal over the Köthe radical
of `R`. Two mismatches:

* `Nil*(R)` vs `Nil*(M_n(R))` on the right of the equation — the docstring names the
wrong ring;
* `M_2` vs an arbitrary `n : Type*` `[Fintype n]` — the docstring fixes the size while
the code quantifies over it (`M_2` is the sibling `two_by_two_matrix`).

**The code is the correct one.** Wikipedia's equivalent formulation 6 of the Köthe
conjecture reads

> For any ring `R`, the upper nilradical of `M_n(R)` is the set of matrices with entries
> from the upper nilradical of `R` for every positive integer `n`

which is exactly `matrix n (Nil* R) = Nil* (Matrix n n R)`. Only the docstring needs
changing.

## Not a defect

`n : Type*` `[Fintype n]` admits `n = Empty`; both sides then live in the trivial ring
and are equal, so the empty case is harmless and no degeneracy hides there.

## Suggested fix

```lean
open scoped Classical in
/-- The **Köthe conjecture**: for any finite index type `n`, the Köthe radical of the matrix
ring `M_n(R)` is the ideal of matrices with entries in the Köthe radical of `R`. -/
@[category research open, AMS 16]
theorem KotherConjecture.variants.matrixOver_KotherRadical (n : Type*) [Fintype n] :
matrix n (Nil* R) = Nil* (Matrix n n R) := by
sorry
```

I have not opened a PR: removing binders from a declaration is the kind of change a
maintainer may prefer to bundle with the file's other pending tidy-up (the namespace is
spelled `KotherConjecture` throughout, apparently a typo for `KotheConjecture`, and the
first declaration is `KotheConjecture` with no `variants` prefix). Happy to send one if
that is preferred.

## The mathematics is unaffected

**This is a defect in the formalization only, and a cosmetic one.** The Köthe conjecture
is untouched; the declaration is not false and not vacuous, and it is a correct
statement of formulation 6. In the four-coordinate sense: (1) the underlying conjecture
is untouched and open; (2) no formal solution exists; (3) the *docstring* is unfaithful
while the code is faithful; (4) what the declaration literally asserts is right, just
with two unused binders attached. Only (3) is at issue.

## Relationship to the C₅[K₄] campaign

Found while auditing `research open` declarations in the `Wikipedia` collection for
faithfulness to their cited sources. Full derivation and the duplicate search:

https://github.com/Kuberwastaken/c5-k4/blob/d8a0c47da83203e1cd2c739b383f7a436435549f/results/expansion/live-search-2026-08-15/wikipedia-scan-A-L.md

## Source/status note

Wikipedia, *Köthe conjecture*, "Equivalent formulations", item 6, quoted above. The
Köthe conjecture is open. `git log` on this file shows only formatting and
classical-reasoning chores since the file was created, so the docstring has said this
since the beginning; `matrixOver_KotherRadical` returns no issue or PR hits.

## AI assistance disclosure

This report was prepared with AI assistance (Claude, Anthropic) for the source audit and
drafting. The submitter reviewed the declaration, the source text, and the suggested
repair, and takes responsibility for the submission.

### Choose either option
- [ ] I plan on working on this issue
- [x] This issue is up for grabs: I would like to see this misformalization fixed by somebody else

Open FormalConjectures/Wikipedia/Koethe.lean and inspect KotherConjecture.variants.matrixOver_KotherRadical alongside the two sibling declarations. Remove the unused binders and align the docstring with the arbitrary finite index type and matrix-ring statement; the file should still elaborate successfully.

Written by the indexing model from the issue text.