Documentation

MIPRE.Foundations.LowDegree.BinaryCyclotomicSeed

The deterministic cyclotomic seed for odd prime-power construction #

For an odd prime q, factor 1+X+...+X^(q-1) and choose the first factor in the specified factorization order. This gives a concrete irreducible polynomial of degree equal to the order of two modulo q; it does not enumerate fields.

source
theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_replicate_true (n : ℕ) :
polyOfBits (List.replicate n true) = ∑ i ∈ Finset.range n, Polynomial.X ^ i

The all-one coefficient vector is the geometric-sum polynomial.

source
def MIPRE.LowDegree.BinaryPolynomial.cyclotomicLowerBits (u : Cost.Unary) :
Cost.BitStr

Lower coefficients of the prime cyclotomic polynomial; the leading one is implicit.

Equations
Instances For
    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.cyclotomicLowerBitsProg :
    Cost.PolyTimeFun Cost.Unary Cost.BitStr

    Uniform unary printing of the binary prime-cyclotomic coefficient vector.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicLowerBitsProg_apply (u : Cost.Unary) :
      cyclotomicLowerBitsProg.toFun u = cyclotomicLowerBits u
      source
      theorem MIPRE.LowDegree.BinaryPolynomial.polyOfBits_cyclotomicLowerBits (q : ℕ) (hq : Nat.Prime q) :
      polyOfBits (cyclotomicLowerBits (Cost.unary q) ++ [true]) = Polynomial.cyclotomic q (ZMod 2)

      The printed monic polynomial is exactly the cyclotomic polynomial at every prime.

      source
      noncomputable def MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits (u : Cost.Unary) :
      Cost.BitStr

      Choose the first factor in the fixed deterministic factorization order.

      Equations
      Instances For
        source
        noncomputable def MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBitsProg :
        Cost.PolyTimeFun Cost.Unary Cost.BitStr

        One fixed ambient program producing the auxiliary irreducible seed.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          @[simp]
          theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBitsProg_apply (u : Cost.Unary) :
          cyclotomicSeedBitsProg.toFun u = cyclotomicSeedBits u
          source
          theorem MIPRE.LowDegree.BinaryPolynomial.oddPrime_cast_ne_zero (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
          ↑q ≠ 0

          An odd prime remains nonzero in the binary field.

          source
          theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits_correct (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
          (polyOfBits (cyclotomicSeedBits (Cost.unary q))).Monic ∧ Irreducible (polyOfBits (cyclotomicSeedBits (Cost.unary q))) ∧ polyOfBits (cyclotomicSeedBits (Cost.unary q)) ∣ Polynomial.cyclotomic q (ZMod 2)

          The chosen seed is a specified monic irreducible divisor of the prime cyclotomic polynomial.

          source
          theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits_natDegree (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) (hcop : Nat.Coprime 2 q) :
          (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree = orderOf (ZMod.unitOfCoprime (2 ^ 1) ⋯)

          The seed degree is the multiplicative order of two modulo the odd prime.

          source
          theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits_degree_dvd (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
          0 < (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree ∧ (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree ∣ q - 1

          The seed has positive degree dividing q-1, so its size is polynomial in unary q.

          source
          theorem MIPRE.LowDegree.BinaryPolynomial.cyclotomicSeedBits_degree_coprime (q : ℕ) (hq : Nat.Prime q) (hq2 : q ≠ 2) :
          (polyOfBits (cyclotomicSeedBits (Cost.unary q))).natDegree.Coprime q

          The seed degree is coprime to the requested odd prime.