Near-halving strong extraction on ordinary Boolean vectors

The full uniform Boolean seed decodes to the exact retained field-seed tuple. Outputs use a single Boolean index in block order. Bijections preserve the strong-extraction guarantee, with no caller-supplied field enumeration instances. The exact list identity fixes the representation needed by the separate string evaluator.

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

Boolean seed and output transport preserves the complete recursive error bound.

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

The Boolean-vector map extracts with error 2^(-e) at local exponent e+h+2.

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

Listing the Boolean output reads the semantic tuple in consecutive block order.