Balanced square generators for two-torsion ideal classes. The anisotropic Minkowski argument is applied to the inverse ideal; the rescaling retains the exact generator needed for bounds at every place.

theorem CCDN.numberField_discriminant_natAbs_cast (K : Type u_1) [Field K] [NumberField K] : ↑(NumberField.discr K).natAbs = |↑(NumberField.discr K)|

The absolute discriminant, as the absolute value of an integer cast to ℕ and to ℝ.

theorem CCDN.numberField_discriminant_natAbs_pos (K : Type u_1) [Field K] [NumberField K] : 0 < (NumberField.discr K).natAbs

The absolute discriminant (discr K).natAbs of a number field is positive.

theorem CCDN.one_le_abs_discr (K : Type u_1) [Field K] [NumberField K] : 1 ≤ |↑(NumberField.discr K)|

The absolute discriminant of a number field is at least 1.

theorem CCDN.three_le_abs_discr (K : Type u_1) [Field K] [NumberField K] (hn : 2 ≤ Module.finrank ℚ K) : 3 ≤ |↑(NumberField.discr K)|

A number field of degree at least 2 over ℚ has absolute discriminant at least 3.

theorem CCDN.one_le_log_abs_discr (K : Type u_1) [Field K] [NumberField K] (hn : 2 ≤ Module.finrank ℚ K) : 1 ≤ Real.log |↑(NumberField.discr K)|

A number field of degree at least 2 over ℚ has logarithmic absolute discriminant log |discr K| ≥ 1.

theorem CCDN.exists_balanced_square_generator_of_radius (K : Type u_1) [Field K] [NumberField K] (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) {α : NumberField.RingOfIntegers K} (hα : α ≠ 0) (hIα : ↑I ^ 2 = Ideal.span {α}) (T : NNReal) (hT : 2 ^ Module.finrank ℚ K * √|↑(NumberField.discr K)| < ↑T ^ Module.finrank ℚ K) : ∃ (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))) (β : NumberField.RingOfIntegers K), ClassGroup.mk0 J = ClassGroup.mk0 I ∧ β ≠ 0 ∧ ↑J ^ 2 = Ideal.span {β} ∧ ∀ (w : NumberField.InfinitePlace K), w ↑β < ↑T ^ 2

The anisotropic Minkowski step, with the radius left explicit.

theorem CCDN.exists_injective_balanced_two_torsion_generators (K : Type u_1) [Field K] [NumberField K] : ∃ (β : ↥(classGroupTwoTorsion K) → NumberField.RingOfIntegers K), Function.Injective β ∧ ∀ (c : ↥(classGroupTwoTorsion K)), β c ≠ 0 ∧ (∀ (w : NumberField.InfinitePlace K), w ↑(β c) < 9 * |↑(NumberField.discr K)| ^ (1 / ↑(Module.finrank ℚ K))) ∧ ∃ (J : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ClassGroup.mk0 J = ↑c ∧ ↑J ^ 2 = Ideal.span {β c} ∧ ((Algebra.norm ℤ) (β c)).natAbs = Ideal.absNorm ↑J ^ 2

The bounded generators can be chosen injectively; equality of generators forces equality of the corresponding ideals and hence of their ideal classes.