Runtime composition and linearity of one-shot extraction

The fixed-width serializer recovers the scheduled condenser's exact output. The checked runtime hash then identifies the one-shot bit program with the statistical composition. Each component preserves addition in the source.

theorem Algebraic.Cutwidth.Extractor.Internal.encodeCondenserOutput_decodedExplicitCondenser (n k e u : ℕ) (source : List Bool) (seed : AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e)))) : let T := explicitCondenserBudget n k e; let s := sparseFieldExponent u T; let m := condenserCoordinates k (sparsePowerBits u T); encodeCondenserOutput s m (decodedExplicitCondenser n k e u source seed) = explicitCondenserBits n k e u source (BinaryFieldCodec.encode s seed)

theorem Algebraic.Cutwidth.Extractor.Internal.decodedOneShotExtractor_eq_composition (n ell e : ℕ) (source : List Bool) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) : let T := explicitCondenserBudget n (ell + 2 * e) (e + 1); let sC := oneShotCondenserExponent n ell e; let sH := oneShotHashExponent n ell e; let m := condenserCoordinates (ell + 2 * e) (sparsePowerBits 1 T); decodedOneShotExtractor n ell e source seeds = binaryFieldHash sH ell (BinaryFieldCodec.decode sH (encodeCondenserOutput sC m (decodedExplicitCondenser n (ell + 2 * e) (e + 1) 1 source seeds.1))) seeds.2

theorem Algebraic.Cutwidth.Extractor.Internal.decodedOneShotExtractor_addBits (n ell e : ℕ) (a b : List Bool) (seeds : AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)) × AdjoinRoot (binaryModulus (oneShotHashExponent n ell e))) : decodedOneShotExtractor n ell e (Complexity.BitPolynomial.addBits a b) seeds = decodedOneShotExtractor n ell e a seeds + decodedOneShotExtractor n ell e b seeds