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 dense
rectangle-free family with sublinear logarithmic threshold. The bound
Wiring.card_vertex_le_two_mul_size makes the graph size independent of the
number of declared inputs, so the witness count m is unrestricted.
nondet_eventually_lt_size_of_rectangleFree instantiates the proved graph
bounds and only needs log₂ K(n) = o(n), rectangle-freeness, and the
accepting-input bound. The explicit family Extractor.sourceReductionHardFamily
meets these hypotheses through balanced padding, but no nondeterministic
corollary for it is stated; SourceReduction.Construction.Hardness states its
deterministic bounds. The generic graph-ordering interfaces are retained; as
in the deterministic case, an ordering coefficient A > 0 gives the
circuit coefficient 1 + 1/A (nondet_eventually_lt_size_of_orderingBound),
and a cubic cutwidth coefficient c gives 1 + 1/(2c).
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.
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)
Instances For
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
Instances For
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)
Instances For
The forgotten wiring network computes the nondeterministic gate function.
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.
The fixed-n nondeterministic core with a general ordering
coefficient. The hypotheses are those of lt_size_of_orderingBound. The
number of witness inputs is unrestricted: only the reachable graph, with at
most 2 s + 1 vertices, enters the counting argument.
The fixed-n core for nondeterministic circuits. The logarithmic
conditions are those of lt_size_of_log_bounds. The number of witness inputs
is unrestricted: only the reachable graph, with at most 2 s + 1 vertices,
enters the counting argument.
The polynomial-threshold nondeterministic bound with an arbitrary number of witness inputs.
Nondeterministic circuits with a general ordering coefficient. Under
the hypotheses of eventually_lt_size_of_orderingBound, for every ε > 0 and
all sufficiently large n, every circuit on n + m inputs that computes
f n nondeterministically has more than (1 + 1/A - ε) n gates, uniformly
over every number m of witness inputs.
Nondeterministic circuits from a cubic cutwidth bound. A cutwidth
coefficient c > 0 at every positive slack gives the nondeterministic
coefficient 1 + 1/(2c).
Nondeterministic circuits from a cubic pathwidth bound with coefficient
p. A pathwidth coefficient p > 0 at every positive slack gives the
nondeterministic coefficient 1 + 1/(2p).
Sublinear source entropy suffices for the nondeterministic coefficient-four
bound, uniformly over every number of witness inputs. This is
nondet_eventually_lt_size_of_orderingBound at A = 1/3.
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 that
computes f n nondeterministically has more than (4 - ε) n gates.
Nondeterministic circuits from the pathwidth hypothesis.
A dense rectangle-free family with sublinear logarithmic threshold
requires more than (4 - ε) n gates even with arbitrarily many witness
inputs. All graph bounds are instantiated by the proved cubic theorem.