Uniform evaluation and robustness of majority

The final majority stage in Chattopadhyay and Liao's constant-error sumset extractor has a uniform polynomial-time evaluator in Complexitylib's machine model. A strict good-coordinate margin larger than the number of bad coordinates forces the verdict, regardless of how the bad bits depend on the good bits.

These are only properties of the final stage; no sumset-extraction guarantee is claimed without the preceding source reduction and its probabilistic analysis.

@[simp]

theorem Algebraic.Cutwidth.Extractor.majorityEval_toList {n : ℕ} (x : Complexity.BitString n) : majorityEval x.toList = [Complexity.majority x]

Majority agrees exactly with the existing finite-vector majority, under the standard list encoding.

theorem Algebraic.Cutwidth.Extractor.majorityEval_mem_FP : majorityEval ∈ Complexity.FP

The majority evaluator is uniform polynomial time in the repository's deterministic Turing-machine model.

theorem Algebraic.Cutwidth.Extractor.majority_eq_true_of_margin {n : ℕ} {good : Finset (Fin n)} {x : Fin n → Bool} (h : ↑(n - good.card) < voteMargin good x) : Complexity.majority x = true

More positive good votes than all possible negative bad votes forces a true majority, without any independence condition on the bad coordinates.

theorem Algebraic.Cutwidth.Extractor.majority_eq_false_of_margin {n : ℕ} {good : Finset (Fin n)} {x : Fin n → Bool} (h : voteMargin good x ≤ -↑(n - good.card)) : Complexity.majority x = false

A sufficiently negative good margin forces false even if every bad coordinate votes true. Ties follow the evaluator's false convention.