Actual strong extraction at matched Boolean widths

The scheduled bit program uses a common padded seed width 2^24 * L and emits exactly 2^h * L bits in block order. Only the exact prescribed seed prefix enters the program. The strong guarantee retains the entire padded seed, including the unused suffix, and requires no supplied extractor or field instances. XOR preservation holds for every parameter choice.

The finite bounds are our deductions in Scheduled.BoundedDepth; the recursive construction is credited in Recursion.Extraction. The matched widths support the alternating-extraction and flip-flop route of Chattopadhyay--Goyal--Li, Section 6, Algorithms 1--2, https://arxiv.org/pdf/1505.00107. This adapter does not assert the correlation-breaker guarantee for their iteration.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_ofFn (n h L e : ℕ) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) : List.ofFn (matchedBlockExtractor n h L e x seed) = scheduledBlockExtractorBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L (List.ofFn x) (List.ofFn fun (i : Fin (scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L)) => (List.ofFn seed)[↑i]?.getD false)

On every parameter choice, the output is the actual program at its zero-completed seed word.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_ofFn_take (n h L e : ℕ) (size : scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L ≤ matchedBlockSeedBits L) (x : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) : List.ofFn (matchedBlockExtractor n h L e x seed) = scheduledBlockExtractorBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L (List.ofFn x) (List.take (scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L) (List.ofFn seed))

A sufficient seed budget makes the actual input precisely the prescribed seed prefix.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_xor (n h L e : ℕ) (x x' : Fin n → Bool) (seed : Fin (matchedBlockSeedBits L) → Bool) : matchedBlockExtractor n h L e (fun (i : Fin n) => x i ^^ x' i) seed = fun (j : Fin (matchedBlockOutputBits h L)) => matchedBlockExtractor n h L e x seed j ^^ matchedBlockExtractor n h L e x' seed j

For every fixed padded seed, source XOR becomes pointwise output XOR.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_seedBits_le (n h L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (room : 64 ≤ L) (depth : h ≤ 64) (error : e + h + 2 ≤ L) : scheduledBlockSeedBits n h (recursiveBlockReserve L (e + h + 2)) (e + h + 2) L ≤ matchedBlockSeedBits L

The finite validity conditions ensure that the padded seed contains the whole actual seed.

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

Any proved seed budget gives the actual padded program's strong guarantee.

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

Strong extraction retains all padded seed bits at the exact scheduled entropy threshold.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_depth24 (n L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (room : 64 ≤ L) (error : e + 24 + 2 ≤ L) : WeightedStrongSeededExtractor (matchedBlockExtractor n 24 L e) (2 ^ (2 ^ 62 * L)) (2 ^ e)⁻¹

Depth twenty-four matches the common seed width, with a simple linear entropy bound.

theorem Algebraic.Cutwidth.Extractor.matchedBlockExtractor_depth64 (n L e : ℕ) (length : Nat.clog 2 (n + 1) ≤ L) (room : 64 ≤ L) (error : e + 64 + 2 ≤ L) : WeightedStrongSeededExtractor (matchedBlockExtractor n 64 L e) (2 ^ (2 ^ 142 * L)) (2 ^ e)⁻¹

Depth sixty-four expands to the refresh width with its actual larger source entropy budget.