Exact finite union and majority budgets

Power identities are first proved at symbolic exponents. The final margin bound uses the discarded-coordinate allowance 2^(3b+1), at most half the outer coordinates and at most one eighth of the square root of their retained count when b >= 5.

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

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

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

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

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

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

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

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

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

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

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

theorem Algebraic.Cutwidth.Extractor.Internal.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