Exact binary trinomial generation

The runtime coefficient generator denotes X^(2*d) + X^d + 1 and has exact length 2*d+1, including d=0. Irreducibility at selected degrees is a separate algebraic theorem. The uniform polynomial-time certificate is supplied by Complexitylib.Classes.P.BitPolynomial.Trinomial.

theorem Complexity.BitPolynomial.trinomialBits_length (d : ℕ) : (trinomialBits d).length = 2 * d + 1

The generated coefficient list retains its leading coefficient.

theorem Complexity.BitPolynomial.ofBits_trinomialBits (d : ℕ) : ofBits (trinomialBits d) = Polynomial.X ^ (2 * d) + Polynomial.X ^ d + 1

The concrete list represents the three-term polynomial, even at degree zero.