Signals and generators of a cut

The cut-counting lemma Network.card_accepting_le_of_realized charges a prefix cut by the number of bit patterns that satisfying assignments realize on it, not by its number of edges. In the wiring network of a binary circuit every edge carrying one signal carries the same bit (eq_firstOut_of_satisfies), and a gate whose two argument signals are both carried by a set of edges C carries a function of their bits. The patterns realized on C are therefore determined by one edge per generator: a signal carried by C that is not a reachable gate both of whose argument signals are carried by C.

The main results are

• determines_of_generators: a subset of C containing an edge of every generator determines C;
• card_realized_le_two_pow_generators: at most 2 ^ |generators C| patterns are realized on C, hence at most 2 ^ |signals C|;
• card_accepting_le_of_generators: the cut-counting lemma for circuits, with every prefix cut charged by its generators instead of its edges.

A layout theorem bounding the generators of every prefix cut of some vertex ordering is the target statement for signal (hypergraph) layouts; none is proved here, and FourN continues to charge edges.

noncomputable def Algebraic.Cutwidth.Wiring.signals {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : Finset (Signal p out)

The signals carried by a set of edges.

Equations

• Algebraic.Cutwidth.Wiring.signals p out C = Finset.image (Algebraic.Cutwidth.Wiring.signal p out) C

theorem Algebraic.Cutwidth.Wiring.mem_signals {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {C : Finset (Edge p out)} {w : Signal p out} : w ∈ signals p out C ↔ ∃ e ∈ C, signal p out e = w

theorem Algebraic.Cutwidth.Wiring.card_signals_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : (signals p out C).card ≤ C.card

def Algebraic.Cutwidth.Wiring.DeterminedIn {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) (w : Signal p out) : Prop

A signal is determined within C when it is a reachable gate both of whose argument signals are carried by C.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algebraic.Cutwidth.Wiring.generators {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : Finset (Signal p out)

The generators of C: the signals carried by C that are not determined within C.

Equations

• Algebraic.Cutwidth.Wiring.generators p out C = {w ∈ Algebraic.Cutwidth.Wiring.signals p out C | ¬Algebraic.Cutwidth.Wiring.DeterminedIn p out C w}

theorem Algebraic.Cutwidth.Wiring.mem_generators {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {C : Finset (Edge p out)} {w : Signal p out} : w ∈ generators p out C ↔ w ∈ signals p out C ∧ ¬DeterminedIn p out C w

theorem Algebraic.Cutwidth.Wiring.generators_subset {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : generators p out C ⊆ signals p out C

theorem Algebraic.Cutwidth.Wiring.card_generators_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : (generators p out C).card ≤ C.card

theorem Algebraic.Cutwidth.Wiring.fanout_signal_pos {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (e : Edge p out) : 0 < fanout p out (signal p out e)

Every edge carries a signal with positive fan-out.

theorem Algebraic.Cutwidth.Wiring.determines_of_generators {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {C T : Finset (Edge p out)} (hgen : ∀ w ∈ generators p out C, ∃ e ∈ T, signal p out e = w) : (network p out).Determines C T

Two satisfying assignments that agree on an edge of every generator of C agree on all of C: along the program order, a determined gate carries its operation applied to bits that already agree.

theorem Algebraic.Cutwidth.Wiring.exists_determining {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : ∃ T ⊆ C, T.card = (generators p out C).card ∧ (network p out).Determines C T

One edge of C per generator is a determining subset with exactly as many edges as generators.

theorem Algebraic.Cutwidth.Wiring.card_realized_le_two_pow_generators {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : ((network p out).realized C).card ≤ 2 ^ (generators p out C).card

The patterns realized on C are bounded by its generators.

theorem Algebraic.Cutwidth.Wiring.card_realized_le_two_pow_signals {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (C : Finset (Edge p out)) : ((network p out).realized C).card ≤ 2 ^ (signals p out C).card

The patterns realized on C are bounded by its signals.

theorem Algebraic.Cutwidth.Wiring.card_accepting_le_of_generators {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) [LinearOrder (Vertex p out)] {w : ℕ} (hw : ∀ (v : Vertex p out), (generators p out ((network p out).charged v)).card ≤ w) {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 - (read p out).card) ∨ (accepting fun (x : Cslib.BitString n) => p.eval Binary.interpretation x out).card ≤ Fintype.card (Vertex p out) * 2 ^ w * (K - 1) ^ 2

The cut-counting lemma for circuits, charged by generators. For a vertex ordering of the wiring network in which the cut before every vertex, together with that vertex's edges, has at most w generators, a circuit computing a K-rectangle-free function either accepts fewer than K · 2 ^ (n - n') inputs, where n' inputs are read, or accepts at most |V| · 2 ^ w · (K - 1) ^ 2 inputs.