Uniform control of the unit contribution to quadratic descent. Dirichlet's theorem and cyclicity of roots of unity give at most one binary choice per free unit and one further binary choice for torsion. The endpoint concerns the unit group modulo squares.

theorem CCDN.numberFieldUnit_exponent_two_quotient (K : Type u_1) [Field K] [NumberField K] {G : Type u_2} [CommGroup G] (φ : (NumberField.RingOfIntegers K)ˣ →* G) (hφ : Function.Surjective ⇑φ) (hG : ∀ (x : G), x ^ 2 = 1) : Finite G ∧ Nat.card G ≤ 2 ^ (NumberField.Units.rank K + 1)

Every exponent-two quotient of the unit group has cardinality at most 2^(unit rank + 1). The finite parametrization is constructed from a torsion generator and a fundamental system of units.

theorem CCDN.numberField_unit_rank_add_one_le_degree (K : Type u_1) [Field K] [NumberField K] : NumberField.Units.rank K + 1 ≤ Module.finrank ℚ K

The unit rank of a number field plus one is at most its degree over ℚ.