XOR (Parity) Function

This module defines the N-input XOR function and its key properties.

Main definitions

• Schnorr.xorBool — the N-input XOR (parity) function

Main results

• Schnorr.xorBool_flip — flipping any input bit flips XOR
• Schnorr.xorBool_essential — XOR depends on all inputs

def CircuitComplexity.Schnorr.xorBool (N : ℕ) : BitString N → Bool

The N-input XOR (parity) function.

Equations

• CircuitComplexity.Schnorr.xorBool 0 x_2 = false
• CircuitComplexity.Schnorr.xorBool n.succ x_2 = (x_2 0 ^^ CircuitComplexity.Schnorr.xorBool n (x_2 ∘ Fin.succ))

theorem CircuitComplexity.Schnorr.xorBool_flip (N : ℕ) (x : BitString N) (a : Fin N) : xorBool N (Function.update x a !x a) = !xorBool N x

Flipping any input bit flips the XOR output.

theorem CircuitComplexity.Schnorr.xorBool_essential (N : ℕ) (a : Fin N) (x : BitString N) : xorBool N x ≠ xorBool N (Function.update x a !x a)

XOR depends on all inputs.