Searching for irreducible polynomials over GF(2)

6 fully proved

Polynomial

TheoremMonic irreducible binary polynomials exist in every degree#✓fully proved

Over ZMod 2, there is a monic irreducible polynomial of every positive degree.

theorem exists_monic_irreducible_zmod_two (s : Nat) (hs : 0 < s) :
    ∃ f : Polynomial (ZMod 2), f.Monic ∧ Irreducible f ∧ f.natDegree = s

Used by 1

Used byExhaustive search returns an irreducible binary modulus

Bit Vec

DefinitionExhaustive inverse test for a binary polynomial modulus#✓fully proved

Test exhaustively whether every nonzero word has a multiplicative inverse modulo g.monicModulus.

def passesInverseTest {s : Nat} (g : BitVec s) : Bool :=
  let words := (List.range (2 ^ s)).map (BitVec.ofNat s)
  words.all fun x =>
    decide (x = 0#s) ||
      words.any fun y => decide (g.mulMod x y = 1#s)

Uses 1 · Used by 4

Statement usesModular multiplication of binary polynomial residues

Used byExhaustive search for an irreducible binary modulus · Minimality of the binary modulus found by exhaustive search · Exhaustive search returns an irreducible binary modulus · Inverse test succeeds exactly for irreducible moduli

TheoremInverse test succeeds exactly for irreducible moduli#✓fully proved

At positive width, the exhaustive inverse test succeeds exactly for irreducible monic moduli.

theorem passesInverseTest_iff_irreducible {s : Nat} (g : BitVec s) (hs : 0 < s) :
    g.passesInverseTest = true ↔ Irreducible g.monicModulus

Uses 8 · Used by 2

Statement usesMonic binary modulus of a fixed-width word · Exhaustive inverse test for a binary polynomial modulus

Proof usesFixed-width binary words as residues modulo a monic polynomial · Forward map of the binary word residue equivalence · Modular multiplication matches the polynomial quotient · Coefficients of the binary polynomial of a bitvector · Modular multiplication of binary polynomial residues · Binary polynomial of a bitvector

Used byMinimality of the binary modulus found by exhaustive search · Exhaustive search returns an irreducible binary modulus

DefinitionExhaustive search for an irreducible binary modulus#✓fully proved

Search the lower coefficient words in ascending order for the first word passing the exhaustive inverse test. Width zero is deliberately reported as failure.

def findIrreducibleModulus (s : Nat) : Option (BitVec s) :=
  if 0 < s then
    ((List.range (2 ^ s)).map (BitVec.ofNat s)).find? passesInverseTest
  else
    none

Uses 1 · Used by 2

Statement usesExhaustive inverse test for a binary polynomial modulus

Used byMinimality of the binary modulus found by exhaustive search · Exhaustive search returns an irreducible binary modulus

TheoremExhaustive search returns an irreducible binary modulus#✓fully proved

At every positive width, exhaustive search returns an irreducible binary modulus.

theorem findIrreducibleModulus_spec (s : Nat) (hs : 0 < s) :
    ∃ g : BitVec s, findIrreducibleModulus s = some g ∧
      Irreducible g.monicModulus

Uses 8

Statement usesExhaustive search for an irreducible binary modulus · Monic binary modulus of a fixed-width word

Proof usesCoefficients of the binary polynomial of a bitvector · Exhaustive inverse test for a binary polynomial modulus · Inverse test succeeds exactly for irreducible moduli · Binary polynomial of a bitvector · Monic irreducible binary polynomials exist in every degree · Bitvector of the low coefficients of a binary polynomial

TheoremMinimality of the binary modulus found by exhaustive search#✓fully proved

The returned modulus is no larger than any lower coefficient word whose monic modulus is irreducible.

theorem findIrreducibleModulus_minimal {s : Nat} (g : BitVec s)
    (h : findIrreducibleModulus s = some g) :
    ∀ g' : BitVec s, Irreducible g'.monicModulus → g.toNat ≤ g'.toNat

Uses 4

Statement usesExhaustive search for an irreducible binary modulus · Monic binary modulus of a fixed-width word

Proof usesExhaustive inverse test for a binary polynomial modulus · Inverse test succeeds exactly for irreducible moduli

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.