Proofs for ε-halvers #
Let N be a comparator network on n wires with s comparators.
- The wire graph. Number the vertices by time: input terminals
0, the ends of comparatorcbyc + 1, and output terminals bys + 1(rank). Every wire segment leaveslastStop w t, of rank at mostt, and enters a vertex of rankt + 1on the same wire, so the graph is loopless. Two wire segments leaving the same vertex lie on the same wire, and if one entered a comparator before the other, the later one would leave a vertex of larger rank. So at most one wire segment leaves each vertex, at most one enters it, and at most one link meets it: the maximum degree is three. There are2 n + 2 svertices andn + 3 sedges. - Token conservation (
sub_le_card_cut). On inputx ∈ {0, 1}ⁿ, a wire segment carries the value of its wire, and the link of a comparator carries1when itsminWireinput is1and itsmaxWireinput is0: the one that moves. For a vertex setL, the potential at timetis the number of wires carrying1whose last vertex beforetlies inL. Comparatortchanges it by minus the net flow out ofLalong its two incoming segments and its link, so summing over all edges, the net flow out ofLis the number of ones at input terminals inLminus the number at output terminals inL. Every edge leavingLcarries at most one token and every edge entering it at least none, so for any two inputsxandx'the cut ofLhas at leastnet x - net x'edges. - Connectivity (
wireGraph_connected). Every vertex is joined to the input terminal of its wire, and the link of a comparator joins its two wires. If a set of wires closed under the comparators held0 < k ≤ n/2wires, the indicator input of the set, and of its complement, would be fixed by the network, and anε-halver withε < 1/2would put at mostε kof its wires in each half. - The cut lemma (
exists_le_card_cut). In a linear order of the vertices take the lower setLwith exactlyh = ⌊n/2⌋input terminals, and letτtop output terminals lie inL. With ones on the inputs inL, at mostε hones end in the bottom half, sonet ≥ h - τ - ε h; with zeros on the inputs inL, at mostε hzeros end in the top half, sonet ≤ ε h - τ. So the cut ofLhas at least(1 - 2 ε) hedges.
Evaluation #
A comparator whose two wires carry the same value changes nothing.
An input on which every comparator sees two equal values is fixed by the network.
Comparators commute with monotone maps.
The network commutes with monotone maps.
Stops along a wire #
The comparators before time t acting on wire w.
Equations
Instances For
The time of a vertex: 0 for input terminals, c + 1 for the ends of comparator c, and
s + 1 for output terminals.
Equations
Instances For
The wire of a vertex.
Equations
Instances For
The two sides of a comparator lie on distinct wires.
The wire graph #
The wire graph has no loops.
The wire of a wire segment.
Equations
Instances For
The time at which a wire segment ends.
Equations
Instances For
A wire segment, as opposed to a link.
Equations
Instances For
A wire segment ending at time t < s enters a comparator acting on its wire.
Two wire segments ending at the same time on the same wire are equal.
The wire graph has maximum degree three.
Counting vertices and edges #
Token conservation #
1 on vertices in L and 0 elsewhere.
Instances For
The tokens carried by an edge on input x: the value of its wire for a wire segment, and for
the link of a comparator 1 exactly when its minWire input is 1 and its maxWire input 0.
Equations
- Algebraic.Cutwidth.Halver.Internal.flow N x (Algebraic.Cutwidth.WireEdge.last w) = ↑(N.eval x w).toNat
- Algebraic.Cutwidth.Halver.Internal.flow N x (Algebraic.Cutwidth.WireEdge.into c b) = ↑(N.state x (↑c) (N.sideWire c b)).toNat
- Algebraic.Cutwidth.Halver.Internal.flow N x (Algebraic.Cutwidth.WireEdge.link c) = ↑(N.state x (↑c) (N.minWire c) && !N.state x (↑c) (N.maxWire c)).toNat
Instances For
The net flow out of L along the edge e.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The number of wires carrying 1 at time t whose last vertex before time t lies in L.
Equations
- Algebraic.Cutwidth.Halver.Internal.potential N x L t = ∑ w : Fin n, Algebraic.Cutwidth.Halver.Internal.ind L (N.lastStop w t) * ↑(N.state x t w).toNat
Instances For
Conservation at a comparator. Comparator c lowers the potential by the net flow out of
L along its two incoming segments and its link.
Token conservation. The net flow out of L is the number of ones at input terminals in
L minus the number at output terminals in L.
One edge carries a net flow of at most one token across L, in either direction.
The cut bound of token conservation. For any two inputs x and x' and any vertex set
L, the cut of L has at least net x - net x' edges, where net y is the number of ones of
y at input terminals in L minus the number of ones of N.eval y at output terminals in
L.
Connectivity #
Every vertex is joined to the input terminal of its wire.
The link of a comparator joins its two wires.
Small closed sets of wires are empty. If N is an ε-halver with ε < 1/2 and a set
S of at most n/2 wires is closed under the comparators, it is empty: the indicator input of
S and that of its complement are fixed by the network, and they would put at most ε |S| of
the wires of S in each half.
Lemma 8: closed sets of wires are trivial. If N is an ε-halver with ε < 1/2, every
set of wires closed under the comparators is empty or all wires.
The wire graph of an ε-halver with ε < 1/2 is connected.
The edge baseline. An ε-halver with ε < 1/2 on n wires has at least n - 1
comparators: its wire graph is connected.
The cut lemma and the bounds #
The cut lemma for halvers. Every linear order of the vertices of the wire graph of an
ε-halver has a lower set whose cut has at least (1 - 2 ε) ⌊n/2⌋ edges.
The finite bound. Under the graph-ordering hypothesis OrderingBound A η C, an
ε-halver with ε < 1/2 on n wires with s comparators satisfies
(1 - 2 ε) ⌊n/2⌋ ≤ (A + η) (s - n)⁺ + 3 log₂ (2 n + 2 s) + C.