Documentation

MIPRE.Foundations.LowDegree.BinaryIrreducibleConstructor

A specified polynomial-time irreducible polynomial of every positive binary degree #

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

The complete constructor, with a fixed constant output at degree zero.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def MIPRE.LowDegree.BinaryPolynomial.irreducibleBitsProg :
    Cost.PolyTimeFun Cost.Unary Cost.BitStr

    One globally polynomial-time program constructs every positive binary degree.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBitsProg_apply (u : Cost.Unary) :
      irreducibleBitsProg.toFun u = irreducibleBits u
      source
      @[simp]
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBits_zero :
      irreducibleBits (Cost.unary 0) = [true]

      Degree zero is handled directly without invoking the construction loops.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBits_getLast (u : Cost.Unary) :
      List.getLastD (irreducibleBits u) false = true

      Every output is in nonzero canonical coefficient form.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBits_correct (n : ℕ) (hn : 1 ≤ n) :
      (polyOfBits (irreducibleBits (Cost.unary n))).Monic ∧ Irreducible (polyOfBits (irreducibleBits (Cost.unary n))) ∧ (polyOfBits (irreducibleBits (Cost.unary n))).natDegree = n

      The complete deterministic constructor is monic, irreducible, and has exactly its requested degree for every positive unary input.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBits_length (n : ℕ) (hn : 1 ≤ n) :
      List.length (irreducibleBits (Cost.unary n)) = n + 1

      The program prints the leading coefficient as well as all lower coefficients.

      source
      theorem MIPRE.LowDegree.BinaryPolynomial.irreducibleBitsProg_time_le :
      ∃ (R : Polynomial ℕ), ∀ (n : ℕ), ∃ t ≤ Polynomial.eval n R, irreducibleBitsProg.code.Runs (Cost.encode (Cost.unary n)) (Cost.encode (irreducibleBits (Cost.unary n))) t

      A concrete polynomial bounds the actual ambient run time as a function of degree, including degree zero and output printing.