Finite budgets for the actual sumset source reduction

The single affine error budget pays exactly for all parity tests of order at most four and every candidate. The chosen parity bias satisfies the fourth-moment budget. At outer bit scale b >= 5, the selection theorem's discard allowance leaves a positive number of good coordinates and meets the majority theorem's square-root margin.

These finite estimates implement conservative parameters for Chattopadhyay--Liao, Extractors for Sum of Two Sources, Lemma 5.4, https://arxiv.org/pdf/2110.12652. They do not supply the sampler, source entropy, eventual parameter guards, or a uniform evaluation certificate.

theorem Algebraic.Cutwidth.Extractor.sourceReductionOuterCount_pos (b : ℕ) : 0 < sourceReductionOuterCount b

The outer index type is nonempty at every size.

theorem Algebraic.Cutwidth.Extractor.sourceReductionCandidateCount_pos (b : ℕ) : 0 < sourceReductionCandidateCount b

The candidate index type is nonempty at every size.

theorem Algebraic.Cutwidth.Extractor.sourceReductionTamperingCount_pos (b : ℕ) : 0 < sourceReductionTamperingCount b

The single actual affine construction has a positive tampering count.

theorem Algebraic.Cutwidth.Extractor.sourceReductionTamperingCount_add_one (b : ℕ) : sourceReductionTamperingCount b + 1 = 4 * sourceReductionCandidateCount b

The honest and tampered slots together hold four complete candidate families.

theorem Algebraic.Cutwidth.Extractor.sourceReductionAdviceLength_pos {b : ℕ} (positive : 0 < b) : 0 < sourceReductionAdviceLength b

A positive outer scale leaves room to flip an advice bit for unused slots.

theorem Algebraic.Cutwidth.Extractor.sourceReductionSamplerError_pos (b : ℕ) : 0 < sourceReductionSamplerError b

The sampler test allowance is positive.

theorem Algebraic.Cutwidth.Extractor.sourceReductionBadThreshold_pos (b : ℕ) : 0 < sourceReductionBadThreshold b

The strict bad-seed discrepancy threshold is positive.

theorem Algebraic.Cutwidth.Extractor.sourceReductionParityBias_nonneg (b : ℕ) : 0 ≤ sourceReductionParityBias b

The sign-parity bias parameter is nonnegative.

theorem Algebraic.Cutwidth.Extractor.sourceReduction_union_budget (b : ℕ) : ↑(sourceReductionOuterCount b) ^ 4 * ↑(sourceReductionCandidateCount b) * ((2 ^ sourceReductionTarget b)⁻¹ / sourceReductionBadThreshold b) = sourceReductionSamplerError b

The union of all fourth-order parity tests and candidate tests exactly spends the allowance.

theorem Algebraic.Cutwidth.Extractor.sourceReduction_moment_budget {b m : ℕ} (size : m ≤ sourceReductionOuterCount b) : 100 * ↑m ^ 2 * sourceReductionParityBias b ≤ 1

Every retained coordinate set satisfies the checked fourth-moment budget.

theorem Algebraic.Cutwidth.Extractor.sourceReduction_bad_count_bound (b : ℕ) : 2 * sourceReductionSamplerError b * ↑(sourceReductionOuterCount b) = 2 ^ (3 * b + 1)

The selection theorem's discard allowance has this exact dyadic size.

theorem Algebraic.Cutwidth.Extractor.sourceReduction_majority_guards {b m : ℕ} (large : 5 ≤ b) (size : m ≤ sourceReductionOuterCount b) (bad : ↑(sourceReductionOuterCount b - m) ≤ 2 * sourceReductionSamplerError b * ↑(sourceReductionOuterCount b)) : 0 < m ∧ ↑(sourceReductionOuterCount b - m) ≤ √↑m / 8

The actual selection allowance gives a positive good set and the required majority margin.