Coefficient interface to Shoup's construction

The field consumers use the lower coefficients of the monic polynomial. Keeping this adapter separate lets generic arithmetic and the future constructor use the same coefficient algorithms without importing the Shoup interface.

noncomputable def MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs : Cost.PolyTimeFun Cost.Unary Cost.BitStr

Shoup's output normalized to the k lower coefficients; the leading monic coefficient is implicit. This construction retains Shoup's unary input bound.

Equations

• MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs = MIPRE.LowDegree.BinaryPolynomial.takeBitsProg.comp ((MIPRE.Cost.PolyTimeFun.id MIPRE.Cost.Unary).pair MIPRE.LowDegree.shoupIrreducible)

theorem MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs_length (k : ℕ) (hk : 1 ≤ k) : List.length (shoupLowerCoeffs.toFun (Cost.unary k)) = k

theorem MIPRE.LowDegree.BinaryPolynomial.shoupLowerCoeffs_poly (k : ℕ) (hk : 1 ≤ k) : polyOfBits (shoupLowerCoeffs.toFun (Cost.unary k) ++ [true]) = polyOfBits (shoupIrreducible.toFun (Cost.unary k))