Balanced padding permits any fixed extraction error below one half

If f extracts with error strictly below one half, balancePad f is exactly balanced and rectangle-free at twice the original threshold. The list evaluator preserves uniform polynomial time. In particular, the lower bound does not need an extractor error of one quarter solely to ensure accepting-input density.

theorem Algebraic.Cutwidth.FlatSumsetExtractor.disperser {n K : ℕ} {f : Cslib.BooleanFunction n} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hK : 0 < K) (hν : ν < 1 / 2) : FlatSumsetDisperser f K

Error strictly below one half guarantees both output values on every large flat-source pair.

theorem Algebraic.Cutwidth.FlatSumsetDisperser.balancePad {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) : FlatSumsetDisperser (Cutwidth.balancePad f) (2 * K)

A two-sided sumset disperser remains one after balanced padding, with a factor-two loss in support threshold.

theorem Algebraic.Cutwidth.FlatSumsetDisperser.rectangleFree {n K : ℕ} {f : Cslib.BooleanFunction n} (disperse : FlatSumsetDisperser f K) : RectangleFree f K

Dispersion excludes one-rectangles, without any accepting-density assumption.

theorem Algebraic.Cutwidth.FlatSumsetExtractor.balancePad_rectangleFree {n K : ℕ} {f : Cslib.BooleanFunction n} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hK : 0 < K) (hν : ν < 1 / 2) : RectangleFree (balancePad f) (2 * K)

Any extraction error strictly below one half yields a rectangle-free balanced extension.

theorem Algebraic.Cutwidth.card_accepting_balancePad {n : ℕ} (f : Cslib.BooleanFunction n) : (accepting (balancePad f)).card = 2 ^ n

Exactly one fresh bit accepts for each old input, so balanced padding accepts exactly half its input cube.

theorem Algebraic.Cutwidth.balancePadEval_toList {n : ℕ} {f : Cslib.BooleanFunction n} {eval : List Bool → List Bool} (heval : ∀ (x : Complexity.BitString n), eval x.toList = [f x]) (x : Complexity.BitString (n + 1)) : balancePadEval eval x.toList = [balancePad f x]

The list evaluator agrees with the finite Boolean-function padding on every positive input length.

theorem Algebraic.Cutwidth.balancePadEval_mem_FP {eval : List Bool → List Bool} (heval : eval ∈ Complexity.FP) : balancePadEval eval ∈ Complexity.FP

Balanced padding preserves a uniform polynomial-time evaluator.