Signs of the actual XOR reduction

The product of outer-coordinate signs differs from the product of all component signs by one constant sign. Absolute bias is therefore exactly the same, for arbitrary source weights and every finite parity test.

theorem Algebraic.Cutwidth.Extractor.Internal.sign_xorBool (C : ℕ) (bits : Fin C → Bool) : (if Complexity.Schnorr.xorBool C bits = true then 1 else -1) = (-1) ^ (C + 1) * ∏ z : Fin C, if bits z = true then 1 else -1

theorem Algebraic.Cutwidth.Extractor.Internal.affineSourceReduction_parity_bias_eq {n N C : ℕ} {α : Type u_1} {Seed : Type u_2} {Advice : Type u_3} (cb : (Fin n → Bool) → Seed → Advice → Bool) (sampler : (Fin n → Bool) → Fin N → Fin C → Seed) (advice : Fin N → Fin C → Advice) (s : Finset α) (w : α → ℝ) (input : α → Fin n → Bool) (U : Finset (Fin N)) : |weightedMean s w fun (x : α) => ∏ i ∈ U, if affineSourceReduction cb sampler advice (input x) i = true then 1 else -1| = |weightedMean s w fun (x : α) => ∏ i ∈ U, ∏ z : Fin C, if cb (input x) (sampler (input x) i z) (advice i z) = true then 1 else -1|