Fixed-width correctness and uniformity of one block-condensation level

The exact runtime length is independent of the source bits. Fixed-width slicing recovers every encoded input block, including blocks of width zero. Polynomial-time range concatenation then composes the existing uniform scheduled condenser without fixing the block count or numerical parameters.

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

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

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