Boolean seed and output transport for near-halving extraction

The exact seed codec and the two-element field equivalence preserve the joint strong-extraction tests. Uncurrying through the finite product equivalence places output coordinates in block order. Field finiteness is derived locally from the proved quotient cardinalities.

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockBooleanExtractor_weighted (n h Q E : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) E + 4 * E ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockBooleanExtractor n h Q E) (2 ^ nearHalvingBlockEntropy h Q 0) ((3 * 2 ^ h - 1) * (2 ^ E)⁻¹)

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockBooleanExtractor_dyadic (n h Q e : ℕ) (capacity : nearHalvingBlockEntropy h Q 0 ≤ n) (budget : 12 * (nearHalvingBlockRate h + 1) * explicitCondenserBudget n (nearHalvingBlockEntropy h Q 0) (e + h + 2) + 4 * (e + h + 2) ≤ Q) : WeightedStrongSeededExtractor (nearHalvingBlockBooleanExtractor n h Q (e + h + 2)) (2 ^ nearHalvingBlockEntropy h Q 0) (2 ^ e)⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.nearHalvingBlockBooleanExtractor_ofFn (n h Q E : ℕ) (x : Fin n → Bool) (seed : Fin (nearHalvingBlockSeedBits n h Q E) → Bool) : List.ofFn (nearHalvingBlockBooleanExtractor n h Q E x seed) = (List.ofFn fun (i : Fin (recursiveBlockCount 1 h)) => List.ofFn fun (j : Fin (nearHalvingBlockLeafLength h Q)) => decide (nearHalvingBlockExtractor n h Q E x (decodeNearHalvingBlockSeeds n h Q E (List.ofFn seed)) i j = 1)).flatten