Runtime coefficient lists for sparse binary trinomials

The list trinomialBits d has true coefficients at positions 0, d, and 2*d, representing X^(2*d) + X^d + 1 over the two-element field. The definition is total at d = 0: all three positions coincide, and their sum is still one in characteristic two. The evaluator takes d in unary as the length of its input; the input bit values are ignored.

def Complexity.BitPolynomial.trinomialBits (d : ℕ) : List Bool

The coefficient list of X^(2*d) + X^d + 1, including the case d = 0.

Equations

• Complexity.BitPolynomial.trinomialBits d = List.map (fun (i : ℕ) => decide (i = 0 ∨ i = d ∨ i = 2 * d)) (List.range (2 * d + 1))

def Complexity.BitPolynomial.trinomialEval (z : List Bool) : List Bool

Generate a sparse binary trinomial from a runtime unary half-degree.

Equations

• Complexity.BitPolynomial.trinomialEval z = Complexity.BitPolynomial.trinomialBits z.length

def Complexity.BitPolynomial.roundedTrinomialEval (z : List Bool) : List Bool

Round a runtime unary target up to a power of three and generate its trinomial.

Equations

• Complexity.BitPolynomial.roundedTrinomialEval z = Complexity.BitPolynomial.trinomialBits (3 ^ Nat.clog 3 z.length)