The wiring graph of a binary circuit

Fix a program over the full binary basis and an output gate. The reachable wires are the output gate and, recursively, the argument wires of reachable gates. The wiring graph has a vertex for every reachable wire and, for a signal feeding f ≥ 2 gate slots, f - 1 copy vertices of degree three through which the signal is routed. Its edges are the slots of reachable gates and the incoming edge of every copy vertex.

Each edge carries one bit. A gate vertex checks that its outgoing edge carries the gate's function of its two slot bits, the output gate checks that this value is 1, and a copy vertex checks that all its incident edges agree. An input vertex has no check; its outgoing edge is the port of the variable.

The main results are

• network_computes: an input is accepted by the circuit exactly when some edge assignment satisfies every check and every port;
• loopless, maxDegreeLE_three, connected: the multigraph hypotheses of the graph-ordering lemma;
• card_edge_add_card_signal, card_slot, card_signal, card_copy_le: the edge and vertex counts, giving M - N = s' - n' for s' reachable gates and n' reachable inputs.

theorem Algebraic.Cutwidth.lines_wires_lt {n s : ℕ} (p : Program Binary.signature n s) (g : Fin s) (a : Fin 2) : ↑((p.lines g).wires a).index < n + ↑g

The argument wires of a widened binary line refer to earlier wires.

inductive Algebraic.Cutwidth.Wiring.Reach {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Wire n s → Prop

A wire is reachable when it is the output gate or an argument of a reachable gate.

• out {n s : ℕ} {p : Program Binary.signature n s} {out : Fin s} : Reach p out (Wire.gate out)

  The output gate is reachable.

• arg {n s : ℕ} {p : Program Binary.signature n s} {out g : Fin s} (a : Fin 2) : Reach p out (Wire.gate g) → Reach p out ((p.lines g).wires a)

  An argument of a reachable gate is reachable.

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.Signal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

The reachable wires: the signals of the wiring graph.

Equations

• Algebraic.Cutwidth.Wiring.Signal p out = { w : Cslib.Circuits.Wire n s // Algebraic.Cutwidth.Wiring.Reach p out w }

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.Slot {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

The argument slots of reachable gates.

Equations

• Algebraic.Cutwidth.Wiring.Slot p out = { t : Fin s × Fin 2 // Algebraic.Cutwidth.Wiring.Reach p out (Cslib.Circuits.Wire.gate t.1) }

@[instance_reducible]

noncomputable instance Algebraic.Cutwidth.Wiring.instFintypeSignal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype (Signal p out)

Reachability is decided classically; the graph is a proof object.

Equations

• Algebraic.Cutwidth.Wiring.instFintypeSignal p out = Subtype.fintype (Algebraic.Cutwidth.Wiring.Reach p out)

@[instance_reducible]

noncomputable instance Algebraic.Cutwidth.Wiring.instFintypeSlot {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype (Slot p out)

Equations

• Algebraic.Cutwidth.Wiring.instFintypeSlot p out = Subtype.fintype fun (t : Fin s × Fin 2) => Algebraic.Cutwidth.Wiring.Reach p out (Cslib.Circuits.Wire.gate t.1)

def Algebraic.Cutwidth.Wiring.slotSignal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : Signal p out

The signal read by a slot.

Equations

• Algebraic.Cutwidth.Wiring.slotSignal p out t = ⟨(p.lines (↑t).1).wires (↑t).2, ⋯⟩

def Algebraic.Cutwidth.Wiring.slotGate {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : Signal p out

The gate owning a slot.

Equations

• Algebraic.Cutwidth.Wiring.slotGate p out t = ⟨Cslib.Circuits.Wire.gate (↑t).1, ⋯⟩

noncomputable def Algebraic.Cutwidth.Wiring.slots {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) : Finset (Slot p out)

The slots fed by a signal.

Equations

• Algebraic.Cutwidth.Wiring.slots p out w = {t : Algebraic.Cutwidth.Wiring.Slot p out | Algebraic.Cutwidth.Wiring.slotSignal p out t = w}

theorem Algebraic.Cutwidth.Wiring.mem_slots {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {w : Signal p out} {t : Slot p out} : t ∈ slots p out w ↔ slotSignal p out t = w

noncomputable def Algebraic.Cutwidth.Wiring.fanout {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) : ℕ

The number of slots fed by a signal.

Equations

• Algebraic.Cutwidth.Wiring.fanout p out w = (Algebraic.Cutwidth.Wiring.slots p out w).card

theorem Algebraic.Cutwidth.Wiring.fanout_pos_of_slot {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : 0 < fanout p out (slotSignal p out t)

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.Copy {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

A signal feeding f ≥ 2 slots is routed through f - 1 copy vertices.

Equations

• Algebraic.Cutwidth.Wiring.Copy p out = ((w : Algebraic.Cutwidth.Wiring.Signal p out) × Fin (Algebraic.Cutwidth.Wiring.fanout p out w - 1))

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.Vertex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

Vertices: reachable wires and copy vertices.

Equations

• Algebraic.Cutwidth.Wiring.Vertex p out = (Algebraic.Cutwidth.Wiring.Signal p out ⊕ Algebraic.Cutwidth.Wiring.Copy p out)

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.Edge {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

Edges: slots of reachable gates and the incoming edges of copy vertices.

Equations

• Algebraic.Cutwidth.Wiring.Edge p out = (Algebraic.Cutwidth.Wiring.Slot p out ⊕ Algebraic.Cutwidth.Wiring.Copy p out)

noncomputable def Algebraic.Cutwidth.Wiring.slotIndex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : ℕ

The position of a slot among the slots of its signal.

Equations

• Algebraic.Cutwidth.Wiring.slotIndex p out t = ↑((Algebraic.Cutwidth.Wiring.slots p out (Algebraic.Cutwidth.Wiring.slotSignal p out t)).equivFin ⟨t, ⋯⟩)

theorem Algebraic.Cutwidth.Wiring.slotIndex_lt {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : slotIndex p out t < fanout p out (slotSignal p out t)

theorem Algebraic.Cutwidth.Wiring.slotIndex_injective {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {t t' : Slot p out} (hsignal : slotSignal p out t = slotSignal p out t') (hindex : slotIndex p out t = slotIndex p out t') : t = t'

Slots of one signal are determined by their positions.

noncomputable def Algebraic.Cutwidth.Wiring.copyIndex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : ℕ

The copy vertex at which a slot is attached, when its signal has fan-out at least two: slots in order, with the last two slots sharing the last copy.

Equations

• Algebraic.Cutwidth.Wiring.copyIndex p out t = min (Algebraic.Cutwidth.Wiring.slotIndex p out t) (Algebraic.Cutwidth.Wiring.fanout p out (Algebraic.Cutwidth.Wiring.slotSignal p out t) - 2)

theorem Algebraic.Cutwidth.Wiring.copyIndex_lt {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) (h : 2 ≤ fanout p out (slotSignal p out t)) : copyIndex p out t < fanout p out (slotSignal p out t) - 1

noncomputable def Algebraic.Cutwidth.Wiring.fst {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Edge p out → Vertex p out

The first endpoint of an edge: the signal vertex or copy vertex supplying it.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Wiring.fst p out (Sum.inr ⟨w, k⟩) = if h : ↑k = 0 then Sum.inl w else Sum.inr ⟨w, ⟨↑k - 1, ⋯⟩⟩

def Algebraic.Cutwidth.Wiring.snd {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Edge p out → Vertex p out

The second endpoint of an edge: the gate reading a slot, or the copy vertex.

Equations

• Algebraic.Cutwidth.Wiring.snd p out (Sum.inl t) = Sum.inl (Algebraic.Cutwidth.Wiring.slotGate p out t)
• Algebraic.Cutwidth.Wiring.snd p out (Sum.inr c) = Sum.inr c

def Algebraic.Cutwidth.Wiring.signal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Edge p out → Signal p out

The signal carried by an edge.

Equations

• Algebraic.Cutwidth.Wiring.signal p out (Sum.inl t) = Algebraic.Cutwidth.Wiring.slotSignal p out t
• Algebraic.Cutwidth.Wiring.signal p out (Sum.inr ⟨w, k⟩) = w

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

The first outgoing edge of a signal with positive fan-out: the incoming edge of its first copy vertex, or its unique slot.

Equations

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

theorem Algebraic.Cutwidth.Wiring.fst_inl_of_two_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) (h : 2 ≤ fanout p out (slotSignal p out t)) : fst p out (Sum.inl t) = Sum.inr ⟨slotSignal p out t, ⟨copyIndex p out t, ⋯⟩⟩

theorem Algebraic.Cutwidth.Wiring.fst_inl_of_fanout_eq_one {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) (h : fanout p out (slotSignal p out t) = 1) : fst p out (Sum.inl t) = Sum.inl (slotSignal p out t)

theorem Algebraic.Cutwidth.Wiring.fst_inr_zero {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (h : 0 < fanout p out w - 1) : fst p out (Sum.inr ⟨w, ⟨0, h⟩⟩) = Sum.inl w

theorem Algebraic.Cutwidth.Wiring.fst_inr_succ {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (k : ℕ) (h : k + 1 < fanout p out w - 1) : fst p out (Sum.inr ⟨w, ⟨k + 1, h⟩⟩) = Sum.inr ⟨w, ⟨k, ⋯⟩⟩

theorem Algebraic.Cutwidth.Wiring.snd_inl {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : snd p out (Sum.inl t) = Sum.inl (slotGate p out t)

theorem Algebraic.Cutwidth.Wiring.snd_inr {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (c : Copy p out) : snd p out (Sum.inr c) = Sum.inr c

theorem Algebraic.Cutwidth.Wiring.fanout_eq_one_of_not_two_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) (h : ¬2 ≤ fanout p out (slotSignal p out t)) : fanout p out (slotSignal p out t) = 1

theorem Algebraic.Cutwidth.Wiring.signal_eq_of_fst_eq_inl {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {e : Edge p out} {w : Signal p out} (h : fst p out e = Sum.inl w) : signal p out e = w

The first endpoint of an edge belongs to the tree of its signal.

theorem Algebraic.Cutwidth.Wiring.signal_eq_of_fst_eq_inr {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {e : Edge p out} {w : Signal p out} {k : Fin (fanout p out w - 1)} (h : fst p out e = Sum.inr ⟨w, k⟩) : signal p out e = w

theorem Algebraic.Cutwidth.Wiring.signal_firstOut {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (h : 0 < fanout p out w) : signal p out (firstOut p out w) = w

theorem Algebraic.Cutwidth.Wiring.fst_firstOut {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (h : 0 < fanout p out w) : fst p out (firstOut p out w) = Sum.inl w

theorem Algebraic.Cutwidth.Wiring.eq_firstOut_of_fst_eq_inl {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {e : Edge p out} {w : Signal p out} (h : fst p out e = Sum.inl w) : e = firstOut p out w

The only edge leaving a signal vertex is its first outgoing edge.

theorem Algebraic.Cutwidth.Wiring.input_ne_gate {n s : ℕ} (j : Fin n) (g : Fin s) : Wire.input j ≠ Wire.gate g

theorem Algebraic.Cutwidth.Wiring.fanout_pos {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (hne : ↑w ≠ Wire.gate out) : 0 < fanout p out w

Every reachable wire other than the output gate feeds a slot.

def Algebraic.Cutwidth.Wiring.opValue {n s : ℕ} (p : Program Binary.signature n s) (out g : Fin s) (h : Reach p out (Wire.gate g)) (α : Edge p out → Bool) : Bool

The value a gate's operation takes on the bits of its two slots.

Equations

• Algebraic.Cutwidth.Wiring.opValue p out g h α = (p.lines g).op (α (Sum.inl ⟨(g, 0), h⟩)) (α (Sum.inl ⟨(g, 1), h⟩))

def Algebraic.Cutwidth.Wiring.Check {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Vertex p out → (Edge p out → Bool) → Prop

The local check of a vertex. A reachable gate requires its outgoing edge, if any, to carry its operation applied to its slot bits, the output gate requires that value to be 1, and a copy vertex requires all its outgoing edges to carry the bit of its incoming edge. Input vertices have no check.

Equations

• One or more equations did not get rendered due to their size.
• Algebraic.Cutwidth.Wiring.Check p out (Sum.inr c) x✝ = ∀ (e : Algebraic.Cutwidth.Wiring.Edge p out), Algebraic.Cutwidth.Wiring.fst p out e = Sum.inr c → x✝ e = x✝ (Sum.inr c)

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

The variables read by the circuit: the reachable input wires.

Equations

• Algebraic.Cutwidth.Wiring.read p out = {j : Fin n | Algebraic.Cutwidth.Wiring.Reach p out (Cslib.Circuits.Wire.input j)}

theorem Algebraic.Cutwidth.Wiring.mem_read {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {j : Fin n} : j ∈ read p out ↔ Reach p out (Wire.input j)

noncomputable def Algebraic.Cutwidth.Wiring.portVertex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (j : Fin n) : Vertex p out

The vertex of an input variable.

Equations

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

noncomputable def Algebraic.Cutwidth.Wiring.portEdge {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (j : Fin n) : Edge p out

The edge carrying an input variable.

Equations

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

theorem Algebraic.Cutwidth.Wiring.portVertex_of_reach {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {j : Fin n} (h : Reach p out (Wire.input j)) : portVertex p out j = Sum.inl ⟨Wire.input j, h⟩

theorem Algebraic.Cutwidth.Wiring.portEdge_of_reach {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {j : Fin n} (h : Reach p out (Wire.input j)) : portEdge p out j = firstOut p out ⟨Wire.input j, h⟩

noncomputable def Algebraic.Cutwidth.Wiring.network {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Network n (Vertex p out) (Edge p out)

The wiring graph as a constraint network.

Equations

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

Semantics

theorem Algebraic.Cutwidth.Wiring.eval_eq_op {n s : ℕ} (p : Program Binary.signature n s) (x : Fin n → Bool) (g : Fin s) : p.eval Binary.interpretation x g = (p.lines g).op (p.trace Binary.interpretation x ((p.lines g).wires 0)) (p.trace Binary.interpretation x ((p.lines g).wires 1))

The value of a gate is its operation applied to the values of its argument wires.

noncomputable def Algebraic.Cutwidth.Wiring.traceAssignment {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (x : Fin n → Bool) : Edge p out → Bool

The bits carried by the edges under the circuit's own evaluation.

Equations

• Algebraic.Cutwidth.Wiring.traceAssignment p out x e = p.trace Algebraic.Binary.interpretation x ↑(Algebraic.Cutwidth.Wiring.signal p out e)

theorem Algebraic.Cutwidth.Wiring.opValue_traceAssignment {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (x : Fin n → Bool) (g : Fin s) (h : Reach p out (Wire.gate g)) : opValue p out g h (traceAssignment p out x) = p.eval Binary.interpretation x g

theorem Algebraic.Cutwidth.Wiring.traceAssignment_satisfies {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (x : Fin n → Bool) (hx : p.eval Binary.interpretation x out = true) : (network p out).Satisfies x (traceAssignment p out x)

The evaluation of an accepted input satisfies every check and every port.

theorem Algebraic.Cutwidth.Wiring.copy_eq_firstOut_of_satisfies {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {x : Fin n → Bool} {α : Edge p out → Bool} (hα : (network p out).Satisfies x α) (w : Signal p out) (m : ℕ) (hm : m < fanout p out w - 1) : α (Sum.inr ⟨w, ⟨m, hm⟩⟩) = α (firstOut p out w)

Under a satisfying assignment, the incoming edge of every copy vertex of a signal carries the bit of the signal's first outgoing edge.

theorem Algebraic.Cutwidth.Wiring.eq_firstOut_of_satisfies {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {x : Fin n → Bool} {α : Edge p out → Bool} (hα : (network p out).Satisfies x α) (w : Signal p out) (e : Edge p out) (he : signal p out e = w) : α e = α (firstOut p out w)

Under a satisfying assignment, every edge carrying a signal with positive fan-out carries the bit of the signal's first outgoing edge.

theorem Algebraic.Cutwidth.Wiring.eq_trace_of_satisfies {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {x : Fin n → Bool} {α : Edge p out → Bool} (hα : (network p out).Satisfies x α) (w : Signal p out) (e : Edge p out) : signal p out e = w → α e = p.trace Binary.interpretation x ↑w

Under a satisfying assignment, every edge carries the circuit's value of its signal.

theorem Algebraic.Cutwidth.Wiring.eval_out_eq_true_of_satisfies {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {x : Fin n → Bool} {α : Edge p out → Bool} (hα : (network p out).Satisfies x α) : p.eval Binary.interpretation x out = true

A satisfying assignment exists only for accepted inputs.

theorem Algebraic.Cutwidth.Wiring.network_computes {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : (network p out).Computes fun (x : Cslib.BitString n) => p.eval Binary.interpretation x out

The wiring network accepts exactly the inputs accepted by the circuit.

Graph properties

theorem Algebraic.Cutwidth.Wiring.loopless {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : (network p out).Loopless

No edge joins a vertex to itself.

noncomputable def Algebraic.Cutwidth.Wiring.outEdges {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (v : Vertex p out) : Finset (Edge p out)

The edges leaving a vertex.

Equations

• Algebraic.Cutwidth.Wiring.outEdges p out v = {e : Algebraic.Cutwidth.Wiring.Edge p out | Algebraic.Cutwidth.Wiring.fst p out e = v}

noncomputable def Algebraic.Cutwidth.Wiring.inEdges {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (v : Vertex p out) : Finset (Edge p out)

The edges entering a vertex.

Equations

• Algebraic.Cutwidth.Wiring.inEdges p out v = {e : Algebraic.Cutwidth.Wiring.Edge p out | Algebraic.Cutwidth.Wiring.snd p out e = v}

theorem Algebraic.Cutwidth.Wiring.mem_outEdges {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {v : Vertex p out} {e : Edge p out} : e ∈ outEdges p out v ↔ fst p out e = v

theorem Algebraic.Cutwidth.Wiring.mem_inEdges {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {v : Vertex p out} {e : Edge p out} : e ∈ inEdges p out v ↔ snd p out e = v

theorem Algebraic.Cutwidth.Wiring.edgesAt_subset {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (v : Vertex p out) : (network p out).edgesAt v ⊆ outEdges p out v ∪ inEdges p out v

theorem Algebraic.Cutwidth.Wiring.gate_injective {n s : ℕ} {g g' : Fin s} (h : Wire.gate g = Wire.gate g') : g = g'

theorem Algebraic.Cutwidth.Wiring.card_inEdges_inl_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) : (inEdges p out (Sum.inl w)).card ≤ 2

A signal vertex receives at most two edges: the slots of its gate.

theorem Algebraic.Cutwidth.Wiring.card_outEdges_inl_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) : (outEdges p out (Sum.inl w)).card ≤ 1

At most one edge leaves a signal vertex: its first outgoing edge.

theorem Algebraic.Cutwidth.Wiring.card_inEdges_inr_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (c : Copy p out) : (inEdges p out (Sum.inr c)).card ≤ 1

Exactly one edge enters a copy vertex.

theorem Algebraic.Cutwidth.Wiring.copyIndex_le_slotIndex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (t : Slot p out) : copyIndex p out t ≤ slotIndex p out t

A slot attached to a copy vertex has its position at least the copy's.

theorem Algebraic.Cutwidth.Wiring.card_outEdges_inr_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (k : Fin (fanout p out w - 1)) : (outEdges p out (Sum.inr ⟨w, k⟩)).card ≤ 2

At most two edges leave a copy vertex: the next copy edge and its slots.

theorem Algebraic.Cutwidth.Wiring.maxDegreeLE_three {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : (network p out).MaxDegreeLE 3

Every vertex has at most three incident edges.

def Algebraic.Cutwidth.Wiring.root {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Vertex p out

The output gate's vertex.

Equations

• Algebraic.Cutwidth.Wiring.root p out = Sum.inl ⟨Cslib.Circuits.Wire.gate out, ⋯⟩

theorem Algebraic.Cutwidth.Wiring.adj_of_edge {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (e : Edge p out) : (network p out).Adj (fst p out e) (snd p out e)

theorem Algebraic.Cutwidth.Wiring.copy_reaches_signal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Signal p out) (m : ℕ) (hm : m < fanout p out w - 1) : Relation.ReflTransGen (network p out).Adj (Sum.inr ⟨w, ⟨m, hm⟩⟩) (Sum.inl w)

Every copy vertex is joined to its signal vertex along the copy chain.

theorem Algebraic.Cutwidth.Wiring.signal_reaches_root {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) (w : Wire n s) (h : Reach p out w) : Relation.ReflTransGen (network p out).Adj (Sum.inl ⟨w, h⟩) (root p out)

Every reachable wire is joined to the output gate.

theorem Algebraic.Cutwidth.Wiring.connected {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : (network p out).Connected

The wiring graph is connected.

instance Algebraic.Cutwidth.Wiring.instNonemptyVertex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Nonempty (Vertex p out)

Counting vertices and edges

@[reducible, inline]

abbrev Algebraic.Cutwidth.Wiring.ReachableGate {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Type

The reachable gates.

Equations

• Algebraic.Cutwidth.Wiring.ReachableGate p out = { g : Fin s // Algebraic.Cutwidth.Wiring.Reach p out (Cslib.Circuits.Wire.gate g) }

theorem Algebraic.Cutwidth.Wiring.card_edge_add_card_signal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (Edge p out) + Fintype.card (Signal p out) = Fintype.card (Vertex p out) + Fintype.card (Slot p out)

Edges plus signals equal vertices plus slots: both sides count every copy once.

theorem Algebraic.Cutwidth.Wiring.card_slot {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (Slot p out) = 2 * Fintype.card (ReachableGate p out)

Every reachable gate has two slots.

theorem Algebraic.Cutwidth.Wiring.card_signal {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (Signal p out) = (read p out).card + Fintype.card (ReachableGate p out)

The signals are the reachable inputs and the reachable gates.

theorem Algebraic.Cutwidth.Wiring.card_copy_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (Copy p out) ≤ Fintype.card (Slot p out)

There are fewer copy vertices than slots.

theorem Algebraic.Cutwidth.Wiring.card_reachableGate_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (ReachableGate p out) ≤ s

theorem Algebraic.Cutwidth.Wiring.card_read_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : (read p out).card ≤ n

theorem Algebraic.Cutwidth.Wiring.card_vertex_le {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : Fintype.card (Vertex p out) ≤ n + 3 * s

The vertex count is at most n + 3 s.

theorem Algebraic.Cutwidth.Wiring.card_edge_sub_card_vertex {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) : ↑(Fintype.card (Edge p out)) - ↑(Fintype.card (Vertex p out)) = ↑(Fintype.card (ReachableGate p out)) - ↑(read p out).card

Edges minus vertices is reachable gates minus reachable inputs, as reals.