The (4 - ε) n lower bound

Assembling the cut-counting lemma, the wiring graph, and the graph-ordering hypothesis gives the circuit lower bound. A K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs and K polynomial in n needs more than (4 - ε) n gates over the full binary basis, for every ε > 0 and all sufficiently large n.

Two statements enter as hypotheses rather than being proved here:

• Multigraph.OrderingBound η C for every η > 0 and some C, the graph-ordering hypothesis on multigraphs of maximum degree three, which eventually_lt_size_of_pathwidthBound derives from the pathwidth hypothesis PathwidthBound for simple cubic graphs;
• a family f n with threshold K n ≤ n ^ c satisfying RectangleFree and the accepting-input bound.

The main theorem is eventually_lt_size. The fixed-n core is lt_size_of_bounds, whose numeric hypotheses are discharged asymptotically.

The proof organization, the threshold-edge charging, the application of a sumset extractor as the hard family, and the merge-tree restoration argument follow Ryan Williams's private working note A (4 − ε)n lower bound for Boolean circuits (September 2026), which uses the circuit-to-read-once compiler of the author's counting note. The formalization is the author's.

theorem Algebraic.Cutwidth.Multigraph.OrderingBound.mono {η C C' : ℝ} (h : OrderingBound η C) (hC : C ≤ C') : OrderingBound η C'

Increasing the additive constant weakens the ordering hypothesis.

theorem Algebraic.Cutwidth.sub_card_lt_clog {n : ℕ} {f : Cslib.BooleanFunction n} {K : ℕ} (hK : 1 < K) (hrect : RectangleFree f K) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (hbig : 2 * K ^ 2 ≤ 2 ^ (n - 2)) {R : Finset (Fin n)} (hR : DependsOnlyOn f R) : n - R.card < Nat.clog 2 K

A rectangle-free function with many accepting inputs cannot ignore ⌈log₂ K⌉ coordinates.

theorem Algebraic.Cutwidth.card_accepting_le_of_orderingBound {η C : ℝ} (hη : 0 ≤ η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound η C) {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree (fun (x : Cslib.BitString n) => p.eval Binary.interpretation x out) K) : (accepting fun (x : Cslib.BitString n) => p.eval Binary.interpretation x out).card < K * 2 ^ (n - (Wiring.read p out).card) ∨ ↑(accepting fun (x : Cslib.BitString n) => p.eval Binary.interpretation x out).card ≤ (↑n + 3 * ↑s) * 2 ^ ((1 / 3 + η) * max (↑s - ↑(Wiring.read p out).card) 0 + 3 * Real.logb 2 (↑n + 3 * ↑s) + C + 3) * ↑K ^ 2

The circuit-level bound: for a circuit with output gate out, either the final past set is small, so that fewer than K · 2 ^ (n - n') inputs are accepted, or the accepted inputs are bounded through the ordering hypothesis. Here n' is the number of inputs with a path to the output.

theorem Algebraic.Cutwidth.eventually_mul_logb_add_lt (A B : ℝ) {δ : ℝ} (hδ : 0 < δ) : ∀ᶠ (n : ℕ) in Filter.atTop, A * Real.logb 2 ↑n + B < δ * ↑n

Every fixed multiple of the binary logarithm, plus a constant, is eventually below every positive multiple of the input.

theorem Algebraic.Cutwidth.false_of_accepting_bound {η C : ℝ} (hη : 0 < η) (hη1 : η ≤ 1 / 18) (hC : 0 ≤ C) {n : ℕ} (hn : 2 ≤ n) {f : Cslib.BooleanFunction n} {K c : ℕ} (hK : K ≤ n ^ c) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (hK1 : 1 < K) (hpow : 8 * n ^ (2 * c) ≤ 2 ^ n) (hlog : (4 + 3 * ↑c) * Real.logb 2 ↑n + (C + 22) < 3 * η * ↑n) {s n' : ℕ} (hs : ↑s ≤ (4 - 18 * η) * ↑n) (hn'le : n' ≤ n) (hread : n - n' < Nat.clog 2 K) {Vb : ℝ} (hVpos : 0 < Vb) (hVb : Vb ≤ 16 * ↑n) (bound : (accepting f).card < K * 2 ^ (n - n') ∨ ↑(accepting f).card ≤ Vb * 2 ^ ((1 / 3 + η) * max (↑s - ↑n') 0 + 3 * Real.logb 2 Vb + C + 3) * ↑K ^ 2) : False

The numeric core. A K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs cannot satisfy the accepting-input bound of the cut-counting lemma for a circuit with s ≤ (4 - 18 η) n gates reading n' inputs, when n - n' < ⌈log₂ K⌉ and n is large enough. The bound is taken as a hypothesis so that the deterministic and nondeterministic assemblies share this argument.

theorem Algebraic.Cutwidth.lt_size_of_bounds {η C : ℝ} (hη : 0 < η) (hη1 : η ≤ 1 / 18) (hC : 0 ≤ C) (order : Multigraph.OrderingBound η C) {n : ℕ} (hn : 2 ≤ n) {f : Cslib.BooleanFunction n} {K c : ℕ} (hK : K ≤ n ^ c) (hacc : 2 ^ (n - 2) ≤ (accepting f).card) (hrect : RectangleFree f K) (hpow : 8 * n ^ (2 * c) ≤ 2 ^ n) (hlog : (4 + 3 * ↑c) * Real.logb 2 ↑n + (C + 22) < 3 * η * ↑n) (circuit : Circuit Binary.signature n 1) (computes : circuit.Computes Binary.interpretation fun (x : Fin n → Bool) (x_1 : Fin 1) => f x) : (4 - 18 * η) * ↑n < ↑circuit.size

The fixed-n core of the lower bound. With the graph-ordering hypothesis for slack η ≤ 1/18, a K-rectangle-free function with at least 2 ^ (n - 2) accepting inputs and K ≤ n ^ c needs more than (4 - 18 η) n binary gates, once n satisfies two explicit numeric conditions.

theorem Algebraic.Cutwidth.eventually_lt_size (order : ∀ (η : ℝ), 0 < η → ∃ (C : ℝ), Multigraph.OrderingBound η C) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (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

Theorem 1. Assume the graph-ordering lemma for every slack η > 0 and a family of functions f n that is K n-rectangle-free with K n ≤ n ^ c and at least 2 ^ (n - 2) accepting inputs, for all large n. Then for every ε > 0 and all sufficiently large n, every binary circuit computing f n has more than (4 - ε) n gates.

theorem Algebraic.Cutwidth.eventually_lt_size_of_pathwidthBound (pathwidth : ∀ (ξ : ℝ), 0 < ξ → ∃ (N₀ : ℕ), PathwidthBound ξ N₀) (f : (n : ℕ) → Cslib.BooleanFunction n) (K : ℕ → ℕ) (c : ℕ) (hK : ∀ᶠ (n : ℕ) in Filter.atTop, K n ≤ n ^ c) (hacc : ∀ᶠ (n : ℕ) in Filter.atTop, 2 ^ (n - 2) ≤ (accepting (f n)).card) (hrect : ∀ᶠ (n : ℕ) in Filter.atTop, RectangleFree (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

Theorem 1 from the pathwidth hypothesis. The graph-ordering hypothesis is replaced by the pathwidth bound for simple cubic graphs: for every ξ > 0 there is a threshold beyond which every simple 3-regular graph on h vertices has a path decomposition of width at most (1/6 + ξ) h.