Serialization and statistical transport for the scheduled pair output

Reading two halves is injective on words of the prescribed length. Serialization is independently injective on field-coordinate vectors, and re-encoding the decoded runtime output gives its actual bits. Transporting the scheduled condenser through these two injections therefore preserves its conditional cap and joint statistical error.

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

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

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