Fixed-width semantics and uniformity of shared-seed leaf extraction

Each slice is one runtime input to the existing one-shot extractor. Equal input widths recover the original tuple, and equal output widths recover the decoded statistical tuple. Polynomial-time range concatenation keeps all numerical parameters, both seeds, and the block count as runtime data.

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotBlockExtractorBits_length (n ell e : ℕ) (blocks condenserSeed hashSeed count : List Bool) : (oneShotBlockExtractorBits n ell e blocks condenserSeed hashSeed count).length = count.length * ell

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotBlockExtractorBits_ofFn (n ell e : ℕ) {t : ℕ} (blocks : Fin t → Fin n → Bool) (condenserSeed hashSeed count : List Bool) (size : count.length = t) : oneShotBlockExtractorBits n ell e (List.ofFn fun (i : Fin t) => List.ofFn (blocks i)).flatten condenserSeed hashSeed count = (List.ofFn fun (i : Fin t) => oneShotExtractorBits n ell e (List.ofFn (blocks i)) condenserSeed hashSeed).flatten

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotBlockExtractorBits_eq_decoded (n ell e : ℕ) {t : ℕ} (blocks : Fin t → Fin n → Bool) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) (count : List Bool) (size : count.length = t) : oneShotBlockExtractorBits n ell e (List.ofFn fun (i : Fin t) => List.ofFn (blocks i)).flatten (BinaryFieldCodec.encode (oneShotCondenserExponent n ell e) seeds.1) (BinaryFieldCodec.encode (oneShotHashExponent n ell e) seeds.2) count = (List.ofFn fun (i : Fin t) => List.ofFn fun (j : Fin ell) => decide (decodedOneShotExtractor n ell e (List.ofFn (blocks i)) seeds j = 1)).flatten

theorem Algebraic.Cutwidth.Extractor.Internal.oneShotBlockExtractorBits_mem_FP {n ell e : List Bool → ℕ} {blocks condenserSeed hashSeed count : List Bool → List Bool} (hn : Complexity.UnaryFn n) (hell : Complexity.UnaryFn ell) (he : Complexity.UnaryFn e) (hblocks : blocks ∈ Complexity.FP) (hcondenser : condenserSeed ∈ Complexity.FP) (hhash : hashSeed ∈ Complexity.FP) (hcount : count ∈ Complexity.FP) : (fun (z : List Bool) => oneShotBlockExtractorBits (n z) (ell z) (e z) (blocks z) (condenserSeed z) (hashSeed z) (count z)) ∈ Complexity.FP