Documentation

MIPRE.Foundations.LowDegree.Shoup

Deterministic irreducible polynomials over the binary field #

This file exposes the proved fixed-characteristic construction of Shoup 1990, Theorem 3.2. The specified program factors squarefree binary polynomials, constructs odd-prime auxiliary nonresidues and trace generators, builds the characteristic-two Artin–Schreier tower, and combines coprime prime-power degrees by composed sums.

The input is the unary requested degree. Every arithmetic operation and bounded loop is compiled into the ambient cost model, including coefficient printing and a fixed constant output at degree zero. BinaryPolynomial.irreducibleBitsProg_time_le gives the resulting polynomial runtime bound in the degree. The public names below retain the interfaces used by the quotient-field and self-dual-normal-basis consumers.

source
noncomputable def MIPRE.LowDegree.shoupIrreducible :
Cost.PolyTimeFun Cost.Unary (List Bool)

The specified deterministic polynomial-time irreducible-polynomial constructor.

Equations
Instances For
    source
    theorem MIPRE.LowDegree.exists_shoup_irreducible :
    ∃ (F : Cost.PolyTimeFun Cost.Unary (List Bool)), ∀ (k : ℕ), 1 ≤ k → (polyOfBits (F.toFun (Cost.unary k))).Monic ∧ Irreducible (polyOfBits (F.toFun (Cost.unary k))) ∧ (polyOfBits (F.toFun (Cost.unary k))).natDegree = k

    Shoup's deterministic irreducible-polynomial construction over 𝔽₂ (Shoup 1990, Theorem 3.2; ledger node 1.1.6.1.1), proved by the explicit program.

    source
    theorem MIPRE.LowDegree.shoupIrreducible_monic (k : ℕ) (hk : 1 ≤ k) :
    (polyOfBits (shoupIrreducible.toFun (Cost.unary k))).Monic

    The constructed polynomial is monic at every positive degree.

    source
    theorem MIPRE.LowDegree.shoupIrreducible_irreducible (k : ℕ) (hk : 1 ≤ k) :
    Irreducible (polyOfBits (shoupIrreducible.toFun (Cost.unary k)))

    The constructed polynomial is irreducible at every positive degree.

    source
    theorem MIPRE.LowDegree.shoupIrreducible_natDegree (k : ℕ) (hk : 1 ≤ k) :
    (polyOfBits (shoupIrreducible.toFun (Cost.unary k))).natDegree = k

    The constructed polynomial has exactly the requested positive degree.