Finite-field bounds that certify auxiliary root-lifting termination

theorem MIPRE.LowDegree.BinaryPolynomial.card_adjoinRoot_binary (f : Polynomial (ZMod 2)) (hf : f.Monic) : Nat.card (AdjoinRoot f) = 2 ^ f.natDegree

Canonical quotient coordinates determine the binary quotient cardinality.

theorem MIPRE.LowDegree.BinaryPolynomial.primitive_root_order_dvd_card (f : Polynomial (ZMod 2)) (hf : f.Monic) (hi : Irreducible f) (n : ℕ) (hn : n ≠ 0) (hr : IsPrimitiveRoot (AdjoinRoot.root f) n) : n ∣ 2 ^ f.natDegree - 1

The primitive order of a binary root divides its field's multiplicative cardinality.

theorem MIPRE.LowDegree.BinaryPolynomial.prime_power_lift_bound (f : Polynomial (ZMod 2)) (hf : f.Monic) (hi : Irreducible f) (q s : ℕ) (hq : Nat.Prime q) (hr : IsPrimitiveRoot (AdjoinRoot.root f) (q ^ s)) : s ≤ f.natDegree

An odd prime cannot be lifted more often than the auxiliary binary degree.