Elimination certificates for fundamental units

A certificate eliminates each polynomial in unitCandidates K B either by excluding real roots in (1, B) or by excluding it as the minimal polynomial of an integral primitive element of K. The field test can be discharged by the index–discriminant formula. These are proofs of the tests, not Boolean assertions about an unchecked root-finding procedure.

In a number field of prime degree and unit rank one, a certificate excludes every unit in the selected real interval. With B = w u > 1, normalization then proves that u generates the units modulo torsion. The certificate does not depend on a choice of real place: the root test excludes all real roots in the interval, and soundness can be applied at any real place.

References

• H. Cohen, A Course in Computational Algebraic Number Theory, §5.7, for unit search.
• J. Neukirch, Algebraic Number Theory, Chapter I, §2, for the index–discriminant formula.

def TauCeti.NumberField.Units.UnitCandidateEliminationCertificate (K : Type u_2) [Field K] [NumberField K] (B : ℝ) : Prop

Every candidate polynomial is excluded either by its real roots in (1, B) or as a minimal polynomial of an integral primitive element of K.

@[simp]

theorem TauCeti.NumberField.Units.unitCandidateEliminationCertificate_iff {K : Type u_1} [Field K] [NumberField K] (B : ℝ) : UnitCandidateEliminationCertificate K B ↔ ∀ f ∈ unitCandidates K B, (∀ x ∈ Set.Ioo 1 B, (Polynomial.aeval x) f ≠ 0) ∨ ∀ (θ : IntegralPrimitiveElement K), minpoly ℤ ↑θ ≠ f

The two possible proofs carried by an elimination certificate for each candidate.

theorem TauCeti.NumberField.Units.UnitCandidateEliminationCertificate.of_discr {K : Type u_1} [Field K] [NumberField K] {B : ℝ} (h : ∀ f ∈ unitCandidates K B, (∀ x ∈ Set.Ioo 1 B, (Polynomial.aeval x) f ≠ 0) ∨ ∀ (n : ℕ), 0 < n → f.discr ≠ ↑n ^ 2 * NumberField.discr K) : UnitCandidateEliminationCertificate K B

Construct a certificate using real-root exclusions and the obstruction that a primitive minimal polynomial must have discriminant equal to the field discriminant times a positive integer square.

theorem TauCeti.NumberField.Units.UnitCandidateEliminationCertificate.no_unit_between_real {K : Type u_1} [Field K] [NumberField K] {B : ℝ} (h : UnitCandidateEliminationCertificate K B) (hr : NumberField.Units.rank K = 1) (hp : Nat.Prime (Module.finrank ℚ K)) {w : NumberField.InfinitePlace K} (hw : w.IsReal) : ¬∃ (v : (NumberField.RingOfIntegers K)ˣ), 1 < (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) ∧ (NumberField.InfinitePlace.embedding_of_isReal hw) ((algebraMap (NumberField.RingOfIntegers K) K) ↑v) < B

A certificate excludes all units with real image strictly between 1 and B, provided the unit rank is one and the field degree is prime.

theorem TauCeti.NumberField.Units.UnitCandidateEliminationCertificate.sound {K : Type u_1} [Field K] [NumberField K] {u : (NumberField.RingOfIntegers K)ˣ} {w : NumberField.InfinitePlace K} (h : UnitCandidateEliminationCertificate K (w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u))) (hr : NumberField.Units.rank K = 1) (hp : Nat.Prime (Module.finrank ℚ K)) (hw : w.IsReal) (hu : 1 < w ((algebraMap (NumberField.RingOfIntegers K) K) ↑u)) : Subgroup.closure {u} ⊔ NumberField.Units.torsion K = ⊤

Soundness of unit-candidate elimination. A unit expanding at a real place generates modulo torsion if every candidate below its absolute value has been eliminated.