Parity bounds for the actual leaked affine outputs

A balanced bit of the honest output has small sign expectation after XOR with any function of all retained tampered outputs. The more general real mask theorem permits any tag statistic of absolute value at most one, including a product of tampered signs. The sign convention is true ↦ 1 and false ↦ -1.

These are finite weighted consequences of the conditional-uniformity comparison used in Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemmas 5.3--5.4: https://arxiv.org/abs/2110.12652. The calculation is valid for raw signed weights, so normalization is unnecessary. The actual-law corollaries require membership outside the defined bad-seed set; they do not assume a parity guarantee or a new correlation breaker.

theorem Algebraic.Cutwidth.Extractor.weightSign_mul_le_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] (p : Tag × Out → ℝ) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : Tag → ℝ) (bound : ∀ (tag : Tag), |mask tag| ≤ 1) : |∑ z : Tag × Out, p z * ((if bit z.2 = true then 1 else -1) * mask z.1)| ≤ 2 * weightDist p (uniformSecondWeight p)

A balanced honest sign times any bounded tag statistic has bias at most twice the distance.

theorem Algebraic.Cutwidth.Extractor.weightSign_xor_le_dist {Tag : Type u_1} {Out : Type u_2} [Fintype Tag] [Fintype Out] (p : Tag × Out → ℝ) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : Tag → Bool) : |∑ z : Tag × Out, p z * if (bit z.2 ^^ mask z.1) = true then 1 else -1| ≤ 2 * weightDist p (uniformSecondWeight p)

XOR with any tag-dependent bit preserves the twice-distance sign bound.

theorem Algebraic.Cutwidth.Extractor.mapWeight_uniform_bool_coordinate {M : ℕ} (j : Fin M) : mapWeight (fun (x : Fin M → Bool) => x j) (uniformWeight (Fin M → Bool)) = uniformWeight Bool

Every coordinate of a uniformly sampled Boolean vector is balanced.

theorem Algebraic.Cutwidth.Extractor.affineLeakage_sign_mul_le_of_not_mem_badSeeds {n d t : ℕ} {Out : Type u_1} [Fintype Out] (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : (Fin t → Out) → ℝ) (bound : ∀ (outputs : Fin t → Out), |mask outputs| ≤ 1) : |∑ x : Fin n → Bool, p x * ((if bit (cb (xorInput x b) (xorInput y (leak x none)) (advice none)) = true then 1 else -1) * mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i)))| ≤ 2 * γ

Nonbad seeds bound the honest sign against every bounded tampered-output statistic.

theorem Algebraic.Cutwidth.Extractor.affineLeakage_sign_le_of_not_mem_badSeeds {n d t : ℕ} {Out : Type u_1} [Fintype Out] (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Out) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (bit : Out → Bool) (balanced : mapWeight bit (uniformWeight Out) = uniformWeight Bool) (mask : (Fin t → Out) → Bool) : |∑ x : Fin n → Bool, p x * if (bit (cb (xorInput x b) (xorInput y (leak x none)) (advice none)) ^^ mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i))) = true then 1 else -1| ≤ 2 * γ

Nonbad seeds bound every XOR mask of the actual tampered outputs.

theorem Algebraic.Cutwidth.Extractor.affineLeakage_coordinate_sign_le_of_not_mem_badSeeds {n d t M : ℕ} (cb : (Fin n → Bool) → (Fin d → Bool) → List Bool → Fin M → Bool) (p : (Fin n → Bool) → ℝ) (leak : (Fin n → Bool) → Option (Fin t) → Fin d → Bool) (advice : Option (Fin t) → List Bool) (γ : ℝ) (y : Fin d → Bool) (good : y ∉ affineLeakageBadSeeds cb p leak advice γ) (b : Fin n → Bool) (ys : Fin t → Fin d → Bool) (j : Fin M) (mask : (Fin t → Fin M → Bool) → Bool) : |∑ x : Fin n → Bool, p x * if (cb (xorInput x b) (xorInput y (leak x none)) (advice none) j ^^ mask fun (i : Fin t) => cb (xorInput x b) (xorInput (ys i) (leak x (some i))) (advice (some i))) = true then 1 else -1| ≤ 2 * γ

Nonbad seeds bound every honest output coordinate after any tampered-output XOR mask.