The scheduled condenser on arbitrary capped sources

The actual decoded runtime map strongly condenses every normalized weighted source with point masses at most 2^(-k). Its ideal output is normalized and has the same point-mass cap separately at every retained seed, with joint total variation error at most 2^(-e).

This extends the checked flat-source guarantee by exact finite mixtures. Inputs may use any injective encoding into words of the stated length; the fixed-length Boolean-vector specialization uses List.ofFn. The ideal real weights are statistical witnesses, not additional runtime inputs.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_weighted (n k e u : ℕ) {α : Type u_1} [Fintype α] [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) (input : α ↪ List Bool) (source : ∀ (x : α), (input x).length = n) : WeightedStrongSeededCondenser (fun (x : α) => decodedExplicitCondenser n k e u (input x)) (2 ^ k) (2 ^ k) (2 ^ e)⁻¹

The scheduled runtime condenser preserves the point-mass cap of every weighted source represented injectively by words of length n.

theorem Algebraic.Cutwidth.Extractor.decodedExplicitCondenser_weighted_ofFn (n k e u : ℕ) [Fintype (AdjoinRoot (binaryModulus (sparseFieldExponent u (explicitCondenserBudget n k e))))] (rate : 0 < u) : WeightedStrongSeededCondenser (fun (x : Fin n → Bool) => decodedExplicitCondenser n k e u (List.ofFn x)) (2 ^ k) (2 ^ k) (2 ^ e)⁻¹

The scheduled runtime condenser is strong on every capped distribution of fixed-length Boolean vectors, including zero-length inputs.