The scheduled condenser with two equal Boolean-vector outputs

Splitting the actual serialized output into two consecutive halves preserves its length, entropy threshold, and statistical error. The field bit width is even, so no padding or rounding loss is needed. Each half has alphabet size 2^H, where H = explicitCondenserHalfWidth n k e u, including H = 0.

This represents the existing scheduled condenser in the pair-output form used by block splitting. The underlying algebraic map and parameter source credits remain in Condenser.Polynomial and Parameters.Sparse. No recursive parameter schedule or polynomial-time certificate for a block loop is asserted.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserHalfWidth_double (n k e u : ℕ) : explicitCondenserHalfWidth n k e u + explicitCondenserHalfWidth n k e u = condenserCoordinates k (sparsePowerBits u (explicitCondenserBudget n k e)) * sparseFieldBits u (explicitCondenserBudget n k e)

Two halves cover the exact coordinate output width, without padding.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserHalfWidth_rate (n k e u : ℕ) : u * (explicitCondenserHalfWidth n k e u + explicitCondenserHalfWidth n k e u) ≤ (u + 1) * k + u * sparseFieldBits u (explicitCondenserBudget n k e)

Representing the output as two halves retains the original exact rate bound.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserPair_fst (n k e u : ℕ) (x : Fin n → Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) (i : Fin (explicitCondenserHalfWidth n k e u)) : (explicitCondenserPair n k e u x seed).1 i = (explicitCondenserBits n k e u (List.ofFn x) (BinaryFieldCodec.encode (sparseFieldExponent u (explicitCondenserBudget n k e)) seed))[↑i]?.getD false

The first half reads the beginning of the actual program output.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserPair_snd (n k e u : ℕ) (x : Fin n → Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) (i : Fin (explicitCondenserHalfWidth n k e u)) : (explicitCondenserPair n k e u x seed).2 i = (explicitCondenserBits n k e u (List.ofFn x) (BinaryFieldCodec.encode (sparseFieldExponent u (explicitCondenserBudget n k e)) seed))[explicitCondenserHalfWidth n k e u + ↑i]?.getD false

The second half immediately follows the first in the actual program output.

theorem Algebraic.Cutwidth.Extractor.explicitCondenserPair_weighted (n k e u : ℕ) [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) : WeightedStrongSeededCondenser (explicitCondenserPair n k e u) (2 ^ k) (2 ^ k) (2 ^ e)⁻¹

The actual paired output strongly condenses every capped input source with the same entropy threshold and error as its field-coordinate representation.