Strong extraction by the actual Boolean program

The input and uniformly sampled seed are Boolean vectors of their exact prescribed widths. Output coordinates are read from the actual bit program in block order. The canonical codec identifies this map with the specified recursive extractor, and bijective transport preserves its retained-seed guarantee and source XOR additivity.

The recursive construction and parameter bounds are credited in Scheduled. This layer adds only finite representation transport. Its statements require no caller-supplied field enumeration instances; those are constructed from the proved binary quotient cardinalities.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_eq (n h Q E ell : ℕ) (x : Fin n → Bool) (seed : Fin (scheduledBlockSeedBits n h Q E ell) → Bool) (i : Fin (recursiveBlockCount 1 h)) (j : Fin ell) : scheduledBlockBooleanExtractor n h Q E ell x seed i j = decide (scheduledBlockExtractor n h Q E ell x (decodeScheduledBlockSeeds n h Q E ell (List.ofFn seed)) i j = 1)

Each actual output bit agrees with the corresponding semantic coordinate at decoded seeds.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_xor (n h Q E ell : ℕ) (x x' : Fin n → Bool) (seed : Fin (scheduledBlockSeedBits n h Q E ell) → Bool) : scheduledBlockBooleanExtractor n h Q E ell (fun (i : Fin n) => x i ^^ x' i) seed = fun (i : Fin (recursiveBlockCount 1 h)) (j : Fin ell) => scheduledBlockBooleanExtractor n h Q E ell x seed i j ^^ scheduledBlockBooleanExtractor n h Q E ell x' seed i j

For any fixed Boolean seed, input XOR becomes pointwise output XOR.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_weighted (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) : WeightedStrongSeededExtractor (scheduledBlockBooleanExtractor n h Q E ell) (2 ^ recursiveBlockEntropy h Q 0) ((3 * 2 ^ h - 1) * (2 ^ E)⁻¹)

The actual program is a strong extractor with its full uniformly sampled Boolean seed.

theorem Algebraic.Cutwidth.Extractor.scheduledBlockBooleanExtractor_dyadic (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (depth : h ≤ L) : WeightedStrongSeededExtractor (scheduledBlockBooleanExtractor n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L) (2 ^ recursiveBlockEntropy h (recursiveBlockReserve L (e + h + 2)) 0) (2 ^ e)⁻¹

The explicit reserve gives error 2^(-e) for the actual Boolean-seed program.