An executable search for a primitive root of unity modulo p

Mathlib proves that ZMod p contains a primitive k-th root of unity when p is prime and k ∣ p - 1, but the witness comes from the cyclicity of the unit group and cannot be evaluated. An algorithm that works modulo p with a root of unity needs one it can compute. This file supplies TauCeti.ZMod.primitiveRoot?, which tests the residues 0, 1, …, p - 1 in turn and returns the first one that is a primitive k-th root of unity, together with the proof that it is one.

The test is the finite criterion of IsPrimitiveRoot.mk_of_lt: 0 < k, ζ ^ k = 1 and ζ ^ l ≠ 1 for 0 < l < k. It is decidable in ZMod p, so the search runs, and since every residue is tested, for p ≠ 0 and k ≠ 0 the search fails only when there is nothing to find (TauCeti.ZMod.isSome_primitiveRoot?_iff). The criterion deliberately excludes order zero, so the search always fails for k = 0, even though 0 : ZMod p is a primitive 0-th root of unity when p ≠ 1.

Main definitions

• TauCeti.ZMod.primitiveRoot?: for p ≠ 0 and k ≠ 0, the least residue modulo p that is a primitive k-th root of unity, if there is one; always none when k = 0.

Main results

• TauCeti.ZMod.isSome_primitiveRoot?_iff: the search succeeds exactly when ZMod p has a primitive k-th root of unity, for p and k nonzero.
• TauCeti.ZMod.map_val_primitiveRoot?_eq_some_iff: the search returns the least residue passing the criterion, a decidable description of its value.

def TauCeti.ZMod.primitiveRoot? (p k : ℕ) : Option { ζ : ZMod p // IsPrimitiveRoot ζ k }

An executable search for a primitive k-th root of unity in ZMod p. The residues 0, 1, …, p - 1 are tested in increasing order against the criterion ζ ^ k = 1 and ζ ^ l ≠ 1 for 0 < l < k, and the first one that passes is returned with the proof that it is a primitive root. The result is none when no residue passes, in particular when k = 0.

Equations

• TauCeti.ZMod.primitiveRoot? p k = List.findSome? (fun (a : ℕ) => if h : 0 < k ∧ ↑a ^ k = 1 ∧ ∀ l < k, 0 < l → ↑a ^ l ≠ 1 then some ⟨↑a, ⋯⟩ else none) (List.range p)

theorem TauCeti.ZMod.isSome_primitiveRoot?_iff {p k : ℕ} [NeZero p] (hk : k ≠ 0) : (primitiveRoot? p k).isSome = true ↔ ∃ (ζ : ZMod p), IsPrimitiveRoot ζ k

The search finds a primitive root whenever there is one. For p and k nonzero, the search over all residues modulo p succeeds exactly when ZMod p contains a primitive k-th root of unity.

theorem TauCeti.ZMod.map_val_primitiveRoot?_eq_some_iff {p k : ℕ} {ζ : ZMod p} : Option.map Subtype.val (primitiveRoot? p k) = some ζ ↔ ζ.val < p ∧ (0 < k ∧ ζ ^ k = 1 ∧ ∀ l < k, 0 < l → ζ ^ l ≠ 1) ∧ ∀ a < ζ.val, ¬(0 < k ∧ ↑a ^ k = 1 ∧ ∀ l < k, 0 < l → ↑a ^ l ≠ 1)

Which root the search returns. The search returns ζ exactly when ζ passes the criterion ζ ^ k = 1 and ζ ^ l ≠ 1 for 0 < l < k and no smaller residue does; the condition ζ.val < p only fails for p = 0, where there are no residues to test. Every condition is decidable, so a concrete value of the search can be checked without unfolding it.