KaplanskyUInvariant.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

17 declarations, 13 contain sorry, 0 declared as axioms

Kaplansky's problem on the values of the $u$-invariant

The $u$-invariant $u(F)$ of a field $F$ is the largest dimension of an anisotropic quadratic form over $F$, or $\infty$ if there is no largest one; that is, $u(F) = n$ exactly when IsGreatest (QuadraticForm.anisotropicDims F) n. Following [Kaplansky1953] and [MerkurjevParimala2025, §5.1], all fields are of characteristic not $2$.

Kaplansky introduced the invariant (his $C(F)$) in [Kaplansky1953, p. 201], proved that $u(F) \ne 3$ (his Theorem 2), observed that every power of $2$ occurs (his Theorem 3 gives $u(F((t))) = 2u(F)$), and conjectured that $u(F)$ is a power of $2$ whenever it is finite [Kaplansky1953, p. 202]. It is classical that $u(F) \notin \{3, 5, 7\}$ [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4]. Merkurjev disproved Kaplansky's conjecture with a field of $u$-invariant $6$ [Merkurjev1989] and then showed that every positive even integer is a $u$-invariant [Merkurjev1991]. Izhboldin constructed a field of $u$-invariant $9$ [Izhboldin2001], and Vishik fields of $u$-invariant $2^r + 1$ for every $r \ge 3$ [Vishik2009]. A 2026 preprint of Karpenko constructs fields of $u$-invariant $n$ for every $n$ that is neither of the form $2^r - 1$ nor of the form $2^r - 3$ [Karpenko2026]; as of September 2026 it is not yet peer-reviewed.

The problem (u_invariant_values) is to determine which integers are $u$-invariants of fields. The survey [MerkurjevParimala2025, §5.1] records the expectation that every odd integer $\ge 9$ is a $u$-invariant (u_invariant_values.variants.odd). Given the results above, the problem is open exactly for the integers $2^r - 1$ and $2^r - 3$ with $r \ge 4$, the smallest of which are $13$ and $15$.

References:

[Kaplansky1953] I. Kaplansky, Quadratic forms, J. Math. Soc. Japan 5 (1953), 200–207, doi:10.2969/jmsj/00520200.
[Lam2005] T. Y. Lam, Introduction to quadratic forms over fields, Grad. Stud. Math. 67, Amer. Math. Soc., 2005, doi:10.1090/gsm/067.
[EKM2008] R. Elman, N. Karpenko, A. Merkurjev, The algebraic and geometric theory of quadratic forms, Amer. Math. Soc. Colloq. Publ. 56, Amer. Math. Soc., 2008, doi:10.1090/coll/056.
[Merkurjev1989] A. S. Merkurjev, Kaplansky's conjecture in the theory of quadratic forms (Russian), Zap. Nauchn. Sem. LOMI 175 (1989), 75–89; English transl. J. Soviet Math. 57 (1991), no. 6, 3489–3497, doi:10.1007/BF01100118.
[Merkurjev1991] A. S. Merkurjev, Simple algebras and quadratic forms (Russian), Izv. Akad. Nauk SSSR Ser. Mat. 55 (1991), no. 1, 218–224; English transl. Math. USSR-Izv. 38 (1992), no. 1, 215–221, doi:10.1070/IM1992v038n01ABEH002195.
[Izhboldin2001] O. T. Izhboldin, Fields of $u$-invariant $9$, Ann. of Math. (2) 154 (2001), no. 3, 529–587, doi:10.2307/3062141.
[Vishik2009] A. Vishik, Fields of $u$-invariant $2^r + 1$, pp. 661–685 in Algebra, arithmetic, and geometry: in honor of Yu. I. Manin, Vol. II, Progr. Math. 270, Birkhäuser, 2009, doi:10.1007/978-0-8176-4747-6_22.
[Karpenko2026] N. A. Karpenko, Fields of any $u$-invariant but a 2-power minus 1 or 3, preprint, 5 August 2026, author's web page.
[MerkurjevParimala2025] A. Merkurjev, R. Parimala, Quadratic forms beyond arithmetic, Notices Amer. Math. Soc. 72 (2025), no. 7, 711–718, doi:10.1090/noti3192.

Imports (1)

FormalConjecturesUtil

def KaplanskyUInvariant.IsUInvariant IsUInvariant n means that some field of characteristic not 2 has $u$-invariant $n$, i.e. $n$ is the largest dimension of an anisotropic quadratic form over that field line 90 source
Source documentation
IsUInvariant n means that some field of characteristic not 2 has $u$-invariant $n$, i.e. $n$ is the largest dimension of an anisotropic quadratic form over that field.
The field is taken in Type (universe $0$), which loses nothing. A quadratic form in $m$ variables is given by finitely many coefficients, so for fixed $n$ the property "characteristic not $2$ and $u$-invariant $n$" is one first-order sentence in the language of rings: $1 + 1 \ne 0$, some form in $n$ variables is anisotropic, and every form in $n + 1$ variables is isotropic (then so is every form in more variables). By the downward Löwenheim–Skolem theorem, a field with this property in any universe has a countable elementary subfield, which has the same property and is isomorphic to a field in Type. Conversely, ULift moves a field in Type to any universe.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Field, NeZero, OfNat.ofNat, IsGreatest, QuadraticForm.anisotropicDims
13 instances, coercions and auxiliary constants left out.
```
def IsUInvariant (n : ℕ) : Prop :=
…
```
theorem KaplanskyUInvariant.isGreatest_anisotropicDims_complex $u(\mathbb{C}) = 1$ [MerkurjevParimala2025, §5.1]: the form $x^2$ is anisotropic, and every quadratic form in two or more variables over an algebraically closed field is isotropic line 96 source
Source documentation
$u(\mathbb{C}) = 1$ [MerkurjevParimala2025, §5.1]: the form $x^2$ is anisotropic, and every quadratic form in two or more variables over an algebraically closed field is isotropic.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: IsGreatest, Nat, QuadraticForm.anisotropicDims, Complex, OfNat.ofNat
Proof uses: And.intro, Membership.mem, Set, upperBounds, QuadraticForm.one_mem_anisotropicDims, LE.le, QuadraticForm, Fin, QuadraticMap.Anisotropic, QuadraticMap.Nondegenerate, Decidable.byContradiction, Not, LinearMap.SeparatingLeft, RingHom.id, LinearMap, QuadraticMap, LinearMap.BilinMap, QuadraticMap.associated, Eq, Eq.mp and 56 more
119 instances, coercions and auxiliary constants left out.

Tactic trace: 18 steps
Open to load the checked before-and-after goal states.
```
theorem isGreatest_anisotropicDims_complex : IsGreatest (anisotropicDims ℂ) 1 := by
…
```
theorem KaplanskyUInvariant.not_bddAbove_anisotropicDims_real $u(\mathbb{R}) = \infty$ [MerkurjevParimala2025, §5.1]: the sum of $n$ squares is anisotropic for every $n$, so there is no largest dimension of an anisotropic form line 117 source
Source documentation
$u(\mathbb{R}) = \infty$ [MerkurjevParimala2025, §5.1]: the sum of $n$ squares is anisotropic for every $n$, so there is no largest dimension of an anisotropic form.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Not, BddAbove, Nat, QuadraticForm.anisotropicDims, Real
Proof uses: Eq.mpr, Set.univ, id, Eq, congrArg, Set, QuadraticForm.anisotropicDims_eq_univ, not_bddAbove_univ
9 instances, coercions and auxiliary constants left out.

Tactic trace: 2 steps
Open to load the checked before-and-after goal states.
```
theorem not_bddAbove_anisotropicDims_real : ¬ BddAbove (anisotropicDims ℝ) := by
…
```
theorem KaplanskyUInvariant.u_invariant_values The values of the $u$-invariant, stated as in [MerkurjevParimala2025, §5.1]: which integers are $u$-invariants of fields (of characteristic not $2$)? sorry line 134 source
Source documentation
The values of the $u$-invariant, stated as in [MerkurjevParimala2025, §5.1]: which integers are $u$-invariants of fields (of characteristic not $2$)? The question goes back to [Kaplansky1953], who conjectured that only powers of $2$ occur (u_invariant_values.variants.kaplansky_conjecture). Every positive even integer is a $u$-invariant (u_invariant_values.variants.even), $3$, $5$ and $7$ are not (u_invariant_values.variants.not_three, u_invariant_values.variants.not_five, u_invariant_values.variants.not_seven), and it is expected that every odd integer $\ge 9$ is (u_invariant_values.variants.odd). Granting the preprint [Karpenko2026] (u_invariant_values.variants.karpenko), the answer is known for every $n$ except $n = 2^r - 1$ and $n = 2^r - 3$ with $r \ge 4$.

depends on sorry what this means
Statement uses: Set, Nat, sorryAx, Bool.false, Iff, Membership.mem, KaplanskyUInvariant.IsUInvariant
Proof uses: Lean.Name, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
3 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values :
    let S : Set ℕ := answer(sorry)
…
```
theorem KaplanskyUInvariant.u_invariant_values.variants.kaplansky_conjecture Kaplansky's conjecture [Kaplansky1953, p sorry line 145 source
Source documentation
Kaplansky's conjecture [Kaplansky1953, p. 202]: the $u$-invariant of a field is a power of $2$ whenever it is finite. Disproved by Merkurjev, who constructed a field of $u$-invariant $6$ [Merkurjev1989] (u_invariant_values.variants.even).

depends on sorry what this means
Statement uses: Iff, False, Nat, KaplanskyUInvariant.IsUInvariant, Exists, Eq, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.kaplansky_conjecture :
    answer(False) ↔ ∀ n, IsUInvariant n → ∃ k, n = 2 ^ k := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.not_three The $u$-invariant is never $3$ [Kaplansky1953, Theorem 2]; see also [Lam2005, Proposition XI.6.8] and [EKM2008, Corollary 36.4] sorry line 152 source
Source documentation
The $u$-invariant is never $3$ [Kaplansky1953, Theorem 2]; see also [Lam2005, Proposition XI.6.8] and [EKM2008, Corollary 36.4].

depends on sorry what this means
Statement uses: Not, KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.not_three : ¬ IsUInvariant 3 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.not_five The $u$-invariant is never $5$ [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4] sorry line 157 source
Source documentation
The $u$-invariant is never $5$ [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4].

depends on sorry what this means
Statement uses: Not, KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.not_five : ¬ IsUInvariant 5 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.not_seven The $u$-invariant is never $7$ [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4] sorry line 162 source
Source documentation
The $u$-invariant is never $7$ [Lam2005, Proposition XI.6.8], [EKM2008, Corollary 36.4].

depends on sorry what this means
Statement uses: Not, KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.not_seven : ¬ IsUInvariant 7 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.two_pow Every power of $2$ is a $u$-invariant [Kaplansky1953, p sorry line 171 source
Source documentation
Every power of $2$ is a $u$-invariant [Kaplansky1953, p. 202]: Theorem 3 of [Kaplansky1953] gives $u(F((t))) = 2u(F)$, so $u(\mathbb{C}((t_1)) \cdots ((t_k))) = 2^k$; see also [EKM2008, §38].

depends on sorry what this means
Statement uses: Nat, KaplanskyUInvariant.IsUInvariant, HPow.hPow, OfNat.ofNat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
10 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.two_pow (k : ℕ) : IsUInvariant (2 ^ k) := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.even Merkurjev's theorem [Merkurjev1991], see also [EKM2008, Theorem 38.4]: every positive even integer is a $u$-invariant sorry line 180 source
Source documentation
Merkurjev's theorem [Merkurjev1991], see also [EKM2008, Theorem 38.4]: every positive even integer is a $u$-invariant. The case $6$, the first counterexample to Kaplansky's conjecture, is [Merkurjev1989].

depends on sorry what this means
Statement uses: Nat, Even, Ne, OfNat.ofNat, KaplanskyUInvariant.IsUInvariant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
4 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.even (n : ℕ) (hn : Even n) (hn₀ : n ≠ 0) :
    IsUInvariant n := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.nine Izhboldin's theorem [Izhboldin2001]: there is a field of $u$-invariant $9$, the first example of an odd $u$-invariant greater than $1$ sorry line 187 source
Source documentation
Izhboldin's theorem [Izhboldin2001]: there is a field of $u$-invariant $9$, the first example of an odd $u$-invariant greater than $1$.

depends on sorry what this means
Statement uses: KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.nine : IsUInvariant 9 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.two_pow_add_one Vishik's theorem [Vishik2009, Corollary 5.2]: for every $r \ge 3$ there is a field of $u$-invariant $2^r + 1$ sorry line 193 source
Source documentation
Vishik's theorem [Vishik2009, Corollary 5.2]: for every $r \ge 3$ there is a field of $u$-invariant $2^r + 1$.

depends on sorry what this means
Statement uses: Nat, LE.le, OfNat.ofNat, KaplanskyUInvariant.IsUInvariant, HAdd.hAdd, HPow.hPow
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
16 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.two_pow_add_one (r : ℕ) (hr : 3 ≤ r) :
    IsUInvariant (2 ^ r + 1) := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.karpenko Karpenko's theorem [Karpenko2026, Theorem 1.1]: if neither $n + 1$ nor $n + 3$ is a power of $2$, then there is a field of $u$-invariant $n$ sorry line 204 source
Source documentation
Karpenko's theorem [Karpenko2026, Theorem 1.1]: if neither $n + 1$ nor $n + 3$ is a power of $2$, then there is a field of $u$-invariant $n$. This covers every positive integer except $1$, $3$, $5$, $7$ and the integers $2^r - 1$, $2^r - 3$ with $r \ge 4$. As of September 2026 the result is a preprint and not yet peer-reviewed.

depends on sorry what this means
Statement uses: Nat, Ne, HPow.hPow, OfNat.ofNat, HAdd.hAdd, KaplanskyUInvariant.IsUInvariant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
14 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.karpenko (n : ℕ) (h₁ : ∀ r, 2 ^ r ≠ n + 1)
    (h₃ : ∀ r, 2 ^ r ≠ n + 3) : IsUInvariant n := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.eleven The special case line 215 source
Source documentation
The special case $n = 11$ of u_invariant_values.variants.karpenko (neither $12$ nor $14$ is a power of $2$), the first odd value not of the form $2^r + 1$ shown to be a $u$-invariant; it was announced in the preprint Fields of $u$-invariant 11 (21 April 2026) that [Karpenko2026] absorbs.

depends on sorry what this means
Statement uses: KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: KaplanskyUInvariant.u_invariant_values.variants.karpenko, Eq, HPow.hPow, HAdd.hAdd, LT.lt, GE.ge, Or, False, Nat.lt_or_ge, dite, LE.le, False.elim, Eq.mp, eq_false_of_decide, Eq.refl, Bool, Bool.false, Eq.symm, le_antisymm, Nat.ge_of_not_lt and 13 more
36 instances, coercions and auxiliary constants left out.

Tactic trace: 9 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.eleven : IsUInvariant 11 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.odd The expectation recorded in [MerkurjevParimala2025, §5.1]: every odd integer $\ge 9$ is a $u$-invariant sorry line 228 source
Source documentation
The expectation recorded in [MerkurjevParimala2025, §5.1]: every odd integer $\ge 9$ is a $u$-invariant. By u_invariant_values.variants.karpenko this is open exactly for the integers $2^r - 1$ and $2^r - 3$ with $r \ge 4$.

depends on sorry what this means
Statement uses: Iff, True, Nat, Odd, LE.le, OfNat.ofNat, KaplanskyUInvariant.IsUInvariant
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
6 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.odd :
    answer(sorry) ↔ ∀ n, Odd n → 9 ≤ n → IsUInvariant n := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.thirteen The smallest open case of the form $2^r - 3$: is there a field of $u$-invariant $13$? sorry line 234 source
Source documentation
The smallest open case of the form $2^r - 3$: is there a field of $u$-invariant $13$?

depends on sorry what this means
Statement uses: Iff, True, KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.thirteen : answer(sorry) ↔ IsUInvariant 13 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant
theorem KaplanskyUInvariant.u_invariant_values.variants.fifteen The smallest open case of the form $2^r - 1$: is there a field of $u$-invariant $15$? sorry line 239 source
Source documentation
The smallest open case of the form $2^r - 1$: is there a field of $u$-invariant $15$?

depends on sorry what this means
Statement uses: Iff, True, KaplanskyUInvariant.IsUInvariant, OfNat.ofNat, Nat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
2 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem u_invariant_values.variants.fifteen : answer(sorry) ↔ IsUInvariant 15 := by
…
```
Mentions: KaplanskyUInvariant.IsUInvariant