Transporting the actual bit program's retained-seed law

Exact program serialization identifies every output coordinate. The canonical seed codec and the two-element output equivalence then transport strong extraction without changing its cap or error. Finite-field instances are derived locally from the proved quotient cardinalities.

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

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

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

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