Depth-two threshold circuits for parity -- proof internals

theorem Complexity.xorBool_eq_decide_countP_internal (N : ℕ) (x : BitString N) : Schnorr.xorBool N x = decide (Fin.countP x % 2 = 1)

Parity is the parity of the number of true inputs.

theorem Complexity.Circuit.wireValue_thresholdParity_natAdd_internal (N : ℕ) [NeZero N] (x : BitString N) (j : Fin N) : (thresholdParity N).wireValue x (Fin.natAdd N j) = decide (↑j + 1 ≤ Fin.countP x)

Internal gate j of the parity circuit tests whether at least j + 1 inputs are true.

theorem Complexity.Circuit.eval_thresholdParity_internal (N : ℕ) [NeZero N] (x : BitString N) : (thresholdParity N).eval x 0 = Schnorr.xorBool N x

theorem Complexity.Circuit.depth_thresholdParity_le_internal (N : ℕ) [NeZero N] : (thresholdParity N).depth ≤ 2

theorem Complexity.CircuitFamily.thresholdParity_computes_internal : thresholdParity.Computes Schnorr.xorBool

theorem Complexity.CircuitFamily.thresholdParity_size_internal (n : ℕ) : thresholdParity.size n ≤ n + 1

theorem Complexity.CircuitFamily.thresholdParity_depth_internal (n : ℕ) : thresholdParity.depth n ≤ 2

theorem Complexity.xorBool_mem_TC0_internal : Schnorr.xorBool ∈ TC0