Parity on a finite support -- definitions

Random restrictions leave parity on the remaining free coordinates, possibly complemented by the fixed coordinates. xorOn makes that support explicit.

def Complexity.Schnorr.xorOp (left right : Bool) : Bool

Boolean exclusive-or as an explicitly named commutative fold operation.

Equations

• Complexity.Schnorr.xorOp left right = (left ^^ right)

instance Complexity.Schnorr.xorOp_commutative : Std.Commutative xorOp

instance Complexity.Schnorr.xorOp_associative : Std.Associative xorOp

def Complexity.Schnorr.xorOn {N : ℕ} (support : Finset (Fin N)) (input : BitString N) : Bool

XOR of exactly the coordinates in support.

Equations

• Complexity.Schnorr.xorOn support input = Finset.fold Complexity.Schnorr.xorOp false input support