Actual bad seeds from adaptive average discrepancy

An average-TV bound for every deterministic, seed-dependent choice of a shift and tampered seeds implies the claimed bad-seed cardinality bound. The counting theorem explicitly assumes that average bound; it does not assert a correlation-breaker guarantee for an arbitrary supplied map.

This is the witness-selection and counting step in Chattopadhyay--Liao, Extractors for Sum of Two Sources (2021), Lemma 5.3, printed pp.19--20: https://arxiv.org/pdf/2110.12652.

theorem Algebraic.Cutwidth.Extractor.affineLeakageOutputWeight_probability {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) (b : Fin n → Bool) (y : Fin d → Bool) (ys : Fin t → Fin d → Bool) (probability : IsProbabilityWeight p) : IsProbabilityWeight (affineLeakageOutputWeight cb p leak advice b y ys)

The actual leaked output law preserves the normalization of its source.

theorem Algebraic.Cutwidth.Extractor.mem_affineLeakageBadSeeds {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) : y ∈ affineLeakageBadSeeds cb p leak advice γ ↔ ∃ (b : Fin n → Bool) (ys : Fin t → Fin d → Bool), γ < weightDist (affineLeakageOutputWeight cb p leak advice b y ys) (uniformSecondWeight (affineLeakageOutputWeight cb p leak advice b y ys))

A bad honest seed has an actual shift and tampered tuple exceeding the strict threshold.

theorem Algebraic.Cutwidth.Extractor.not_mem_affineLeakageBadSeeds {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) : y ∉ affineLeakageBadSeeds cb p leak advice γ ↔ ∀ (b : Fin n → Bool) (ys : Fin t → Fin d → Bool), weightDist (affineLeakageOutputWeight cb p leak advice b y ys) (uniformSecondWeight (affineLeakageOutputWeight cb p leak advice b y ys)) ≤ γ

Outside the bad set, every actual shift and tampered tuple has discrepancy at most the threshold.

theorem Algebraic.Cutwidth.Extractor.affineLeakageBadSeeds_card_le {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) {γ ε : ℝ} (positive : 0 < γ) (average : ∀ (g : (Fin d → Bool) → Fin n → Bool) (f : (Fin d → Bool) → Fin t → Fin d → Bool), ∑ y : Fin d → Bool, uniformWeight (Fin d → Bool) y * weightDist (affineLeakageOutputWeight cb p leak advice (g y) y (f y)) (uniformSecondWeight (affineLeakageOutputWeight cb p leak advice (g y) y (f y))) ≤ ε) : ↑(affineLeakageBadSeeds cb p leak advice γ).card ≤ ε / γ * ↑(Fintype.card (Fin d → Bool))

All adaptive deterministic witness averages control the actual bad-seed cardinality.