The single-cut criterion #
Split the wires of a circuit, its inputs and its gates, into a set S and its complement. Let
i be the number of inputs in S, let A = forward p S be the signals computed in S and
read outside S, and let B = backward p S be the signals computed outside S and read in
S. A signal is the value of one wire, counted once however many gates read it.
The single-cut criterion (card_accepting_le, card_accepting_lt). If a single-output
circuit computes a K-rectangle-free function f, then for every such split
|f⁻¹(1)| ≤ (K - 1) (2 ^ (i + |B|) + 2 ^ (n - i + |A|)) < K (2 ^ (i + |B|) + 2 ^ (n - i + |A|)).
With at least 2 ^ (n - 2) accepted inputs this gives
n ≤ max (i + |B|) (n - i + |A|) + ⌈log₂ K⌉ + 2 (le_max_add_clog), hence
max (i + |B|) (n - i + |A|) > n - log₂ K - 3 (sub_logb_lt_max).
The proof fixes the values (a, b) of the forward and backward signals (the boundary key).
Two facts hold for every signature and value type:
- Cut and paste (
trace_mix): if two inputs have the same boundary key, the input taking the first input's coordinates onSand the second's elsewhere evaluates like the first onSand like the second outsideS. So the inputs with a fixed key, and the accepted inputs with a fixed key, form a product of a left part and a right part (card_filter_boundaryKey_eq), and the latter product is a one-rectangle off. - Determination (
trace_eq_of_agree_backward,trace_eq_of_agree_forward): the inputs inSand the backward values determine every value inS; symmetrically outsideS. So for a fixedbthe left parts of different keys are disjoint, and the left parts of all keys number at most2 ^ (i + |B|)in total (sum_card_leftParts_le); symmetrically the right parts number at most2 ^ (n - i + |A|)(sum_card_rightParts_le).
A rectangle with a side below K has at most K - 1 times its other side many points, and
summing over the keys gives the criterion.
The structural results are stated for programs with any number of outputs, any signature, and
any value type, so they apply equally to multi-output circuits: an output carried by a wire in
S is a function of the left part on each fibre, and an output carried by a wire outside S is
a function of the right part.
As a remark connecting to orderings (exists_prefix_le), every injective ranking of the wires
has a prefix containing half of the inputs, so some prefix is crossed by at least
⌊n/2⌋ - ⌈log₂ K⌉ - 2 signals.
Cut and paste, and determination #
Cut and paste. If two inputs agree on the forward and backward signals of S, the
mixed input has the values of the first input on S and of the second outside S.
Determination. The inputs placed in S and the backward signal values determine every
value on S.
Determination outside the cut. The inputs placed outside S and the forward signal
values determine every value outside S.
Equal boundary keys mean agreement on the forward signals.
Equal boundary keys mean agreement on the backward signals.
Mixing two inputs with equal boundary keys keeps the key.
Left parts and backward values determine the key. Two inputs with the same left part and the same backward values have the same forward values.
Right parts and forward values determine the key. Two inputs with the same right part and the same forward values have the same backward values.
Product fibres and partition bounds #
Fibres are closed under mixing. If Z is closed under mixing inputs with equal keys,
so is the set of members of Z with a given key.
Product fibres. If Z is closed under mixing inputs with equal keys (for example all
inputs, or the inputs on which an output wire carries a fixed value), the members of Z with
a given key are in bijection with the product of their left and right parts.
There are at most |U| ^ (|A| + |B|) boundary keys.
For a fixed backward part, the left parts partition the left inputs. Summed over the
keys realized in Z, the left parts number at most |U| ^ (i + |B|).
For a fixed forward part, the right parts partition the right inputs. Summed over the
keys realized in Z, the right parts number at most |U| ^ (n - i + |A|).
The criterion #
The single-cut criterion for a wire. If the wire out of a program carries a
K-rectangle-free function f, then for every set S of wires,
|f⁻¹(1)| ≤ (K - 1) (2 ^ (i + |B|) + 2 ^ (n - i + |A|)).
The single-cut criterion. If a single-output circuit computes a K-rectangle-free
function f, then for every set S of its wires, with i inputs in S, forward signals
A = forward c.program S and backward signals B = backward c.program S,
|f⁻¹(1)| ≤ (K - 1) (2 ^ (i + |B|) + 2 ^ (n - i + |A|)).
The single-cut criterion, strict form.
|f⁻¹(1)| < K (2 ^ (i + |B|) + 2 ^ (n - i + |A|)).
The single-cut corollary. If a single-output circuit computes a K-rectangle-free
function with at least 2 ^ (n - 2) accepted inputs, then every set S of its wires has
n ≤ max (i + |B|) (n - i + |A|) + ⌈log₂ K⌉ + 2.
The single-cut corollary, real form. Under the hypotheses of le_max_add_clog,
max (i + |B|) (n - i + |A|) > n - log₂ K - 3.
Every ordering has a heavily crossed prefix. Under the hypotheses of
le_max_add_clog, every injective ranking of the wires has a prefix, the wires ranked below
some t, crossed by at least ⌊n/2⌋ - ⌈log₂ K⌉ - 2 signals: the prefix containing exactly
⌊n/2⌋ inputs would otherwise violate the criterion.