From sumset extraction to circuit hardness

Zero-padding the two sides of a coordinate rectangle gives independent flat sources whose XOR is the glued input. Flat-source sumset extraction therefore implies Balanced, then rectangle-freeness and the accepting-input bound. These are the combinatorial bridges for the extractor route in Ryan Williams's September 2026 working note. The cubic bisection and pathwidth theorems are proved. The new deterministic, nondeterministic, and average-case endpoints instantiate these graph bounds. SourceReduction.Construction.Hardness supplies an explicit extractor family and proves its deterministic bounds. The generic interfaces with explicit graph bounds are retained.

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

Nontrivial extraction excludes singleton sources, so its support-size threshold is at least two.

theorem Algebraic.Cutwidth.flatSumsetExtractor_singleBit : FlatSumsetExtractor (fun (x : Fin 1 → Bool) => x 0) 2 0

On a single bit, XOR of two full-support uniform sources is exactly uniform. This is a non-vacuous zero-error instance of the extractor contract.

theorem Algebraic.Cutwidth.FlatSumsetExtractor.balanced {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) : Balanced f K ν

Independent uniform rectangle sides become flat sumset sources by zero-padding their complementary coordinates.

theorem Algebraic.Cutwidth.Balanced.rectangleFree {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (balanced : Balanced f K ν) (hK : 0 < K) (hν : ν < 1 / 2) : RectangleFree f K

Error strictly below one half excludes a monochromatic one-rectangle with both sides at least the extraction threshold.

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

A flat sumset extractor is rectangle-free at the same threshold.

theorem Algebraic.Cutwidth.FlatSumsetExtractor.card_accepting_bounds {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hK : K ≤ 2 ^ (n / 2)) : (1 / 2 - ν) * 2 ^ n ≤ ↑(accepting f).card ∧ ↑(accepting f).card ≤ (1 / 2 + ν) * 2 ^ n

The full cube has accepting density within the extraction error of one half, provided each half of its coordinates supports a large enough source.

theorem Algebraic.Cutwidth.FlatSumsetExtractor.card_accepting_ge {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} {ν : ℝ} (extract : FlatSumsetExtractor f K ν) (hν : ν ≤ 1 / 4) (hn : 2 ≤ n) (hK : K ≤ 2 ^ (n / 2)) : 2 ^ (n - 2) ≤ (accepting f).card

Error at most one quarter gives the density required by the circuit lower bound, including odd input lengths.

theorem Algebraic.Cutwidth.eventually_hard_of_flatSumsetExtractor {f : (n : ℕ) → Cslib.BooleanFunction n} {K : ℕ → ℕ} {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (f n) (K n) ∧ 2 ^ (n - 2) ≤ (accepting (f n)).card

Sublinear source entropy and error at most one quarter supply both hard-family hypotheses of the circuit lower bound for all large inputs.

theorem Algebraic.Cutwidth.eventually_lt_size_of_flatSumsetExtractor (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound (1 / 3) η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (4 - ε) * ↑n < ↑circuit.size

The extractor route to the coefficient-four lower bound. Only sublinear source entropy is needed, with any fixed error at most one quarter. This generic interface keeps the graph-ordering bound as an explicit parameter.

theorem Algebraic.Cutwidth.eventually_lt_size_of_pathwidthBound_of_flatSumsetExtractor (pathwidth : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), PathwidthBound (1 / 6) ξ N₀) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (4 - ε) * ↑n < ↑circuit.size

The extractor-to-circuit bridge with the cubic pathwidth theorem as its graph-theoretic prerequisite.

theorem Algebraic.Cutwidth.eventually_lt_size_of_bisectionBound_of_flatSumsetExtractor (bisection : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), BisectionBound ξ N₀) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (4 - ε) * ↑n < ↑circuit.size

The generic extractor route with an explicit cubic bisection bound. The extraction-to-rectangle and bisection-to-pathwidth reductions are proved.

theorem Algebraic.Cutwidth.nondet_eventually_lt_size_of_flatSumsetExtractor (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound (1 / 3) η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ) (circuit : Circuit Binary.signature (n + m) 1), NondetComputes circuit (f n) → (4 - ε) * ↑n < ↑circuit.size

Flat sumset extraction also gives the coefficient-four lower bound against nondeterministic circuits with arbitrarily many witness inputs.

theorem Algebraic.Cutwidth.eventually_lt_size_of_flatSumsetExtractor_of_log_sublinear (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), (circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f n x) → (4 - ε) * ↑n < ↑circuit.size

Flat sumset extraction at sublinear source entropy gives the deterministic coefficient-four lower bound with all graph bounds instantiated.

theorem Algebraic.Cutwidth.nondet_eventually_lt_size_of_flatSumsetExtractor_of_log_sublinear (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) {ν : ℝ} (hν : ν ≤ 1 / 4) (hK : (fun (n : ℕ) => Real.logb 2 ↑(K n)) =o[Filter.atTop] fun (n : ℕ) => ↑n) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (m : ℕ) (circuit : Circuit Binary.signature (n + m) 1), NondetComputes circuit (f n) → (4 - ε) * ↑n < ↑circuit.size

Flat sumset extraction at sublinear source entropy gives the same lower bound with unrestricted nondeterministic witnesses and no graph hypothesis.

theorem Algebraic.Cutwidth.eventually_card_agree_le_of_flatSumsetExtractor (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) {ν : ℝ} (hν : 0 ≤ ν) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (extract : ∀ᶠ (n : ℕ) in Filter.atTop, FlatSumsetExtractor (f n) (K n) ν) {ε : ℝ} (hε : 0 < ε) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (circuit : Circuit Binary.signature n 1), ↑circuit.size ≤ (4 - ε) * ↑n → ↑{x : Fin n → Bool | circuit.eval Binary.interpretation x 0 = f n x}.card ≤ (1 / 2 + 3 * ν) * 2 ^ n + 2 ^ ((1 - ε / 24) * ↑n)

Polynomial-threshold flat sumset extraction gives the average-case agreement bound using the proved graph theorems.