Uniform one-shot extraction across all leaf blocks

The actual program applies one-shot extraction to a runtime number of fixed-width blocks with one shared pair of seed words. It emits exactly count.length*ell bits. On concatenated Boolean tuples and canonical field seeds, the output is exactly the serialized tuple of decoded one-shot outputs. This includes empty tuples and zero input or output widths.

The existing one-shot program supplies the condensation and hashing mechanism. Its shared-seed statistical use follows Chattopadhyay--Goodman--Liao, Lemma 5.5, https://eccc.weizmann.ac.il/report/2021/075/. This module certifies the uniform runtime leaf stage; it does not assert a polynomial-time evaluator for the complete variable-depth recursion.

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

Every requested input block contributes exactly ell output bits.

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

Fixed-width tuple inputs produce their individual one-shot outputs in the same order.

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

At canonical shared field seeds, the runtime word is the decoded statistical tuple serialized in block order, with field values 0,1 represented by Boolean bits.

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

Runtime unary parameters, payload, both seeds, and block count define one uniform FP map.