Flat-source bookkeeping for the actual construction

The maximum entropy reserve supplies the original affine point-mass cap and the sampler support threshold. Restricting the ambient flat-weight average to its support changes neither its value nor its normalization.

theorem Algebraic.Cutwidth.Extractor.Internal.weightedMean_flatWeight {α : Type u_1} [Fintype α] (P : Finset α) (f : α → ℝ) : weightedMean Finset.univ (flatWeight P) f = weightedMean P (fun (x : α) => 1 / ↑P.card) f

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_flatWeight_cap (n L : ℕ) (P : Finset (Fin n → Bool)) (size : 2 ^ sourceReductionEntropy n L ≤ P.card) (x : Fin n → Bool) : flatWeight P x ≤ (2 ^ affineLeakageSourceEntropy n (sourceReductionTamperingCount (matchedBlockSeedBits L)) (sourceReductionAdviceLength (matchedBlockSeedBits L)) (sourceReductionTarget (matchedBlockSeedBits L)))⁻¹

theorem Algebraic.Cutwidth.Extractor.Internal.sourceReduction_sampler_threshold (n L : ℕ) (Q : Finset (Fin n → Bool)) (size : 2 ^ sourceReductionEntropy n L ≤ Q.card) : 2 ^ amplifiedMatchedSamplerEntropy L (sourceReductionSeedBits n L) ≤ ↑Q.card