Flattening the actual program and retaining padded seed bits #
The flat output is a bijective rearrangement of the scheduled Boolean
blocks. The exact seed prefix is then extended by independent unused bits,
using the checked strong seed-padding theorem. The finite numerical bounds
are those of Scheduled.BoundedDepth; no field instances are supplied.
theorem
Algebraic.Cutwidth.Extractor.Internal.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)
theorem
Algebraic.Cutwidth.Extractor.Internal.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))
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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
theorem
Algebraic.Cutwidth.Extractor.Internal.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)⁻¹
theorem
Algebraic.Cutwidth.Extractor.Internal.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)⁻¹