One-way-liveness proof: Wiring

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Wiring.lean

Module and namespace names, imports, and formatting are adapted to complexitylib. The machine definitions are shared through Models.FiniteAutomaton.Defs.

structure Complexity.FiniteAutomaton.Pairing (P : Type u_1) : Type u_1

A perfect matching of ports, represented by a symmetric fixed-point-free relation.

• link : P → P → Prop

  The symmetric relation pairing the ports.

• symm {x y : P} : self.link x y → self.link y x
• irrefl (x : P) : ¬self.link x x
• unique (x : P) : ∃! y : P, self.link x y

theorem Complexity.FiniteAutomaton.Pairing.ext_iff {P : Type u_1} {x y : Pairing P} : x = y ↔ x.link = y.link

theorem Complexity.FiniteAutomaton.Pairing.ext {P : Type u_1} {x y : Pairing P} (link : x.link = y.link) : x = y

noncomputable def Complexity.FiniteAutomaton.Pairing.mate {P : Type u_1} (a : Pairing P) (x : P) : P

The unique port paired with the given port.

Equations

• a.mate x = Exists.choose ⋯

theorem Complexity.FiniteAutomaton.Pairing.mate_link {P : Type u_1} (a : Pairing P) (x : P) : a.link x (a.mate x)

theorem Complexity.FiniteAutomaton.Pairing.eq_mate {P : Type u_1} (a : Pairing P) {x y : P} (h : a.link x y) : y = a.mate x

theorem Complexity.FiniteAutomaton.Pairing.mate_involutive {P : Type u_1} (a : Pairing P) : Function.Involutive a.mate

theorem Complexity.FiniteAutomaton.Pairing.mate_ne {P : Type u_1} (a : Pairing P) (x : P) : a.mate x ≠ x

theorem Complexity.FiniteAutomaton.Pairing.link_iff {P : Type u_1} (a : Pairing P) (x y : P) : a.link x y ↔ a.mate x = y

instance Complexity.FiniteAutomaton.Pairing.instFinite {P : Type u_1} [Finite P] : Finite (Pairing P)

def Complexity.FiniteAutomaton.Pairing.Compatible {P : Type u_1} (a : Pairing P) {C : Type u_2} (color : P → C) : Prop

An assignment obeys all wire equalities.

Equations

• a.Compatible color = ∀ (x y : P), a.link x y → color x = color y

def Complexity.FiniteAutomaton.Pairing.connected {P : Type u_1} (a : Pairing P) (x y : P) : Prop

The equivalence relation whose classes are the pairs.

Equations

• a.connected x y = (x = y ∨ a.link x y)

theorem Complexity.FiniteAutomaton.Pairing.connected_refl {P : Type u_1} (a : Pairing P) (x : P) : a.connected x x

theorem Complexity.FiniteAutomaton.Pairing.connected_symm {P : Type u_1} (a : Pairing P) {x y : P} (h : a.connected x y) : a.connected y x

theorem Complexity.FiniteAutomaton.Pairing.connected_trans {P : Type u_1} (a : Pairing P) {x y z : P} (h : a.connected x y) (k : a.connected y z) : a.connected x z

noncomputable def Complexity.FiniteAutomaton.Pairing.testColor {P : Type u_1} (a : Pairing P) (x y : P) : Bool

The Boolean indicator of the pairing component containing a chosen port.

Equations

• a.testColor x y = decide (a.connected x y)

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.testColor_self {P : Type u_1} (a : Pairing P) (x : P) : a.testColor x x = true

theorem Complexity.FiniteAutomaton.Pairing.compatible_testColor {P : Type u_1} (a : Pairing P) (x : P) : a.Compatible (a.testColor x)

theorem Complexity.FiniteAutomaton.Pairing.eq_of_compatible {P : Type u_1} (a : Pairing P) {b : Pairing P} (h : ∀ (c : P → Bool), a.Compatible c ↔ b.Compatible c) : a = b

Two-color constraints remember an entire matching, not just rank or connectivity among one side of its ports.

theorem Complexity.FiniteAutomaton.FiniteWiring.leaves_card_le_two {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hd : ∀ (v : V), G.degree v ≤ 2) : {v : V | G.degree v = 1}.card ≤ 2

A finite connected graph with degrees at most two has at most two leaves. The proof uses the degree-sum formula and the edge-count bound for a connected graph.

theorem Complexity.FiniteAutomaton.FiniteWiring.unique_other_leaf {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hc : G.Connected) (hd : ∀ (v : V), G.degree v ≤ 2) (x : V) (hx : G.degree x = 1) : ∃! y : V, y ≠ x ∧ G.degree y = 1

In a finite connected graph of maximum degree two, a leaf has exactly one other leaf.

theorem Complexity.FiniteAutomaton.FiniteWiring.component_degree {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (C : G.ConnectedComponent) [Fintype ↥C] [DecidableRel C.toSimpleGraph.Adj] (v : ↥C) : C.toSimpleGraph.degree v = G.degree ↑v

Passing to a connected component preserves every vertex degree.

theorem Complexity.FiniteAutomaton.FiniteWiring.unique_reachable_leaf {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] (hd : ∀ (v : V), G.degree v ≤ 2) (x : V) (hx : G.degree x = 1) : ∃! y : V, y ≠ x ∧ G.degree y = 1 ∧ G.Reachable x y

Maximum degree two makes the reachable boundary pairing unique, even when other connected components are cycles.

noncomputable def Complexity.FiniteAutomaton.FiniteWiring.boundaryPairing {V : Type u_1} [Fintype V] (G : SimpleGraph V) {P : Type u_2} (port : P ↪ V) [DecidableRel G.Adj] (hd : ∀ (v : V), G.degree v ≤ 2) (hb : ∀ (v : V), G.degree v = 1 ↔ ∃ (p : P), port p = v) : Pairing P

Contract all path components onto their boundary. The degree assumptions are precisely degree one at the exposed ports and degree zero or two elsewhere. Closed components disappear.

Equations

• Complexity.FiniteAutomaton.FiniteWiring.boundaryPairing G port hd hb = { link := fun (x y : P) => x ≠ y ∧ G.Reachable (port x) (port y), symm := ⋯, irrefl := ⋯, unique := ⋯ }

theorem Complexity.FiniteAutomaton.FiniteWiring.color_eq_of_reachable {V : Type u_1} (G : SimpleGraph V) {C : Type u_2} (color : V → C) (hc : ∀ (x y : V), G.Adj x y → color x = color y) {x y : V} (h : G.Reachable x y) : color x = color y

Edge-compatible colors are constant along any finite path.

theorem Complexity.FiniteAutomaton.FiniteWiring.coloring_extension {V : Type u_1} [Fintype V] (G : SimpleGraph V) {P : Type u_2} (port : P ↪ V) [DecidableRel G.Adj] (hd : ∀ (v : V), G.degree v ≤ 2) (hb : ∀ (v : V), G.degree v = 1 ↔ ∃ (p : P), port p = v) (color : P → Bool) : (boundaryPairing G port hd hb).Compatible color ↔ ∃ (c : V → Bool), (∀ (p : P), c (port p) = color p) ∧ ∀ (x y : V), G.Adj x y → c x = c y

Every compatible boundary coloring extends through the wiring. This justifies replacing a cell's wiring by its boundary matching.

def Complexity.FiniteAutomaton.Pairing.glueAdj {A : Type u_1} {B : Type u_2} {C : Type u_3} (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) : (A ⊕ B) ⊕ B ⊕ C → (A ⊕ B) ⊕ B ⊕ C → Prop

Adjacency in the glued pairing graph.

Equations

• a.glueAdj b (Sum.inl x_2) (Sum.inl y) = a.link x_2 y
• a.glueAdj b (Sum.inr x_2) (Sum.inr y) = b.link x_2 y
• a.glueAdj b (Sum.inl (Sum.inr i)) (Sum.inr (Sum.inl j)) = (i = j)
• a.glueAdj b (Sum.inr (Sum.inl j)) (Sum.inl (Sum.inr i)) = (i = j)
• a.glueAdj b x✝¹ x✝ = False

def Complexity.FiniteAutomaton.Pairing.glueGraph {A : Type u_1} {B : Type u_2} {C : Type u_3} (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) : SimpleGraph ((A ⊕ B) ⊕ B ⊕ C)

Keep the two copies of the interface separate and join them by edges. This subdivision avoids parallel edges without changing boundary paths.

Equations

• a.glueGraph b = { Adj := a.glueAdj b, symm := ⋯, loopless := ⋯ }

def Complexity.FiniteAutomaton.Pairing.outer {A : Type u_1} {B : Type u_2} {C : Type u_3} : A ⊕ C ↪ (A ⊕ B) ⊕ B ⊕ C

Embed the external ports into the disjoint union of two glued diagrams.

Equations

• Complexity.FiniteAutomaton.Pairing.outer = { toFun := fun (x : A ⊕ C) => match x with | Sum.inl i => Sum.inl (Sum.inl i) | Sum.inr i => Sum.inr (Sum.inr i), inj' := ⋯ }

@[instance_reducible]

noncomputable instance Complexity.FiniteAutomaton.Pairing.glueDec {A : Type u_1} {B : Type u_2} {C : Type u_3} (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) : DecidableRel (a.glueGraph b).Adj

Equations

• a.glueDec b = Classical.decRel (a.glueGraph b).Adj

theorem Complexity.FiniteAutomaton.Pairing.glue_degree_LL {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (i : A) : (a.glueGraph b).degree (Sum.inl (Sum.inl i)) = 1

theorem Complexity.FiniteAutomaton.Pairing.glue_degree_RR {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (i : C) : (a.glueGraph b).degree (Sum.inr (Sum.inr i)) = 1

theorem Complexity.FiniteAutomaton.Pairing.glue_degree_LR {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (i : B) : (a.glueGraph b).degree (Sum.inl (Sum.inr i)) = 2

theorem Complexity.FiniteAutomaton.Pairing.glue_degree_RL {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (i : B) : (a.glueGraph b).degree (Sum.inr (Sum.inl i)) = 2

theorem Complexity.FiniteAutomaton.Pairing.glue_degree_le_two {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (v : (A ⊕ B) ⊕ B ⊕ C) : (a.glueGraph b).degree v ≤ 2

theorem Complexity.FiniteAutomaton.Pairing.glue_boundary {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (v : (A ⊕ B) ⊕ B ⊕ C) : (a.glueGraph b).degree v = 1 ↔ ∃ (p : A ⊕ C), outer p = v

noncomputable def Complexity.FiniteAutomaton.Pairing.compose {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) : Pairing (A ⊕ C)

Glue along the common interface and pair the surviving external ports.

Equations

• a.compose b = Complexity.FiniteAutomaton.FiniteWiring.boundaryPairing (a.glueGraph b) Complexity.FiniteAutomaton.Pairing.outer ⋯ ⋯

theorem Complexity.FiniteAutomaton.Pairing.compose_compatible {A : Type u_1} {B : Type u_2} {C : Type u_3} [Fintype A] [Fintype B] [Fintype C] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (f : A → Bool) (g : C → Bool) : (a.compose b).Compatible (Sum.elim f g) ↔ ∃ (k : B → Bool), a.Compatible (Sum.elim f k) ∧ b.Compatible (Sum.elim k g)

Boolean boundary behavior composes as ordinary relational composition.

def Complexity.FiniteAutomaton.Pairing.ofInvolution {P : Type u_1} (f : P → P) (hf : Function.Involutive f) (hn : ∀ (p : P), f p ≠ p) : Pairing P

The perfect matching given by a fixed-point-free involution.

Equations

• Complexity.FiniteAutomaton.Pairing.ofInvolution f hf hn = { link := fun (x y : P) => f x = y, symm := ⋯, irrefl := ⋯, unique := ⋯ }

def Complexity.FiniteAutomaton.Pairing.transport {P : Type u_1} {Q : Type u_2} (a : Pairing P) (e : P ≃ Q) : Pairing Q

Rename the ports of a pairing along an equivalence.

Equations

• a.transport e = { link := fun (x y : Q) => a.link (e.symm x) (e.symm y), symm := ⋯, irrefl := ⋯, unique := ⋯ }

def Complexity.FiniteAutomaton.Pairing.bijection {A : Type u_3} {B : Type u_4} (e : A ≃ B) : Pairing (A ⊕ B)

A rectangular permutation diagram; arbitrary equivalences also allow renumbering finite port sets without changing the underlying diagram.

Equations

• Complexity.FiniteAutomaton.Pairing.bijection e = Complexity.FiniteAutomaton.Pairing.ofInvolution (Sum.elim (Sum.inr ∘ ⇑e) (Sum.inl ∘ ⇑e.symm)) ⋯ ⋯

def Complexity.FiniteAutomaton.Pairing.identity (A : Type u_7) : Pairing (A ⊕ A)

The pairing that connects each left port to its equal right port.

Equations

• Complexity.FiniteAutomaton.Pairing.identity A = Complexity.FiniteAutomaton.Pairing.bijection (Equiv.refl A)

theorem Complexity.FiniteAutomaton.Pairing.bijection_compatible {A : Type u_3} {B : Type u_4} (e : A ≃ B) (f : A → Bool) (g : B → Bool) : (bijection e).Compatible (Sum.elim f g) ↔ ∀ (x : A), f x = g (e x)

theorem Complexity.FiniteAutomaton.Pairing.identity_compatible {A : Type u_3} (f g : A → Bool) : (identity A).Compatible (Sum.elim f g) ↔ f = g

theorem Complexity.FiniteAutomaton.Pairing.ext_colors {A : Type u_3} {B : Type u_4} {a b : Pairing (A ⊕ B)} (h : ∀ (f : A → Bool) (g : B → Bool), a.Compatible (Sum.elim f g) ↔ b.Compatible (Sum.elim f g)) : a = b

theorem Complexity.FiniteAutomaton.Pairing.connected_of_color_eq {P : Type u_1} (a : Pairing P) (x y : P) (h : ∀ (c : P → Bool), a.Compatible c → c x = c y) : a.connected x y

The Boolean equality semantics is faithful even for a single pair.

theorem Complexity.FiniteAutomaton.Pairing.link_of_color_eq {P : Type u_1} (a : Pairing P) {x y : P} (hne : x ≠ y) (h : ∀ (c : P → Bool), a.Compatible c → c x = c y) : a.link x y

theorem Complexity.FiniteAutomaton.Pairing.compose_assoc {A : Type u_3} {B : Type u_4} {C : Type u_5} {D : Type u_6} [Fintype A] [Fintype B] [Fintype C] [Fintype D] (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) (c : Pairing (C ⊕ D)) : (a.compose b).compose c = a.compose (b.compose c)

theorem Complexity.FiniteAutomaton.Pairing.identity_compose {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : (identity A).compose a = a

theorem Complexity.FiniteAutomaton.Pairing.compose_identity {A : Type u_3} {B : Type u_4} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : a.compose (identity B) = a