Class number one from a small discriminant

Minkowski's bound, in the form of Mathlib's NumberField.RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt, makes 𝓞 K a principal ideal domain as soon as |discr K| < (2 (π/4)^{r₂} nⁿ/n!)², where n = [K : ℚ] and r₂ is the number of complex places. In degree two the right-hand side is 16 for r₂ = 0 and π² > 9 for r₂ = 1; in degree three it is 81 for r₂ = 0 and (9π/4)² > 49 for r₂ = 1. This file records the integer thresholds: a quadratic field with |discr K| ≤ 9, a real quadratic field with |discr K| ≤ 15, and a cubic field with |discr K| ≤ 49 have class number 1.

The proofs follow the pattern of Mathlib's IsCyclotomicExtension.Rat.three_pid and five_pid in Mathlib.NumberTheory.NumberField.Cyclotomic.PID, with the discriminant bounded by an integer instead of computed; the two signature-independent results split into the cases r₂ = 0 and r₂ = 1, and the real quadratic result fixes r₂ = 0.

Main results

• TauCeti.NumberField.isPrincipalIdealRing_of_finrank_eq_two_of_natAbs_discr_le_nine: a quadratic field with |discr K| ≤ 9 has 𝓞 K a principal ideal domain.
• isPrincipalIdealRing_of_finrank_eq_two_of_nrComplexPlaces_eq_zero_of_natAbs_discr_le_fifteen (in the same namespace): a real quadratic field with |discr K| ≤ 15 has 𝓞 K a principal ideal domain.
• TauCeti.NumberField.isPrincipalIdealRing_of_finrank_eq_three_of_natAbs_discr_le_forty_nine: a cubic field with |discr K| ≤ 49 has 𝓞 K a principal ideal domain.

theorem TauCeti.NumberField.isPrincipalIdealRing_of_finrank_eq_two_of_natAbs_discr_le_nine {K : Type u_1} [Field K] [NumberField K] (hfin : Module.finrank ℚ K = 2) (hdisc : (NumberField.discr K).natAbs ≤ 9) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

Quadratic fields of discriminant at most 9 in absolute value have class number 1. Minkowski's bound (4/π)^{r₂} · √|discr K| / 2 is below 2 when |discr K| < 16 for real K and when |discr K| < π² for imaginary K; 9 is below both thresholds.

theorem TauCeti.NumberField.isPrincipalIdealRing_of_finrank_eq_two_of_nrComplexPlaces_eq_zero_of_natAbs_discr_le_fifteen {K : Type u_1} [Field K] [NumberField K] (hfin : Module.finrank ℚ K = 2) (hr : NumberField.InfinitePlace.nrComplexPlaces K = 0) (hdisc : (NumberField.discr K).natAbs ≤ 15) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

Real quadratic fields of discriminant at most 15 have class number 1. Minkowski's bound √|discr K| / 2 is below 2 when |discr K| < 16.

theorem TauCeti.NumberField.isPrincipalIdealRing_of_finrank_eq_three_of_natAbs_discr_le_forty_nine {K : Type u_1} [Field K] [NumberField K] (hfin : Module.finrank ℚ K = 3) (hdisc : (NumberField.discr K).natAbs ≤ 49) : IsPrincipalIdealRing (NumberField.RingOfIntegers K)

Cubic fields of discriminant at most 49 in absolute value have class number 1. Minkowski's bound (4/π)^{r₂} · (2/9) · √|discr K| is below 2 when |discr K| < 81 for totally real K and when |discr K| < (9π/4)² for K with a complex place; 49 is below both thresholds.