Actual scheduled extraction from a Boolean affine source

The named Boolean bit program extracts from a left source XOR a right-side mask while retaining the entire right variable and shared transcript. The error pays for extraction, the seed's distance from uniform given the transcript, and an average joint source-mass envelope. Source XOR linearity and the output translation equivalence are discharged by the implementation.

Both the general finite schedule and its explicit dyadic-error family are available without caller-supplied extractors or field instances. This is a finite extraction step for the affine correlation-breaker argument of Chattopadhyay--Liao, Extractors for Sum of Two Sources, Theorem 6.1, https://arxiv.org/pdf/2110.12652. The remaining tampering and recursive correlation-breaker guarantees are separate layers.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_affine_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {δ : ℝ} (n h Q E ell : ℕ) (budget : 3 * (24 * explicitCondenserBudget (scheduledBlockInitialWidth n h Q E) (recursiveBlockEntropy h Q 0) E) + 6 * E ≤ 2 * Q) (reserve : ell + 2 * E ≤ Q) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (y : Z → B → Fin (scheduledBlockSeedBits n h Q E ell) → Bool) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ) : weightDist (affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (scheduledBlockBooleanExtractor n h Q E ell)) (uniformSecondWeight (affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (scheduledBlockBooleanExtractor n h Q E ell))) ≤ (3 * 2 ^ h - 1) * (2 ^ E)⁻¹ + δ + ↑(2 ^ recursiveBlockEntropy h Q 0) * ∑ z : Z, μ z

The actual scheduled extractor tolerates a correlated right mask with its full state retained.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_dyadic_affine_dist_le {Z : Type u_1} {A : Type u_2} {B : Type u_3} [Fintype Z] [Fintype A] [Fintype B] {δ : ℝ} (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (depth : h ≤ L) (w : Z → ℝ) (l : Z → A → ℝ) (r : Z → B → ℝ) (x : Z → A → Fin n → Bool) (mask : Z → B → Fin n → Bool) (y : Z → B → Fin (scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L) → Bool) (μ : Z → ℝ) (hw : IsProbabilityWeight w) (hl : ∀ (z : Z), IsProbabilityWeight (l z)) (hr : ∀ (z : Z), IsProbabilityWeight (r z)) (nonnegative : ∀ (z : Z), 0 ≤ μ z) (cap : ∀ (z : Z) (x₀ : Fin n → Bool), w z * mapWeight (x z) (l z) x₀ ≤ μ z) (seed : weightDist (retainedSeedWeight w r y) (uniformSecondWeight (retainedSeedWeight w r y)) ≤ δ) : weightDist (affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (scheduledBlockBooleanExtractor n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L)) (uniformSecondWeight (affineExtractionWeight w l r x mask y (fun (a b : Fin n → Bool) (i : Fin n) => a i ^^ b i) (scheduledBlockBooleanExtractor n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L))) ≤ (2 ^ e)⁻¹ + δ + ↑(2 ^ recursiveBlockEntropy h (recursiveBlockReserve L (e + h + 2)) 0) * ∑ z : Z, μ z

Explicit reserve parameters give the same retained affine guarantee with error 2^(-e).