Direction in the wiring graph

The wiring graph is undirected for the layout lemma, but every edge runs from the vertex producing its signal (fst) to the vertex consuming it (snd). Relative to a vertex set L, an edge is backward-crossing when it is produced outside L and consumed inside, and forward-crossing in the opposite case.

The determination lemma trace_eq_of_agree_backward says that the values of all signals with an edge touching L are determined by the inputs read in L together with the bits on the backward-crossing edges: two evaluations that agree on those agree on every such signal. Applied to the complement of L, the inputs read outside L and the forward-crossing bits determine every signal with an edge touching the outside. These are the two facts the average-case bound needs beyond the cut-counting lemma.

theorem Algebraic.Cutwidth.Wiring.copy_not_mem_of_no_backward {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {L : Finset (Vertex p out)} {w : Signal p out} (hA : ∀ (e : Edge p out), signal p out e = w → fst p out e ∉ L → snd p out e ∈ L → False) (hw : Sum.inl w ∉ L) (k : ℕ) (hk : k < fanout p out w - 1) : Sum.inr ⟨w, ⟨k, hk⟩⟩ ∉ L

If no edge of a signal is backward-crossing and its signal vertex lies outside L, then none of its copy vertices lies in L.

theorem Algebraic.Cutwidth.Wiring.trace_eq_of_agree_backward {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {L : Finset (Vertex p out)} {x x' : Fin n → Bool} (hpast : ∀ j ∈ (network p out).past L, x j = x' j) (hback : ∀ (e : Edge p out), fst p out e ∉ L → snd p out e ∈ L → traceAssignment p out x e = traceAssignment p out x' e) (w : Signal p out) (e : Edge p out) : signal p out e = w → fst p out e ∈ L ∨ snd p out e ∈ L → p.trace Binary.interpretation x ↑w = p.trace Binary.interpretation x' ↑w

Determination. Two evaluations agreeing on the inputs read in L and on the backward-crossing edges of L agree on every signal with an edge touching L.

theorem Algebraic.Cutwidth.Wiring.mem_past_compl {n s : ℕ} (p : Program Binary.signature n s) (out : Fin s) {L : Finset (Vertex p out)} {j : Fin n} : j ∈ (network p out).past Lᶜ ↔ j ∈ (network p out).read ∧ j ∉ (network p out).past L

The past of the complement of L consists of the read variables outside the past of L.