Affine extraction by the scheduled Boolean program

The actual program's source XOR law expresses a right-source mask as an output XOR mask. Coordinatewise XOR is an involution on the curried output blocks, supplying the output equivalence required by retained affine extraction. The extractor guarantee comes from the checked finite schedule.

theorem Algebraic.Cutwidth.Extractor.Internal.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

theorem Algebraic.Cutwidth.Extractor.Internal.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