38552.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

10 declarations, 4 contain sorry, 0 declared as axioms

Conjectures associated with A038552

A038552 lists the largest squarefree number $k$ such that the imaginary quadratic field $\mathbb{Q}(\sqrt{-k})$ has class number $n$.

The conjectures state that:

All terms are congruent to $19 \pmod{24}$.
This is also the largest absolute value of negative fundamental discriminant $d$ for class number $n$.
For even $n$, if $k$ is the largest odd number with $h(-k) = n$ and $k'$ is the largest even number with $h(-k') = n$, then $k > k'$. Here $h(D)$ is the class number of the quadratic field with discriminant $D$, so $k$ and $k'$ are absolute values of negative fundamental discriminants, not radicands. The source states conjecture 2 in this form.

The squarefree condition in the definition is needed for the maximum to exist, since $\mathbb{Q}(\sqrt{-k}) = \mathbb{Q}(\sqrt{-4k})$.

Conjecture 2 is not a restatement of the definition. Both maxima range over the same imaginary quadratic fields, but they maximize different integers attached to those fields. A038552 uses the squarefree radicand $k$, whereas the discriminant of $\mathbb{Q}(\sqrt{-k})$ is $-k$ for $k \equiv 3 \pmod 4$ and $-4k$ otherwise. The map $k \mapsto |d|$ is not monotone: it sends $2$ to $8$ and $3$ to $3$. So conjecture 2 says that the largest term $k$ satisfies $k \equiv 3 \pmod 4$, and that $4k' \le k$ for every $k' \equiv 1, 2 \pmod 4$ with class number $n$.

References:

[Sta67] Stark, Harold M. "A complete determination of the complex quadratic fields of class-number one." Michigan Mathematical Journal 14.1 (1967): 1-27.
oeis.org/A038552

Imports (1)

FormalConjecturesUtil

def OeisA38552.HasClassNumber The class number of the imaginary quadratic field $\mathbb{Q}(\sqrt{-k})$ equals $n$ line 59 source
Source documentation
The class number of the imaginary quadratic field $\mathbb{Q}(\sqrt{-k})$ equals $n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: Exists, Irreducible, Polynomial, Rat, HAdd.hAdd, HPow.hPow, Polynomial.X, OfNat.ofNat, RingHom, Polynomial.C, Eq, NumberField.classNumber, AdjoinRoot
21 instances, coercions and auxiliary constants left out.
```
def HasClassNumber (k n : ℕ) : Prop :=
…
```
def OeisA38552.IsA038552 $k$ is maximal among squarefree numbers such that $\mathbb{Q}(\sqrt{-k})$ has class number $n$ line 66 source
Source documentation
$k$ is maximal among squarefree numbers such that $\mathbb{Q}(\sqrt{-k})$ has class number $n$. This defines the $n$-th term of A038552.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: MaximalFor, And, Squarefree, OeisA38552.HasClassNumber, id
2 instances, coercions and auxiliary constants left out.
```
def IsA038552 (n k : ℕ) : Prop :=
…
```
def OeisA38552.classNumberOfDiscriminant The class number of the quadratic field with discriminant $d$ line 70 source
Source documentation
The class number of the quadratic field with discriminant $d$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Int, Nat
Proof uses: dite, Irreducible, Polynomial, Rat, HSub.hSub, HPow.hPow, Polynomial.X, OfNat.ofNat, RingHom, Polynomial.C, Classical.dec, NumberField.classNumber, AdjoinRoot, Not
23 instances, coercions and auxiliary constants left out.
```
noncomputable def classNumberOfDiscriminant (d : ℤ) : ℕ :=
…
```
def OeisA38552.IsLargestNegFundDiscrForClassNumber $|d|$ is the largest absolute value among negative fundamental discriminants with class number $n$ line 79 source
Source documentation
$|d|$ is the largest absolute value among negative fundamental discriminants with class number $n$.

standard axioms: Classical.choice, Quot.sound, propext what this means
Statement uses: Nat
Proof uses: IsGreatest, Set.ofPred, And, NumberField.IsFundamentalDiscr, Neg.neg, Int, Eq, OeisA38552.classNumberOfDiscriminant
4 instances, coercions and auxiliary constants left out.
```
def IsLargestNegFundDiscrForClassNumber {n : ℕ} (absD : ℕ) : Prop :=
…
```
theorem OeisA38552.starkHeegner_classNumberOne The Stark-Heegner theorem [Sta67] implies that the squarefree $k > 0$ such that $\mathbb{Q}(\sqrt{-k})$ has class number $1$ are exactly $\{1, 2, 3, 7, 11, 19, 43, 67, 163\}$ sorry line 86 source
Source documentation
The Stark-Heegner theorem [Sta67] implies that the squarefree $k > 0$ such that $\mathbb{Q}(\sqrt{-k})$ has class number $1$ are exactly $\{1, 2, 3, 7, 11, 19, 43, 67, 163\}$.

depends on sorry what this means
Statement uses: Eq, Set, Nat, Set.ofPred, And, Squarefree, OeisA38552.HasClassNumber, OfNat.ofNat, Insert.insert, Singleton.singleton
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
8 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem starkHeegner_classNumberOne :
    {k : ℕ | Squarefree k ∧ HasClassNumber k 1} = {1, 2, 3, 7, 11, 19, 43, 67, 163} := by
…
```
Mentions: OeisA38552.HasClassNumber
theorem OeisA38552.hasClassNumber_163_1 $\mathbb{Q}(\sqrt{-163})$ has class number $1$ line 92 source
Source documentation
$\mathbb{Q}(\sqrt{-163})$ has class number $1$.

depends on sorry what this means
Statement uses: OeisA38552.HasClassNumber, OfNat.ofNat, Nat
Proof uses: Eq, Set, Set.ofPred, And, Squarefree, Insert.insert, Singleton.singleton, OeisA38552.starkHeegner_classNumberOne, And.right, Iff.mpr, Or, Eq.mp, Iff, Eq.trans, Membership.mem, forall_congr, congrArg, of_decide_eq_true, id, Bool and 3 more
11 instances, coercions and auxiliary constants left out.

Tactic trace: 4 steps
Open to load the checked before-and-after goal states.
```
theorem hasClassNumber_163_1 : HasClassNumber 163 1 := by
…
```
Mentions: OeisA38552.HasClassNumber
theorem OeisA38552.isA038552_1_163 $163$ is the largest squarefree $k$ with class number $1$ line 99 source
Source documentation
$163$ is the largest squarefree $k$ with class number $1$.

depends on sorry what this means
Statement uses: OeisA38552.IsA038552, OfNat.ofNat, Nat
Proof uses: And.intro, And, Squarefree, OeisA38552.HasClassNumber, LE.le, id, Nat.Prime.squarefree, Mathlib.Meta.NormNum.isNat_prime_2, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Bool, Bool.true, Mathlib.Meta.NormNum.isNat_minFac_4, Mathlib.Meta.NormNum.IsNat.raw_refl, Mathlib.Meta.NormNum.minFacHelper_3, Bool.false, Mathlib.Meta.NormNum.minFacHelper_2, Mathlib.Meta.NormNum.not_prime_mul_of_ble, Mathlib.Meta.NormNum.minFacHelper_0, OeisA38552.hasClassNumber_163_1 and 14 more
12 instances, coercions and auxiliary constants left out.

Tactic trace: 6 steps
Open to load the checked before-and-after goal states.
```
theorem isA038552_1_163 : IsA038552 1 163 := by
…
```
Mentions: OeisA38552.IsA038552
theorem OeisA38552.mod_24_of_isA038552 All terms of A038552 are congruent to $19 \pmod{24}$ sorry line 117 source
Source documentation
All terms of A038552 are congruent to $19 \pmod{24}$.

depends on sorry what this means
Statement uses: Nat, OeisA38552.IsA038552, Eq, HMod.hMod, OfNat.ofNat
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 mod_24_of_isA038552 {n k : ℕ} (h : IsA038552 n k) : k % 24 = 19 := by
…
```
Mentions: OeisA38552.IsA038552
theorem OeisA38552.isA038552_eq_largestNegFundDisc A038552 also gives the largest absolute value of negative fundamental discriminant for each class number sorry line 123 source
Source documentation
A038552 also gives the largest absolute value of negative fundamental discriminant for each class number.

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

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem isA038552_eq_largestNegFundDisc {n k : ℕ} (h : IsA038552 n k) :
    IsLargestNegFundDiscrForClassNumber (n := n) k := by
…
```
Mentions: OeisA38552.IsA038552, OeisA38552.IsLargestNegFundDiscrForClassNumber
theorem OeisA38552.largestEven_lt_largestOdd_negFundDisc For even class number sorry line 131 source
Source documentation
For even class number $n$, let $k$ be the largest odd number such that the quadratic field with discriminant $-k$ has class number $n$, and let $k'$ be the largest even such number, when they exist. Then $k > k'$.

depends on sorry what this means
Statement uses: Nat, Even, IsGreatest, Set.ofPred, And, Odd, NumberField.IsFundamentalDiscr, Neg.neg, Int, Eq, OeisA38552.classNumberOfDiscriminant, LT.lt
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat
15 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem largestEven_lt_largestOdd_negFundDisc {n k k' : ℕ} (hn : Even n)
    (hk : IsGreatest {m : ℕ | Odd m ∧ IsFundamentalDiscr (-m : ℤ) ∧
      classNumberOfDiscriminant (-m : ℤ) = n} k)
    (hk' : IsGreatest {m : ℕ | Even m ∧ IsFundamentalDiscr (-m : ℤ) ∧
      classNumberOfDiscriminant (-m : ℤ) = n} k') : k' < k := by
…
```
Mentions: OeisA38552.classNumberOfDiscriminant