A uniform runtime level of shared-seed block condensation

One polynomial-time map applies the actual scheduled condenser to every fixed-width input block, reusing the supplied seed and preserving block order. The width, entropy and error parameters, rate, seed, payload, and unary block count remain runtime operands. Concatenated Boolean tuples recover exactly the concatenation of their individual condenser outputs, including zero width and zero blocks.

The underlying algebraic map and parameter source credits remain in Condenser.Polynomial and Parameters.Sparse. This certifies one level only. Recursion.Scheduled.Program iterates the levels under a uniform numerical schedule (scheduledBlockExtractorEval_mem_FP).

theorem Algebraic.Cutwidth.Extractor.explicitBlockCondenserBits_length (n k e u : ℕ) (blocks seed count : List Bool) : (explicitBlockCondenserBits n k e u blocks seed count).length = count.length * (condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e)) * sparseFieldBits u (explicitCondenserBudget n k e))

Every requested block contributes one scheduled output of the exact selected width.

theorem Algebraic.Cutwidth.Extractor.explicitBlockCondenserBits_ofFn (n k e u : ℕ) {t : ℕ} (blocks : Fin t → Fin n → Bool) (seed count : List Bool) (size : count.length = t) : explicitBlockCondenserBits n k e u (List.ofFn fun (i : Fin t) => List.ofFn (blocks i)).flatten seed count = (List.ofFn fun (i : Fin t) => explicitCondenserBits n k e u (List.ofFn (blocks i)) seed).flatten

Flattening a fixed-width tuple and running the program gives exactly the individual scheduled outputs in the same order, all with the same seed.

theorem Algebraic.Cutwidth.Extractor.explicitBlockCondenserBits_mem_FP {n k e u : List Bool → ℕ} {blocks seed count : List Bool → List Bool} (hn : Complexity.UnaryFn n) (hk : Complexity.UnaryFn k) (he : Complexity.UnaryFn e) (hu : Complexity.UnaryFn u) (hblocks : blocks ∈ Complexity.FP) (hseed : seed ∈ Complexity.FP) (hcount : count ∈ Complexity.FP) : (fun (z : List Bool) => explicitBlockCondenserBits (n z) (k z) (e z) (u z) (blocks z) (seed z) (count z)) ∈ Complexity.FP

Runtime parameters and a runtime unary block count compose into one uniform polynomial-time level; the result is the raw concatenation of all block outputs.