An internally proved quadratic class-group descent estimate. The unit obstruction, invariant-ideal decomposition, and finite discriminant-prime cover are all constructed in the preceding modules. The resulting discriminant-prime coefficient is sufficient for subpower absorption; no sharp relative-discriminant genus formula is asserted.

The degree-one base case for descent on the number-field degree. The ring of integers is identified with the integers, so its class group and its two-torsion subgroup are trivial.

theorem CCDN.classGroupTwoTorsionCard_eq_one_of_degree_one (K : Type u_1) [Field K] [NumberField K] (hd : Module.finrank ℚ K = 1) : classGroupTwoTorsionCard K = 1

A number field of degree one over ℚ has trivial two-torsion in its class group.

theorem CCDN.quadratic_classGroupTwoTorsion_descent (F : Type u_1) (K : Type u_2) [Field F] [Field K] [NumberField F] [NumberField K] [Algebra F K] (hd : Module.finrank F K = 2) : classGroupTwoTorsionCard K ≤ (classGroupTwoTorsionCard F * 2 ^ (Module.finrank ℚ K * (NumberField.discr K).natAbs.primeFactors.card + Module.finrank ℚ F)) ^ 2

For a quadratic extension K / F of number fields, h₂(K) ≤ (h₂(F) * 2 ^ ([K : ℚ] * ω(discr K) + [F : ℚ])) ^ 2, where ω counts distinct prime factors; the term [F : ℚ] accounts for the unit-norm obstruction.

theorem CCDN.quadratic_field_classGroupTwoTorsionCard_le (K : Type u_1) [Field K] [NumberField K] (hd : Module.finrank ℚ K = 2) : classGroupTwoTorsionCard K ≤ 2 ^ (4 * (NumberField.discr K).natAbs.primeFactors.card + 2)

A quadratic number field K satisfies h₂(K) ≤ 2 ^ (4 * ω(discr K) + 2), where ω counts distinct prime factors; this is subpower in the discriminant.