Weighted-source correctness of the actual one-shot program

An injective fixed-length encoding sends every flat source support to a support of the same size. The checked flat program theorem therefore applies, and the weighted-source extension keeps exactly the same error.

theorem Algebraic.Cutwidth.Extractor.Internal.decodedOneShotExtractor_weightedStrongSeededExtractor (n ell e : ℕ) {α : Type u_1} [Fintype α] [Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)))] [Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent n ell e)))] (input : α ↪ List Bool) (source : ∀ (x : α), (input x).length = n) : WeightedStrongSeededExtractor (fun (x : α) => decodedOneShotExtractor n ell e (input x)) (2 ^ (ell + 2 * e)) (2 ^ e)⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.decodedOneShotExtractor_ofFn_weighted (n ell e : ℕ) [Fintype (AdjoinRoot (binaryModulus (oneShotCondenserExponent n ell e)))] [Fintype (AdjoinRoot (binaryModulus (oneShotHashExponent n ell e)))] : WeightedStrongSeededExtractor (fun (x : Fin n → Bool) => decodedOneShotExtractor n ell e (List.ofFn x)) (2 ^ (ell + 2 * e)) (2 ^ e)⁻¹