Bounded modular Frobenius on binary coefficient lists

A count list requests one square-and-remainder step per bit, independently of the bit values. The initial dividend is reduced before the first step. Every state has the fixed width of the modulus degree.

A zero modulus produces the empty list at initialization and at every step. This explicit convention keeps the total algorithm bounded: unreduced successive squares could have exponential output length. Nonzero moduli may have arbitrary high zero padding, and a constant-one modulus also gives the empty list. The evaluator uses the codec pair (pair a modulus) count.

def Complexity.BitPolynomial.frobeniusStep (modulus state : List Bool) : List Bool

Square and reduce a state, returning the empty list for a zero modulus.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.BitPolynomial.frobeniusBits (a modulus : List Bool) : List Bool → List Bool

Reduce a dividend, then square and reduce once per bit of the count list.

Equations

• Complexity.BitPolynomial.frobeniusBits a modulus [] = if Complexity.BitPolynomial.significantLength modulus = 0 then [] else Complexity.BitPolynomial.remainderBits a modulus
• Complexity.BitPolynomial.frobeniusBits a modulus (head :: tail) = Complexity.BitPolynomial.frobeniusStep modulus (Complexity.BitPolynomial.frobeniusBits a modulus tail)

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

The total evaluator on pair (pair dividend modulus) count.

Equations

• Complexity.BitPolynomial.frobeniusEval z = Complexity.BitPolynomial.frobeniusBits (Complexity.pairFst (Complexity.pairFst z)) (Complexity.pairSnd (Complexity.pairFst z)) (Complexity.pairSnd z)