Proofs for the ordering transfer

The components of the wire graph are closed sets of wires (component_closed), and a closed set contributes no crossing signals to a split (forward_union_of_closed, backward_union_of_closed). The ranking of the wires lists the components one after another, ordered by their first wire, and inside each component follows the vertex order that the graph-ordering bound gives its wire graph (WireGraph). A prefix up to a wire w is then the union of whole earlier components, which are closed, and of the wires of the component of w whose vertices lie in a lower set of that order. Its crossing signals are therefore bounded by a lower-set cut of one connected wire graph (exists_rank).

Components of the wire graph

theorem Algebraic.Cutwidth.MultiOutput.Internal.linked_symm {σ : Signature} {n s : ℕ} {p : Program σ n s} {u v : Wire n s} (h : Linked p u v) : Linked p v u

theorem Algebraic.Cutwidth.MultiOutput.Internal.reflTransGen_linked_symm {σ : Signature} {n s : ℕ} {p : Program σ n s} {u v : Wire n s} (h : Relation.ReflTransGen (Linked p) u v) : Relation.ReflTransGen (Linked p) v u

theorem Algebraic.Cutwidth.MultiOutput.Internal.linked_of_reads {σ : Signature} {n s : ℕ} {p : Program σ n s} {g : Fin s} {w : Wire n s} (h : p.Reads g w) : Linked p (Wire.gate g) w

theorem Algebraic.Cutwidth.MultiOutput.Internal.mem_component {σ : Signature} {n s : ℕ} {p : Program σ n s} {v w : Wire n s} : v ∈ component p w ↔ Relation.ReflTransGen (Linked p) w v

theorem Algebraic.Cutwidth.MultiOutput.Internal.mem_component_self {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) : w ∈ component p w

theorem Algebraic.Cutwidth.MultiOutput.Internal.component_closed {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) (g : Fin s) (v : Wire n s) (h : p.Reads g v) : Wire.gate g ∈ component p w ↔ v ∈ component p w

A component is closed: a gate lies in it exactly when the wires it reads do.

theorem Algebraic.Cutwidth.MultiOutput.Internal.component_eq_of_mem {σ : Signature} {n s : ℕ} {p : Program σ n s} {v w : Wire n s} (h : v ∈ component p w) : component p v = component p w

theorem Algebraic.Cutwidth.MultiOutput.Internal.component_connected {σ : Signature} {n s : ℕ} (p : Program σ n s) (w u : Wire n s) : u ∈ component p w → ∀ v ∈ component p w, Relation.ReflTransGen (Linked p) u v

Any two wires of a component are joined by a path of linked wires.

theorem Algebraic.Cutwidth.MultiOutput.Internal.component_eq_of_reads {σ : Signature} {n s : ℕ} {p : Program σ n s} {g : Fin s} {v : Wire n s} (h : p.Reads g v) : component p (Wire.gate g) = component p v

A gate and a wire it reads have the same component.

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.componentSet {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) : ClosedSet p

The component of a wire, as a closed set.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.componentSet p w = { carrier := Algebraic.Cutwidth.MultiOutput.component p w, closed := ⋯ }

theorem Algebraic.Cutwidth.MultiOutput.Internal.componentSet_eq {σ : Signature} {n s : ℕ} {p : Program σ n s} {v w : Wire n s} (h : component p v = component p w) : componentSet p v = componentSet p w

Closed sets contribute no crossing signals

theorem Algebraic.Cutwidth.MultiOutput.Internal.forward_union_of_closed {σ : Signature} {n s : ℕ} {p : Program σ n s} {Q P : Finset (Wire n s)} (hQ : ∀ (g : Fin s) (w : Wire n s), p.Reads g w → (Wire.gate g ∈ Q ↔ w ∈ Q)) (hdisj : Disjoint Q P) : SingleCut.forward p (Q ∪ P) = SingleCut.forward p P

Adding a closed set disjoint from P does not change the forward signals of P.

theorem Algebraic.Cutwidth.MultiOutput.Internal.backward_union_of_closed {σ : Signature} {n s : ℕ} {p : Program σ n s} {Q P : Finset (Wire n s)} (hQ : ∀ (g : Fin s) (w : Wire n s), p.Reads g w → (Wire.gate g ∈ Q ↔ w ∈ Q)) (hdisj : Disjoint Q P) : SingleCut.backward p (Q ∪ P) = SingleCut.backward p P

Adding a closed set disjoint from P does not change the backward signals of P.

theorem Algebraic.Cutwidth.MultiOutput.Internal.forward_eq_empty_of_closed {σ : Signature} {n s : ℕ} {p : Program σ n s} {Q : Finset (Wire n s)} (hQ : ∀ (g : Fin s) (w : Wire n s), p.Reads g w → (Wire.gate g ∈ Q ↔ w ∈ Q)) : SingleCut.forward p Q = ∅

A closed set has no forward signals.

theorem Algebraic.Cutwidth.MultiOutput.Internal.backward_eq_empty_of_closed {σ : Signature} {n s : ℕ} {p : Program σ n s} {Q : Finset (Wire n s)} (hQ : ∀ (g : Fin s) (w : Wire n s), p.Reads g w → (Wire.gate g ∈ Q ↔ w ∈ Q)) : SingleCut.backward p Q = ∅

A closed set has no backward signals.

Ranking by an injective key

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_lt_le_card_lt_iff {α : Type u_1} {β : Type u_2} [Fintype α] [LinearOrder β] (f : α → β) (a b : α) : {x : α | f x < f a}.card ≤ {x : α | f x < f b}.card ↔ f a ≤ f b

In a finite set ranked by an injective key, the number of elements with a smaller key compares like the keys.

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_lt_lt_card {α : Type u_1} {β : Type u_2} [Fintype α] [LinearOrder β] (f : α → β) (a : α) : {x : α | f x < f a}.card < Fintype.card α

The ranking of the wires

theorem Algebraic.Cutwidth.MultiOutput.Internal.index_injective {n s : ℕ} : Function.Injective fun (w : Wire n s) => w.index

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.componentId {σ : Signature} {n s : ℕ} (p : Program σ n s) (w : Wire n s) : WithTop ℕ

The least index of a wire of the component of w; it identifies the component.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.componentId p w = (Finset.image (fun (v : Cslib.Circuits.Wire n s) => ↑v.index) (Algebraic.Cutwidth.MultiOutput.component p w)).min

theorem Algebraic.Cutwidth.MultiOutput.Internal.componentId_congr {σ : Signature} {n s : ℕ} {p : Program σ n s} {v w : Wire n s} (h : component p v = component p w) : componentId p v = componentId p w

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_componentId_eq {σ : Signature} {n s : ℕ} {p : Program σ n s} (w : Wire n s) : ∃ v ∈ component p w, componentId p w = ↑↑v.index

theorem Algebraic.Cutwidth.MultiOutput.Internal.component_eq_of_componentId_eq {σ : Signature} {n s : ℕ} {p : Program σ n s} {v w : Wire n s} (h : componentId p v = componentId p w) : component p v = component p w

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.posIn {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (K : ClosedSet p) (w : Wire n s) : ℕ

The position of a wire of K in the order chosen on the wire graph of K.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.posIn ord K w = if h : w ∈ K.carrier then {x : Algebraic.Cutwidth.MultiOutput.Internal.WireGraph.Vertex K | x < Sum.inl ⟨w, h⟩}.card else 0

theorem Algebraic.Cutwidth.MultiOutput.Internal.posIn_le_posIn_iff {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (K : ClosedSet p) {u v : Wire n s} (hu : u ∈ K.carrier) (hv : v ∈ K.carrier) : posIn ord K u ≤ posIn ord K v ↔ Sum.inl ⟨u, hu⟩ ≤ Sum.inl ⟨v, hv⟩

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.pos {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : ℕ

The position of a wire in the order chosen on its component.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.pos ord w = Algebraic.Cutwidth.MultiOutput.Internal.posIn ord (Algebraic.Cutwidth.MultiOutput.Internal.componentSet p w) w

theorem Algebraic.Cutwidth.MultiOutput.Internal.pos_eq_posIn {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) {v w : Wire n s} (h : v ∈ component p w) : pos ord v = posIn ord (componentSet p w) v

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.key {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : Lex (WithTop ℕ × ℕ)

The ranking key: the component's identifier, then the position inside the component.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.key ord w = toLex (Algebraic.Cutwidth.MultiOutput.Internal.componentId p w, Algebraic.Cutwidth.MultiOutput.Internal.pos ord w)

theorem Algebraic.Cutwidth.MultiOutput.Internal.key_le_key_iff {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (v w : Wire n s) : key ord v ≤ key ord w ↔ componentId p v < componentId p w ∨ ∃ (hv : v ∈ component p w), Sum.inl ⟨v, hv⟩ ≤ Sum.inl ⟨w, ⋯⟩

theorem Algebraic.Cutwidth.MultiOutput.Internal.key_injective {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) : Function.Injective (key ord)

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.rank {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : ℕ

The rank of a wire: the number of wires with a smaller key.

Equations

• Algebraic.Cutwidth.MultiOutput.Internal.rank ord w = {v : Cslib.Circuits.Wire n s | Algebraic.Cutwidth.MultiOutput.Internal.key ord v < Algebraic.Cutwidth.MultiOutput.Internal.key ord w}.card

theorem Algebraic.Cutwidth.MultiOutput.Internal.rank_le_rank_iff {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (v w : Wire n s) : rank ord v ≤ rank ord w ↔ key ord v ≤ key ord w

theorem Algebraic.Cutwidth.MultiOutput.Internal.rank_injective {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) : Function.Injective (rank ord)

theorem Algebraic.Cutwidth.MultiOutput.Internal.rank_lt {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : rank ord w < n + s

noncomputable def Algebraic.Cutwidth.MultiOutput.Internal.lowerUpTo {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : Finset (WireGraph.Vertex (componentSet p w))

The vertices of the wire graph of the component of w up to the vertex of w.

Equations

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

theorem Algebraic.Cutwidth.MultiOutput.Internal.isLowerSet_lowerUpTo {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : IsLowerSet ↑(lowerUpTo ord w)

theorem Algebraic.Cutwidth.MultiOutput.Internal.prefixUpTo_rank_eq {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : prefixUpTo (rank ord) w = {v : Wire n s | componentId p v < componentId p w} ∪ WireGraph.wiresIn (componentSet p w) (lowerUpTo ord w)

The prefix decomposition. The prefix up to w is the union of the wires of earlier components and of the wires of the component of w whose vertices lie up to that of w.

theorem Algebraic.Cutwidth.MultiOutput.Internal.earlier_closed {σ : Signature} {n s : ℕ} {p : Program σ n s} (w : Wire n s) (g : Fin s) (v : Wire n s) : p.Reads g v → (Wire.gate g ∈ {u : Wire n s | componentId p u < componentId p w} ↔ v ∈ {u : Wire n s | componentId p u < componentId p w})

The earlier components form a closed set.

theorem Algebraic.Cutwidth.MultiOutput.Internal.earlier_disjoint {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : Disjoint {u : Wire n s | componentId p u < componentId p w} (WireGraph.wiresIn (componentSet p w) (lowerUpTo ord w))

theorem Algebraic.Cutwidth.MultiOutput.Internal.card_crossing_le_cut {σ : Signature} {n s : ℕ} {p : Program σ n s} (ord : (K : ClosedSet p) → LinearOrder (WireGraph.Vertex K)) (w : Wire n s) : (SingleCut.forward p (prefixUpTo (rank ord) w)).card + (SingleCut.backward p (prefixUpTo (rank ord) w)).card ≤ ((WireGraph.graph (componentSet p w)).cut (lowerUpTo ord w)).card

Prefix crossings are lower-set cuts of one component.

The ordering transfer

theorem Algebraic.Cutwidth.MultiOutput.Internal.orderingBound_nonneg {A η C : ℝ} (order : Multigraph.OrderingBound A η C) : 0 ≤ C

The ordering hypothesis forces a nonnegative additive constant: the empty lower set of the one-vertex graph has an empty cut.

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_rank {σ : Signature} {n s : ℕ} {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (p : Program σ n s) (hp : p.FanInAtMost 2) : ∃ (rank : Wire n s → ℕ), Function.Injective rank ∧ (∀ (w : Wire n s), rank w < n + s) ∧ ∀ (w : Wire n s), ↑((SingleCut.forward p (prefixUpTo rank w)).card + (SingleCut.backward p (prefixUpTo rank w)).card) ≤ (A + η) * max (↑(gatesIn (component p w)).card - ↑(SingleCut.inputsIn (component p w)).card) 0 + 3 * Real.logb 2 (↑n + 3 * ↑s) + C

The ordering transfer.

theorem Algebraic.Cutwidth.MultiOutput.Internal.exists_rank_of_connected {σ : Signature} {n s : ℕ} {A η C : ℝ} (hAη : 0 ≤ A + η) (order : Multigraph.OrderingBound A η C) (p : Program σ n s) (hp : p.FanInAtMost 2) (hconn : ∀ (u v : Wire n s), Relation.ReflTransGen (Linked p) u v) : ∃ (rank : Wire n s → ℕ), Function.Injective rank ∧ (∀ (w : Wire n s), rank w < n + s) ∧ ∀ (t : ℕ), ↑((SingleCut.forward p (prefixBelow rank t)).card + (SingleCut.backward p (prefixBelow rank t)).card) ≤ (A + η) * max (↑s - ↑n) 0 + 3 * Real.logb 2 (↑n + 3 * ↑s) + C

The ordering transfer for a connected wire graph.