The (4 - ε) n bound for nondeterministic circuits

A nondeterministic circuit for f : {0,1}ⁿ → {0,1} is a circuit on n + m inputs whose accepted inputs x are exactly those with some witness y for which the output is 1. Witness inputs are read by the wiring graph but carry no port of the function computed, so the cut-counting lemma applies to the forgotten network (Network.forget) with the same multigraph. The excess of the wiring graph is the number of reachable gates minus the number of reachable inputs, ordinary and witness alike, which is at most the number of gates minus the number of ordinary inputs read. Hence the same bound holds: nondeterminism does not reduce the size below (4 - ε) n for any rectangle-free family with the hypotheses of eventually_lt_size.

The proof organization, the threshold-edge charging, the extractor application, and the graph restoration argument of the deterministic bound follow Ryan Williams's private working note (September 2026); this module only replaces the wiring network by its forgotten version.

noncomputable def Algebraic.Cutwidth.nondetFunction {n m : ℕ} (circuit : Circuit Binary.signature (n + m) 1) : Cslib.BooleanFunction n

The Boolean function computed nondeterministically by a circuit on n + m inputs: x is accepted when some witness y makes the output 1.

Equations

• Algebraic.Cutwidth.nondetFunction circuit x = decide (∃ (y : Fin m → Bool), circuit.eval Algebraic.Binary.interpretation (Fin.append x y) 0 = true)

def Algebraic.Cutwidth.NondetComputes {n m : ℕ} (circuit : Circuit Binary.signature (n + m) 1) (f : Cslib.BooleanFunction n) : Prop

A circuit on n + m inputs computes f nondeterministically when f x = 1 exactly when some witness makes the output 1.

Equations

• Algebraic.Cutwidth.NondetComputes circuit f = ∀ (x : Cslib.BitString n), f x = true ↔ ∃ (y : Fin m → Bool), circuit.eval Algebraic.Binary.interpretation (Fin.append x y) 0 = true

theorem Algebraic.Cutwidth.NondetComputes.eq_nondetFunction {n m : ℕ} {circuit : Circuit Binary.signature (n + m) 1} {f : Cslib.BooleanFunction n} (h : NondetComputes circuit f) : f = nondetFunction circuit

noncomputable def Algebraic.Cutwidth.nondetGateFunction {n m s : ℕ} (p : Program Binary.signature (n + m) s) (out : Fin s) : Cslib.BooleanFunction n

The function computed nondeterministically by a program with m witness inputs and output gate out.

Equations

• Algebraic.Cutwidth.nondetGateFunction p out x = decide (∃ (y : Fin m → Bool), p.eval Algebraic.Binary.interpretation (Fin.append x y) out = true)

theorem Algebraic.Cutwidth.forget_network_computes {n m s : ℕ} (p : Program Binary.signature (n + m) s) (out : Fin s) : (Wiring.network p out).forget.Computes (nondetGateFunction p out)

The forgotten wiring network computes the nondeterministic gate function.

theorem Algebraic.Cutwidth.nondet_card_accepting_le_of_orderingBound {η C : ℝ} (hη : 0 ≤ η) (hC : 0 ≤ C) (order : Multigraph.OrderingBound η C) {n m s : ℕ} (p : Program Binary.signature (n + m) s) (out : Fin s) {K : ℕ} (hK : 1 < K) (hrect : RectangleFree (nondetGateFunction p out) K) : (accepting (nondetGateFunction p out)).card < K * 2 ^ (n - (Wiring.network p out).forget.read.card) ∨ ↑(accepting (nondetGateFunction p out)).card ≤ (↑n + ↑m + 3 * ↑s) * 2 ^ ((1 / 3 + η) * max (↑s - ↑(Wiring.network p out).forget.read.card) 0 + 3 * Real.logb 2 (↑n + ↑m + 3 * ↑s) + C + 3) * ↑K ^ 2

The nondeterministic version of the circuit-level bound: the ordinary inputs read are those of the forgotten network, and the excess of the wiring graph is at most s minus their number.

theorem Algebraic.Cutwidth.nondet_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) {m : ℕ} (hm : m ≤ n) (circuit : Circuit Binary.signature (n + m) 1) (computes : NondetComputes circuit f) : (4 - 18 * η) * ↑n < ↑circuit.size

The fixed-n core for nondeterministic circuits. The hypotheses are those of lt_size_of_bounds with the number of witness inputs m at most n, so that the vertex count stays below 16 n.

theorem Algebraic.Cutwidth.nondet_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, ∀ m ≤ n, ∀ (circuit : Circuit Binary.signature (n + m) 1), NondetComputes circuit (f n) → (4 - ε) * ↑n < ↑circuit.size

Nondeterministic circuits. Under the graph-ordering hypothesis and the hypotheses of eventually_lt_size on the family f n, for every ε > 0 and all sufficiently large n, every circuit on n + m inputs with m ≤ n that computes f n nondeterministically has more than (4 - ε) n gates.

theorem Algebraic.Cutwidth.nondet_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, ∀ m ≤ n, ∀ (circuit : Circuit Binary.signature (n + m) 1), NondetComputes circuit (f n) → (4 - ε) * ↑n < ↑circuit.size

Nondeterministic circuits from the pathwidth hypothesis.