Long division of binary coefficient lists

significantLength discards high zero padding numerically: it is one past the highest true coefficient, or zero for the zero polynomial. Every nonzero binary polynomial is monic, independently of its list's high zero padding.

For a modulus of degree d, remainderScan processes the dividend from its highest coefficient to its constant coefficient, keeping exactly d bits. Each step shifts the current remainder, inserts the next coefficient, and cancels the possible degree-d term with the supplied modulus. Constant-one moduli have d = 0 and produce the empty list.

remainderBits returns its dividend unchanged for a zero modulus, agreeing with Mathlib's convention for remainder by a nonmonic zero polynomial. Both operands are runtime inputs, and every definition is total.

def Complexity.BitPolynomial.significantLength (bits : List Bool) : ℕ

One past the highest true coefficient, or zero for an all-false list.

Equations

• Complexity.BitPolynomial.significantLength bits = (Finset.range bits.length).sup fun (i : ℕ) => if bits[i]?.getD false = true then i + 1 else 0

def Complexity.BitPolynomial.remainderStep (modulus : List Bool) (bit : Bool) (state : List Bool) : List Bool

One long-division step, retaining exactly the modulus degree in coefficients.

Equations

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

def Complexity.BitPolynomial.remainderScan (modulus : List Bool) : List Bool → List Bool

Scan a little-endian dividend from its high coefficients to its low coefficients.

Equations

• Complexity.BitPolynomial.remainderScan modulus [] = List.replicate (Complexity.BitPolynomial.significantLength modulus - 1) false
• Complexity.BitPolynomial.remainderScan modulus (bit :: tail) = Complexity.BitPolynomial.remainderStep modulus bit (Complexity.BitPolynomial.remainderScan modulus tail)

def Complexity.BitPolynomial.remainderBits (a modulus : List Bool) : List Bool

Remainder by a runtime binary modulus, allowing high zeros and the zero polynomial.

Equations

• Complexity.BitPolynomial.remainderBits a modulus = if Complexity.BitPolynomial.significantLength modulus = 0 then a else Complexity.BitPolynomial.remainderScan modulus a

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

The total paired-input evaluator for binary-polynomial remainder.

Equations

• Complexity.BitPolynomial.remainderEval z = Complexity.BitPolynomial.remainderBits (Complexity.pairFst z) (Complexity.pairSnd z)