noncomputable def FiniteFieldArith.bitSize (n : ℕ) : ℕ

The bit-size of a natural number n, defined as ⌊log₂ n⌋ + 1. This is the number of bits in the standard binary representation and serves as the cost parameter n = lg q used throughout Sutherland's complexity analyses.

noncomputable def FiniteFieldArith.fpAddBitOps (p : ℕ) : ℕ

Bit-operation cost of addition/subtraction in 𝔽_p: linear in the bit-size of p. The constant 3 is a small fixed overhead for carry propagation.

noncomputable def FiniteFieldArith.fqAddBitOps (p d : ℕ) : ℕ

Bit-operation cost of addition in 𝔽_q = 𝔽_{p^d}: d independent additions in 𝔽_p, one per coefficient of the polynomial-basis representation.

theorem FiniteFieldArith.fq_add_cost_is_sum_over_coefficients (p d : ℕ) : ∑ _i : Fin d, fpAddBitOps p = fqAddBitOps p d

The cost of adding in 𝔽_q is the sum of the per-coordinate costs in 𝔽_p, i.e. ∑_{i < d} fpAddBitOps p = fqAddBitOps p d.

@[simp]

theorem FiniteFieldArith.fqAddBitOps_def (p d : ℕ) : fqAddBitOps p d = d * (3 * (Nat.log 2 p + 1))

Definitional unfolding of fqAddBitOps: fqAddBitOps p d = d · (3 · (⌊log₂ p⌋ + 1)).

theorem FiniteFieldArith.d_mul_log_le (p d : ℕ) (hp : 2 ≤ p) : d * Nat.log 2 p ≤ Nat.log 2 (p ^ d)

For p ≥ 2, d · log₂ p ≤ log₂(p^d). Used to bound costs over extension fields in terms of the bit-size of q = p^d.

theorem FiniteFieldArith.d_le_log_pow (p d : ℕ) (hp : 2 ≤ p) : d ≤ Nat.log 2 (p ^ d)

For p ≥ 2, d ≤ log₂(p^d). A simple monotonicity bound.

theorem FiniteFieldArith.d_mul_bitSize_le (p d : ℕ) (hp : 2 ≤ p) : d * bitSize p ≤ 2 * bitSize (p ^ d)

For p ≥ 2, d · bitSize p ≤ 2 · bitSize (p^d). This is the absorbing inequality used to compare per-𝔽_p and per-𝔽_q cost contributions.

theorem FiniteFieldArith.fq_add_bitOps_linear (p d : ℕ) (hp : Nat.Prime p) : fqAddBitOps p d ≤ 6 * bitSize (p ^ d)

Linear-in-bitSize (p^d) bound on the cost of addition in 𝔽_q: fqAddBitOps p d ≤ 6 · bitSize(p^d). This is the key inequality behind Theorem 3.24.

noncomputable def FiniteFieldArith.fqSubBitOps (p d : ℕ) : ℕ

Bit-operation cost of subtraction in 𝔽_q: identical to addition.

theorem FiniteFieldArith.fq_sub_bitOps_linear (p d : ℕ) (hp : Nat.Prime p) : fqSubBitOps p d ≤ 6 * bitSize (p ^ d)

Linear bound for subtraction in 𝔽_q, mirroring fq_add_bitOps_linear.

theorem FiniteFieldArith.fq_add_complexity_linear : ∃ (C : ℕ), ∀ (p d : ℕ), Nat.Prime p → fqAddBitOps p d ≤ C * bitSize (p ^ d)

Theorem 3.24 (formal statement): addition in 𝔽_q runs in O(n) bit operations where n = lg q. Existence of a universal constant C (here C = 6) such that fqAddBitOps p d ≤ C · bitSize(p^d) for all primes p and all d.

noncomputable def DFT {R : Type u_1} [CommRing R] (ω : R) (n : ℕ) (f : Polynomial R) : Fin n → R

The discrete Fourier transform DFT_ω(f)(i) := f(ω^i) at an element ω ∈ R of order dividing n, returned as a function Fin n → R. Appears in Theorem 3.29 / Theorem 3.30.

noncomputable def cyclicConv {R : Type u_1} [CommRing R] (n : ℕ) (f g : Polynomial R) : Polynomial R

The cyclic convolution (f * g) mod (X^n − 1). Used as the polynomial-level operation diagonalised by the DFT in Theorem 3.29.

@[simp]

theorem DFT_apply {R : Type u_1} [CommRing R] (ω : R) (n : ℕ) (f : Polynomial R) (i : Fin n) : DFT ω n f i = Polynomial.eval (ω ^ ↑i) f

Definitional simp lemma: DFT_ω(f)(i) = f(ω^i).

@[simp]

theorem cyclicConv_def {R : Type u_1} [CommRing R] (n : ℕ) (f g : Polynomial R) : cyclicConv n f g = f * g %ₘ (Polynomial.X ^ n - 1)

Definitional simp lemma: cyclicConv n f g = (f · g) mod (X^n − 1).

theorem eval_modByMonic_eq_eval {R : Type u_1} [CommRing R] (p m : Polynomial R) (a : R) (hroot : m.IsRoot a) : Polynomial.eval a (p %ₘ m) = Polynomial.eval a p

If a is a root of the monic divisor m, then evaluating (p mod m) at a is the same as evaluating p at a. Used to identify DFT of a cyclic convolution with the pointwise product.

theorem isRoot_X_pow_sub_one {R : Type u_1} [CommRing R] {ω : R} {n : ℕ} (hω : ω ^ n = 1) (i : ℕ) : (Polynomial.X ^ n - 1).IsRoot (ω ^ i)

If ω^n = 1, then every power ω^i is a root of X^n − 1.

theorem dft_cyclicConv {R : Type u_1} [CommRing R] (ω : R) (n : ℕ) (f g : Polynomial R) (hω : ω ^ n = 1) : DFT ω n (cyclicConv n f g) = DFT ω n f * DFT ω n g

Theorem 3.29: when ω^n = 1, the DFT diagonalises cyclic convolution, i.e. DFT_ω(f * g mod X^n − 1) = DFT_ω(f) · DFT_ω(g) pointwise.

noncomputable def polyFirstHalf {R : Type u_1} [CommRing R] (m : ℕ) (f : Polynomial R) : Polynomial R

The "first half" of a polynomial f: the truncation ∑_{j < m} c_j X^j of f to degree < m.

noncomputable def polySecondHalf {R : Type u_1} [CommRing R] (m : ℕ) (f : Polynomial R) : Polynomial R

The "second half" of a polynomial f: the coefficient sequence (f_m, f_{m+1}, …, f_{2m−1}) repackaged as a degree-< m polynomial.

noncomputable def fftTwistedDiff {R : Type u_1} [CommRing R] (ω : R) (m : ℕ) (f : Polynomial R) : Polynomial R

The twisted-difference polynomial s_f(ω, m) := ∑_{j < m} (f_j − f_{m+j}) ω^j X^j that appears in the recursive FFT identity for odd-indexed DFT values.

noncomputable def fft {R : Type u_1} [CommRing R] (ω : R) (n : ℕ) : Polynomial R → Fin (2 ^ n) → R

The radix-2 FFT (cf. Theorem 3.30): given a primitive 2^n-th root of unity ω, recursively computes DFT_ω(f)(i) for all i < 2^n using O(n · 2^n) ring operations.

def IsPrim2PowRoot {R : Type u_1} [CommRing R] (ω : R) : ℕ → Prop

Predicate: ω is a primitive 2^n-th root of unity in the radix-2 sense, i.e. ω^(2^(n−1)) = −1 (with the convention that the n = 0 case is trivial). This is the hypothesis under which the recursive FFT identities hold.

theorem isPrim2PowRoot_sq {R : Type u_1} [CommRing R] {n : ℕ} {ω : R} (h : IsPrim2PowRoot ω (n + 1)) : IsPrim2PowRoot (ω ^ 2) n

If ω is a primitive 2^(n+1)-th root of unity, then ω² is a primitive 2^n-th root of unity. Drives the recursion of the FFT.

theorem isPrim2PowRoot_pow_eq_one {R : Type u_1} [CommRing R] {n : ℕ} {ω : R} (h : IsPrim2PowRoot ω (n + 1)) : ω ^ 2 ^ (n + 1) = 1

If ω is a primitive 2^(n+1)-th root of unity (i.e. ω^(2^n) = −1), then ω^(2^(n+1)) = 1.

theorem natDegree_sum_C_X_pow_lt {R : Type u_1} [CommRing R] {m : ℕ} (hm : 0 < m) (c : ℕ → R) : (∑ j ∈ Finset.range m, Polynomial.C (c j) * Polynomial.X ^ j).natDegree < m

A ∑_{j < m} C(c_j) X^j polynomial has natural degree strictly less than m (for m > 0). Bounds the degrees of the recursive subpolynomials in the FFT.

theorem fftTwistedDiff_eval {R : Type u_1} [CommRing R] (ω : R) (m : ℕ) (f : Polynomial R) (x : R) : Polynomial.eval x (fftTwistedDiff ω m f) = Polynomial.eval (ω * x) (polyFirstHalf m f - polySecondHalf m f)

Evaluation rule for the twisted-difference polynomial: (fftTwistedDiff ω m f)(x) = ((firstHalf − secondHalf))(ω · x).

theorem poly_split_eval {R : Type u_1} [CommRing R] (m : ℕ) (f : Polynomial R) (hf : f.natDegree < 2 * m) (x : R) : Polynomial.eval x f = Polynomial.eval x (polyFirstHalf m f) + x ^ m * Polynomial.eval x (polySecondHalf m f)

Splitting identity: if deg f < 2m, then f(x) = firstHalf(x) + x^m · secondHalf(x).

theorem fft_even_identity {R : Type u_1} [CommRing R] (ω : R) (m : ℕ) (f : Polynomial R) (hf : f.natDegree < 2 * m) (hω : ω ^ (2 * m) = 1) (i : ℕ) : Polynomial.eval (ω ^ (2 * i)) f = Polynomial.eval ((ω ^ 2) ^ i) (polyFirstHalf m f + polySecondHalf m f)

Even-index FFT identity: under ω^(2m) = 1 and deg f < 2m, the value f(ω^{2i}) equals (firstHalf + secondHalf)((ω²)^i).

theorem fft_odd_identity {R : Type u_1} [CommRing R] (ω : R) (m : ℕ) (f : Polynomial R) (hf : f.natDegree < 2 * m) (hωm : ω ^ m = -1) (i : ℕ) : Polynomial.eval (ω ^ (2 * i + 1)) f = Polynomial.eval ((ω ^ 2) ^ i) (fftTwistedDiff ω m f)

Odd-index FFT identity: under ω^m = −1 and deg f < 2m, the value f(ω^{2i+1}) equals (fftTwistedDiff ω m f)((ω²)^i).

theorem fft_eq_DFT {R : Type u_1} [CommRing R] (ω : R) (n : ℕ) (f : Polynomial R) (hprim : IsPrim2PowRoot ω n) (hdeg : f.natDegree < 2 ^ n) : fft ω n f = DFT ω (2 ^ n) f

Theorem 3.30 (correctness of the FFT): if ω is a primitive 2^n-th root of unity and deg f < 2^n, then fft ω n f equals DFT_ω(f) on all of Fin (2^n).

def fftOpCount (k : ℕ) : ℕ

Operation count 5 · 2^k · k for one radix-2 FFT of size 2^k (Theorem 3.30).

def pointwiseMulOpCount (n : ℕ) : ℕ

Operation count n for pointwise multiplication of two n-vectors.

def computePowersOpCount (n : ℕ) : ℕ

Operation count n for computing n consecutive powers of an element.

def scalarMulOpCount (n : ℕ) : ℕ

Operation count 2n for scalar multiplication of an n-vector.

def fftPolyMulCost (k : ℕ) : ℕ

Total operation count for FFT-based polynomial multiplication at size 2^k: three FFTs plus pointwise multiplication, twiddle-power generation, and scalar multiplications. This is the operation budget behind Corollary 3.31.

theorem fftPolyMulCost_le (k : ℕ) : fftPolyMulCost k ≤ 20 * 2 ^ k * (k + 1)

Quantitative form of Corollary 3.31: the FFT polynomial-multiplication cost at size 2^k is bounded by 20 · 2^k · (k+1) = O(n log n).

theorem cyclicConv_eq_mul {R : Type u_1} [CommRing R] [Nontrivial R] (n : ℕ) (hn : 0 < n) (f g : Polynomial R) (hdeg : (f * g).natDegree < n) : cyclicConv n f g = f * g

If deg(f · g) < n, then the cyclic convolution (f · g) mod (X^n − 1) is just f · g. This is the soundness step letting one recover the full product from a single cyclic convolution by padding the input length.

theorem fft_poly_mul_complexity (R : Type u_2) [CommRing R] (k : ℕ) (ω : R) (hprim : IsPrim2PowRoot ω (k + 1)) (hunit : IsUnit 2) (f g : Polynomial R) (hf : f.natDegree < 2 ^ k) (hg : g.natDegree < 2 ^ k) : cyclicConv (2 ^ (k + 1)) f g = f * g ∧ DFT ω (2 ^ (k + 1)) (f * g) = DFT ω (2 ^ (k + 1)) f * DFT ω (2 ^ (k + 1)) g ∧ IsUnit (2 ^ (k + 1)) ∧ fftPolyMulCost (k + 1) ≤ 20 * 2 ^ (k + 1) * (k + 1 + 1)

Corollary 3.31 (full statement): over a commutative ring R containing a primitive 2^(k+1)-th root of unity ω with 2 invertible, two polynomials of degree < 2^k can be multiplied as a cyclic convolution, the DFT diagonalises the multiplication, 2^(k+1) is invertible (needed for the inverse FFT), and the total cost is O(n log n) = 20 · 2^(k+1) · (k+2).

def FiniteFieldArith.bitlength (n : ℕ) : ℕ

Bit-length of a natural number n, using Nat.size. Equivalent to bitSize but defined in terms of the standard library Nat.size.

theorem FiniteFieldArith.fp_repr_bitlength_le (p : ℕ) [NeZero p] (a : ZMod p) : bitlength a.val ≤ bitlength p

Bit-length of any element of 𝔽_p (in its canonical representative a ∈ {0, …, p − 1}) is at most the bit-length of p.

theorem FiniteFieldArith.fp_mul_repr_bitlength_le (p : ℕ) [NeZero p] (a b : ZMod p) : bitlength (a.val * b.val) ≤ 2 * bitlength p

The integer product of two 𝔽_p-representatives fits in at most 2 · bitlength p bits. Used to bound the input size of modular reduction in 𝔽_p multiplication.

def FiniteFieldArith.modReductionCost (intMulCost : ℕ → ℕ) (n : ℕ) : ℕ

Cost model for modular reduction by an n-bit modulus using Newton-iteration based fast division: 3 · M(n) + n where M(n) = intMulCost n.

theorem FiniteFieldArith.modReductionCost_le (intMulCost : ℕ → ℕ) (hM_ge_id : ∀ (n : ℕ), n ≤ intMulCost n) (n : ℕ) : modReductionCost intMulCost n ≤ 4 * intMulCost n

Bound modReductionCost(n) ≤ 4 · M(n) whenever the multiplication cost M dominates the identity (i.e. M(n) ≥ n).

def FiniteFieldArith.fpMulCost (intMulCost : ℕ → ℕ) (p : ℕ) : ℕ

Cost of multiplication in 𝔽_p: one integer multiplication plus one modular reduction, both of bit-length bitlength p.

theorem FiniteFieldArith.fp_mul_cost_is_O_intMulCost (intMulCost : ℕ → ℕ) (hM_ge_id : ∀ (n : ℕ), n ≤ intMulCost n) : ∃ (C : ℕ), ∀ (p : ℕ), fpMulCost intMulCost p ≤ C * intMulCost (bitlength p)

Theorem 3.33: multiplication in 𝔽_p takes O(M(n)) bit operations where n = lg p (here packaged as the existence of a constant C = 5 such that fpMulCost p ≤ 5 · M(bitlength p)).

def FiniteFieldArith.schoolbookMulCost (n : ℕ) : ℕ

Schoolbook (quadratic) integer-multiplication cost: M(n) = n².

@[irreducible]

def FiniteFieldArith.halfGcdCost (M : ℕ → ℕ) : ℕ → ℕ

Recursive cost model for the half-GCD algorithm (Lehmer / Knuth-Schönhage): H(n+1) = 2 · H((n+1)/2) + M(n+1) with H(0) = 0. Underlies the O(M(n) log n) complexity of fast Euclidean algorithms.

theorem FiniteFieldArith.halfGcdCost_le (M : ℕ → ℕ) : (∀ (a b : ℕ), a ≤ b → M a ≤ M b) → ∃ (C : ℕ), ∀ (n : ℕ), halfGcdCost M n ≤ C * M n * (Nat.log 2 n + 1)

Master-recurrence bound for the half-GCD cost: for monotone multiplication cost M, there is a constant C such that halfGcdCost M n ≤ C · M(n) · (log₂ n + 1).

def FiniteFieldArith.fpInvCost (intMulCost : ℕ → ℕ) (n : ℕ) : ℕ

Cost of inversion in 𝔽_p for an n-bit prime: implemented via the half-GCD extended Euclidean algorithm.

theorem FiniteFieldArith.fp_inversion_complexity (intMulCost : ℕ → ℕ) (hM_mono : ∀ (a b : ℕ), a ≤ b → intMulCost a ≤ intMulCost b) : ∃ (C : ℕ), ∀ (p : ℕ), Nat.Prime p → have n := bitlength p; fpInvCost intMulCost n ≤ C * intMulCost n * (Nat.log 2 n + 1)

Theorem 3.40: inversion in 𝔽_p^× takes O(M(n) · log n) bit operations where n = lg p. Formalised as existence of a constant C with the asymptotic bound for every prime p.

def FiniteFieldArith.LogEBoundedByLogP (K p e : ℕ) : Prop

The size-restriction hypothesis log₂ e = O(log₂ p) used in Theorems 3.35 and 3.41, controlling how large the extension degree e can be relative to the base prime.

def FiniteFieldArith.polyGcdCost (polyMulCost : ℕ → ℕ) (n : ℕ) : ℕ

Cost of computing polynomial GCDs at length n, using the half-GCD algorithm instantiated with a given polynomial-multiplication cost.

noncomputable def FiniteFieldArith.fqInvCost (intMulCost : ℕ → ℕ) (p e : ℕ) : ℕ

Cost model for inversion in 𝔽_q = 𝔽_{p^e}: the Kronecker substitution converts polynomial inversion into integer inversion of bit-width e · (bitSize p + bitSize e), then a half-GCD-based integer inversion gives the final O(M(n) log n) bound.

theorem FiniteFieldArith.bitSize_pow_ge_e (p e : ℕ) (hp : 2 ≤ p) : e ≤ bitSize (p ^ e)

For p ≥ 2, the bit-size of p^e is at least e. Useful to express the cost bounds in Theorems 3.35 / 3.41 purely in terms of n = bitSize(p^e).

theorem FiniteFieldArith.fqInvCost_kb_le (p e K : ℕ) (hp : 2 ≤ p) (hlog : LogEBoundedByLogP K p e) : e * (bitSize p + bitSize e) ≤ (2 * K + 5) * bitSize (p ^ e)

Under the hypothesis LogEBoundedByLogP K p e, the Kronecker bit-width e · (bitSize p + bitSize e) used in fqInvCost is bounded by (2K + 5) · bitSize(p^e), i.e. linear in n = lg q.

theorem FiniteFieldArith.fq_inversion_complexity (intMulCost : ℕ → ℕ) (K : ℕ) (_hM_ge_id : ∀ (n : ℕ), n ≤ intMulCost n) (hM_mono : ∀ (a b : ℕ), a ≤ b → intMulCost a ≤ intMulCost b) : ∃ (C : ℕ), ∀ (p e : ℕ), Nat.Prime p → 0 < e → LogEBoundedByLogP K p e → fqInvCost intMulCost p e ≤ C * intMulCost (C * bitSize (p ^ e)) * (Nat.log 2 (bitSize (p ^ e)) + 1)

Theorem 3.41: assuming log e = O(log p) and an M-regular multiplication cost, inversion in 𝔽_q^× runs in O(M(n) log n) = O(n log² n) bit operations where n = lg q.

noncomputable def FiniteFieldArith.kroneckerBitWidth (p e : ℕ) : ℕ

Bit-width of the Kronecker substitution used to reduce multiplication in 𝔽_{p^e} to a single integer multiplication: e · (2 · bitSize p + bitSize e).

noncomputable def FiniteFieldArith.fqMulCost (intMulCost : ℕ → ℕ) (p e : ℕ) : ℕ

Cost model for multiplication in 𝔽_q = 𝔽_{p^e} via Kronecker substitution: one integer multiplication of bit-width kroneckerBitWidth p e, plus a coefficient extraction step costing kroneckerBitWidth p e bit operations.

theorem FiniteFieldArith.kronecker_bitWidth_le (p e K : ℕ) (hp : 2 ≤ p) (hlog : LogEBoundedByLogP K p e) : kroneckerBitWidth p e ≤ (2 * K + 5) * bitSize (p ^ e)

Under LogEBoundedByLogP K p e, the Kronecker bit-width e · (2 bitSize p + bitSize e) is bounded linearly by (2K + 5) · bitSize(p^e).

theorem FiniteFieldArith.fq_mul_complexity (intMulCost : ℕ → ℕ) (p e : ℕ) [Fact (Nat.Prime p)] (_he : 0 < e) (hM_ge_id : ∀ (n : ℕ), n ≤ intMulCost n) (hM_mono : ∀ (a b : ℕ), a ≤ b → intMulCost a ≤ intMulCost b) (K : ℕ) (hlog : LogEBoundedByLogP K p e) (C_reg : ℕ) (hM_reg : ∀ (n : ℕ), intMulCost ((2 * K + 5) * n) ≤ C_reg * intMulCost n) : ∃ (C : ℕ), fqMulCost intMulCost p e ≤ C * intMulCost (bitSize (p ^ e))

Theorem 3.35: multiplication in 𝔽_q runs in O(M(n)) = O(n log n) bit operations, where n = lg q, under the size hypothesis log e = O(log p) and a regular integer-multiplication cost model.

def LongDivision.longDivAux (a b : ℕ) : ℕ → ℕ → ℕ → ℕ × ℕ

Helper for the bit-by-bit long-division algorithm (Algorithm 3.37): at bit index k, with current quotient q and remainder r, perform the shift-and- conditional-subtract step using the k-th bit of a against modulus b.

def LongDivision.longDiv (a b : ℕ) : ℕ × ℕ

Algorithm 3.37 (long division): given naturals a, b, return a pair (q, r) with a = qb + r and 0 ≤ r < b, handling the edge cases b = 0, b > a, and b = 1 directly.

theorem LongDivision.longDivAux_rem_lt (a b : ℕ) (_hb : b ≥ 2) (k q r : ℕ) (hr : r < b) : (longDivAux a b k q r).2 < b

Invariant for longDivAux: the running remainder stays strictly less than the modulus b throughout the bit-by-bit iteration.

theorem LongDivision.longDivAux_spec (a b : ℕ) (_hb : b ≥ 2) (k q r : ℕ) (hr : r < b) : (longDivAux a b k q r).1 * b + (longDivAux a b k q r).2 = q * b * 2 ^ (k + 1) + r * 2 ^ (k + 1) + a % 2 ^ (k + 1)

Correctness invariant for longDivAux: after processing bits k, k−1, …, 0, the quotient/remainder pair (q', r') satisfies q'·b + r' = q·b·2^(k+1) + r·2^(k+1) + (a mod 2^(k+1)).

noncomputable def LongDivision.longDivCost (m n : ℕ) : ℕ

Bit-operation cost model for long division of an m-bit integer by an n-bit integer: 3 · m · n.

theorem LongDivision.longDiv_complexity : ∃ (C : ℕ), ∀ (m n : ℕ), longDivCost m n ≤ C * (m * n)

Theorem 3.38: long division uses O(mn) bit operations to divide an m-bit integer by an n-bit integer, witnessed by the explicit constant C = 3.

def AreDifferentType {F : Type u_2} [Field F] [Fintype F] (hF : ringChar F ≠ 2) (a b : F) : Prop

The "different type" predicate from Theorem 3.44 (Rabin 1980): two nonzero elements a, b ∈ 𝔽_q (with char ≠ 2) have different type when their (q−1)/2-th powers disagree, i.e. one is a square and the other is not. Used in the root-finding Algorithm 3.45.

@[implicit_reducible]

instance instDecidableAreDifferentType {F : Type u_2} [Field F] [Fintype F] [DecidableEq F] (hF : ringChar F ≠ 2) (a b : F) : Decidable (AreDifferentType hF a b)

Decidability of AreDifferentType: each of the three conditions (a ≠ 0, b ≠ 0, distinct (q−1)/2-th powers) is decidable in a finite field.

structure Polynomial.IsSquarefreeFactorization {k : Type u_3} [Field k] (f : Polynomial k) (m : ℕ) (gs : Fin m → Polynomial k) : Prop

Squarefree factorization data (Algorithm 3.46): a polynomial f is given a squarefree factorization as f = ∏_{i < m} g_i^{i+1} where the g_i are pairwise coprime squarefree polynomials, m > 0, and the top exponent factor g_{m-1} is not the constant 1.

• pos : 0 < m
• prod_eq : f = ∏ i : Fin m, gs i ^ (↑i + 1)
• squarefree (i : Fin m) : Squarefree (gs i)
• coprime (i j : Fin m) : i ≠ j → IsCoprime (gs i) (gs j)
• last_ne_one : gs ⟨m - 1, ⋯⟩ ≠ 1

theorem Polynomial.irreducible_sq_dvd_iff_dvd_derivative {k : Type u_3} [Field k] [PerfectField k] {f g : Polynomial k} (hirr : Irreducible g) : g ^ 2 ∣ f ↔ g ∣ f ∧ g ∣ derivative f

Over a perfect field, an irreducible polynomial g satisfies g² ∣ f iff both g ∣ f and g ∣ f'. The characterization used in Yun's algorithm to detect squares.

theorem Polynomial.irreducible_sq_dvd_iff_dvd_gcd_derivative {k : Type u_3} [Field k] [PerfectField k] {f g : Polynomial k} (hirr : Irreducible g) : g ^ 2 ∣ f ↔ g ∣ EuclideanDomain.gcd f (derivative f)

Refined form of the previous lemma: g² ∣ f iff g divides gcd(f, f'). This is the divisibility used directly in Yun's algorithm to peel off the squarefree part.

structure Polynomial.YunState (k : Type u_4) [Field k] : Type u_4

Loop state for Yun's algorithm (Algorithm 3.46): the running pair (v_i, w_i) of polynomials whose GCD with the derivative-difference yields the next factor g_i.

• v : Polynomial k
• w : Polynomial k

noncomputable def Polynomial.yunStep {k : Type u_3} [Field k] (st : YunState k) : Polynomial k × YunState k

One iteration of Yun's algorithm: from state (v, w), compute g = gcd(v, w − v'), then advance to the new state (v/g, (w − v')/g).

noncomputable def Polynomial.yunInit {k : Type u_3} [Field k] (f : Polynomial k) : YunState k

Initialization of Yun's algorithm: from input f, divide out u = gcd(f, f') to set v_1 = f/u and w_1 = f'/u.

noncomputable def Polynomial.yunIterate {k : Type u_3} [Field k] (st : YunState k) : ℕ → List (Polynomial k) × YunState k

Iterate Yun's algorithm for a bounded number of steps n, collecting the factor sequence g_1, g_2, …. Stops early when the current v_i equals the computed g_i.

noncomputable def Polynomial.yunAlgorithm {k : Type u_3} [Field k] (f : Polynomial k) (fuel : ℕ) : List (Polynomial k)

Top-level Yun's algorithm (Algorithm 3.46): start from f, initialize, and iterate for at most fuel steps, returning the list of squarefree factors g_1, g_2, …, g_m.

@[simp]

theorem Polynomial.yunStep_fst {k : Type u_3} [Field k] (st : YunState k) : (yunStep st).1 = EuclideanDomain.gcd st.v (st.w - derivative st.v)

simp lemma: the first component of yunStep is gcd(v, w − v').

@[simp]

theorem Polynomial.yunInit_v {k : Type u_3} [Field k] (f : Polynomial k) : f.yunInit.v = f / EuclideanDomain.gcd f (derivative f)

simp lemma: the initial v in Yun's algorithm is f / gcd(f, f').

@[simp]

theorem Polynomial.yunInit_w {k : Type u_3} [Field k] (f : Polynomial k) : f.yunInit.w = derivative f / EuclideanDomain.gcd f (derivative f)

simp lemma: the initial w in Yun's algorithm is f' / gcd(f, f').

theorem Polynomial.yunAlgorithm_exists_sqfreeFactorization {k : Type u_3} [Field k] [PerfectField k] (f : Polynomial k) (hf : f.Monic) (hf_ne : f ≠ 1) (hdeg : ringChar k = 0 ∨ f.natDegree < ringChar k) : ∃ (m : ℕ) (gs : Fin m → Polynomial k), f.IsSquarefreeFactorization m gs

Correctness of Yun's algorithm (Algorithm 3.46): for a monic polynomial f over a perfect field with deg f < char k (or char = 0), there exist a positive m and pairwise coprime squarefree polynomials g_0, …, g_{m-1} such that f = ∏_{i} g_i^{i+1}.

noncomputable def Polynomial.xPowCardPowSubX (k : Type u_4) [Field k] [Fintype k] (j : ℕ) : Polynomial k

The polynomial X^{q^j} - X over a finite field k of cardinality q. Its roots are exactly the elements of the unique subfield 𝔽_{q^j} ⊆ k̄, so its factorization isolates irreducibles of degree dividing j. Used in Algorithm 3.47 / Algorithm 3.46 for distinct-degree factorization.

@[simp]

theorem Polynomial.xPowCardPowSubX_def {k : Type u_3} [Field k] [Fintype k] (j : ℕ) : xPowCardPowSubX k j = X ^ Fintype.card k ^ j - X

Definitional simp lemma for xPowCardPowSubX.

theorem Polynomial.irreducible_dvd_xPowCardPowSubX_natDegree_dvd {k : Type u_3} [Field k] [Fintype k] {j : ℕ} {g : Polynomial k} (hirr : Irreducible g) (hdvd : g ∣ xPowCardPowSubX k j) : g.natDegree ∣ j

If an irreducible polynomial g divides X^{q^j} − X, then its degree divides j. This is the key fact behind distinct-degree factorization: roots of X^{q^j} − X lie in 𝔽_{q^j}, whose irreducible factors over 𝔽_q have degrees dividing j.

noncomputable def Polynomial.distinctDegreeStep {k : Type u_3} [Field k] [Fintype k] (f : Polynomial k) (j : ℕ) : Polynomial k × Polynomial k

One step of distinct-degree factorization: from f, compute g = gcd(f, X^{q^j} − X) (the product of degree-j irreducible factors of f) and the new remaining polynomial f / g.

@[simp]

theorem Polynomial.distinctDegreeStep_fst {k : Type u_3} [Field k] [Fintype k] (f : Polynomial k) (j : ℕ) : (f.distinctDegreeStep j).1 = EuclideanDomain.gcd f (xPowCardPowSubX k j)

simp lemma: the first component of distinctDegreeStep is gcd(f, X^{q^j} − X).

@[simp]

theorem Polynomial.distinctDegreeStep_snd {k : Type u_3} [Field k] [Fintype k] (f : Polynomial k) (j : ℕ) : (f.distinctDegreeStep j).2 = f / EuclideanDomain.gcd f (xPowCardPowSubX k j)

simp lemma: the second component of distinctDegreeStep is the quotient f / gcd(f, X^{q^j} − X).

structure Polynomial.DistinctDegreeState (k : Type u_4) [Field k] : Type u_4

State for the distinct-degree factorization loop: the polynomial still left to factor and the list of degree-j partial products accumulated so far.

• remaining : Polynomial k
• factors : List (Polynomial k)

noncomputable def Polynomial.distinctDegreeIter {k : Type u_3} [Field k] [Fintype k] (st : DistinctDegreeState k) (j : ℕ) : DistinctDegreeState k

A single iteration of the distinct-degree factorization loop: extract the product of degree-j irreducible factors of the current remaining, and append it to the factor list.

noncomputable def Polynomial.distinctDegreeLoop {k : Type u_3} [Field k] [Fintype k] (f : Polynomial k) : ℕ → DistinctDegreeState k

Iterate distinct-degree factorization for j = 1, 2, …, n, starting from f.

noncomputable def Polynomial.distinctDegreeFactorize {k : Type u_3} [Field k] [Fintype k] (f : Polynomial k) : List (Polynomial k)

Top-level distinct-degree factorization (step 2 of Algorithm 3.47): for input f, run the loop up to degree deg f and return the list of degree-j factors.

structure Polynomial.IsDistinctDegreeFactorization {k : Type u_3} [Field k] (f : Polynomial k) (d : ℕ) (hs : Fin d → Polynomial k) : Prop

Distinct-degree factorization specification (step 2 of Algorithm 3.47): f factors as ∏ h_j where each h_j is a (possibly trivial) squarefree product of irreducibles all of degree j+1, and the h_j are pairwise coprime.

• prod_eq : f = ∏ i : Fin d, hs i
• irred_deg (j : Fin d) (g : Polynomial k) : Irreducible g → g ∣ hs j → g.natDegree = ↑j + 1
• squarefree (j : Fin d) : hs j = 1 ∨ Squarefree (hs j)
• coprime (i j : Fin d) : i ≠ j → IsCoprime (hs i) (hs j)

theorem Polynomial.distinctDegreeFactorization_exists (k : Type u_4) [Field k] [Fintype k] (f : Polynomial k) (hf : f.Monic) (hsqf : Squarefree f) : ∃ (d : ℕ) (hs : Fin d → Polynomial k), f.IsDistinctDegreeFactorization d hs

Correctness of distinct-degree factorization (step 2 of Algorithm 3.47): for any monic squarefree polynomial f over a finite field, there exist d and factors h_0, …, h_{d-1} with the IsDistinctDegreeFactorization property.