One-way-liveness proof: Rank

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

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

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.identity_link {A : Type u_1} (x y : A ⊕ A) : (identity A).link x y ↔ x.swap = y

theorem Complexity.FiniteAutomaton.Pairing.eq_identity {A : Type u_1} (a : Pairing (A ⊕ A)) (h : ∀ (i : A), a.link (Sum.inl i) (Sum.inr i)) : a = identity A

theorem Complexity.FiniteAutomaton.Pairing.compose_link_iff {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)) (x y : A ⊕ C) : (a.compose b).link x y ↔ x ≠ y ∧ (a.glueGraph b).Reachable (outer x) (outer y)

theorem Complexity.FiniteAutomaton.Pairing.compose_left_cap {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 j : A} (h : a.link (Sum.inl i) (Sum.inl j)) : (a.compose b).link (Sum.inl i) (Sum.inl j)

theorem Complexity.FiniteAutomaton.Pairing.compose_right_cap {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 j : C} (h : b.link (Sum.inr i) (Sum.inr j)) : (a.compose b).link (Sum.inr i) (Sum.inr j)

theorem Complexity.FiniteAutomaton.Pairing.compose_transversal {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} {j : B} {k : C} (ha : a.link (Sum.inl i) (Sum.inr j)) (hb : b.link (Sum.inl j) (Sum.inr k)) : (a.compose b).link (Sum.inl i) (Sum.inr k)

noncomputable def Complexity.FiniteAutomaton.Pairing.lefts {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : Finset A

Left ports paired with a right port.

Equations

• a.lefts = {i : A | ∃ (j : B), a.link (Sum.inl i) (Sum.inr j)}

noncomputable def Complexity.FiniteAutomaton.Pairing.rights {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : Finset B

Right ports paired with a left port.

Equations

• a.rights = {j : B | ∃ (i : A), a.link (Sum.inl i) (Sum.inr j)}

noncomputable def Complexity.FiniteAutomaton.Pairing.rank {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : ℕ

The number of transversal paths from the left boundary to the right boundary.

Equations

• a.rank = a.lefts.card

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.mem_lefts {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) (i : A) : i ∈ a.lefts ↔ ∃ (j : B), a.link (Sum.inl i) (Sum.inr j)

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.mem_rights {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) (j : B) : j ∈ a.rights ↔ ∃ (i : A), a.link (Sum.inl i) (Sum.inr j)

noncomputable def Complexity.FiniteAutomaton.Pairing.transversalEquiv {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : ↥a.lefts ≃ ↥a.rights

The matching bijects its left and right transversal endpoints.

Equations

• a.transversalEquiv = Equiv.ofBijective (fun (i : ↥a.lefts) => ⟨⋯.choose, ⋯⟩) ⋯

theorem Complexity.FiniteAutomaton.Pairing.rank_eq_rights {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : a.rank = a.rights.card

theorem Complexity.FiniteAutomaton.Pairing.lefts_compose_subset {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)) : (a.compose b).lefts ⊆ a.lefts

theorem Complexity.FiniteAutomaton.Pairing.rights_compose_subset {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)) : (a.compose b).rights ⊆ b.rights

theorem Complexity.FiniteAutomaton.Pairing.rank_compose_le_left {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)) : (a.compose b).rank ≤ a.rank

theorem Complexity.FiniteAutomaton.Pairing.rank_compose_le_right {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)) : (a.compose b).rank ≤ b.rank

theorem Complexity.FiniteAutomaton.Pairing.rank_le_card {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) : a.rank ≤ Fintype.card A

noncomputable def Complexity.FiniteAutomaton.Pairing.support {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) : Finset A

Ports at which the pairing differs from the identity pairing.

Equations

• a.support = {i : A | ¬a.link (Sum.inl i) (Sum.inr i)}

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.mem_support {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) (i : A) : i ∈ a.support ↔ ¬a.link (Sum.inl i) (Sum.inr i)

theorem Complexity.FiniteAutomaton.Pairing.defect_le_support {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) : Fintype.card A - a.rank ≤ a.support.card

theorem Complexity.FiniteAutomaton.Pairing.support_compose_subset {A : Type u_1} [Fintype A] (a b : Pairing (A ⊕ A)) : (a.compose b).support ⊆ a.support ∪ b.support

theorem Complexity.FiniteAutomaton.Pairing.support_idempotent_subset {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e.compose e = e) : e.support ⊆ Finset.univ \ e.lefts ∪ Finset.univ \ e.rights

theorem Complexity.FiniteAutomaton.Pairing.support_idempotent_bound {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e.compose e = e) : e.support.card ≤ 2 * (Fintype.card A - e.rank)

theorem Complexity.FiniteAutomaton.Pairing.idempotent_full_rank {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e.compose e = e) (hr : e.rank = Fintype.card A) : e = identity A

theorem Complexity.FiniteAutomaton.Pairing.eq_of_link_imp {P : Type u_1} (a b : Pairing P) (h : ∀ (x y : P), a.link x y → b.link x y) : a = b

def Complexity.FiniteAutomaton.Pairing.flip {A : Type u_2} {B : Type u_3} (a : Pairing (A ⊕ B)) : Pairing (B ⊕ A)

Exchange the left and right boundaries of a pairing.

Equations

• a.flip = a.transport (Equiv.sumComm A B)

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.flip_link {A : Type u_2} {B : Type u_3} (a : Pairing (A ⊕ B)) (x y : B ⊕ A) : a.flip.link x y ↔ a.link x.swap y.swap

theorem Complexity.FiniteAutomaton.Pairing.flip_flip {A : Type u_2} {B : Type u_3} (a : Pairing (A ⊕ B)) : a.flip.flip = a

theorem Complexity.FiniteAutomaton.Pairing.left_cap_not_lefts {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) {i j : A} (h : a.link (Sum.inl i) (Sum.inl j)) : i ∉ a.lefts

theorem Complexity.FiniteAutomaton.Pairing.right_cap_not_rights {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) {i j : B} (h : a.link (Sum.inr i) (Sum.inr j)) : i ∉ a.rights

theorem Complexity.FiniteAutomaton.Pairing.compose_flip_eq_identity {A : Type u_2} {B : Type u_3} [Fintype A] [Fintype B] (a : Pairing (A ⊕ B)) (ha : ∀ (i : A), i ∈ a.lefts) : a.compose a.flip = identity A

theorem Complexity.FiniteAutomaton.Pairing.compose_cancel_left {A : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype A] [Fintype B] [Fintype C] (u : Pairing (A ⊕ B)) (v : Pairing (B ⊕ A)) (hu : v.compose u = identity B) {x y : Pairing (B ⊕ C)} (h : u.compose x = u.compose y) : x = y

theorem Complexity.FiniteAutomaton.Pairing.compose_cancel_right {A : Type u_2} {B : Type u_3} {C : Type u_4} [Fintype A] [Fintype B] [Fintype C] (u : Pairing (A ⊕ B)) (v : Pairing (B ⊕ A)) (hu : u.compose v = identity A) {x y : Pairing (C ⊕ A)} (h : x.compose u = y.compose u) : x = y

noncomputable def Complexity.FiniteAutomaton.Pairing.splitLeft {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) : Pairing (A ⊕ ↥e.lefts)

Retain the left caps and straighten the left transversal endpoints.

Equations

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

noncomputable def Complexity.FiniteAutomaton.Pairing.splitRight {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) : Pairing (↥e.lefts ⊕ A)

Retain the right caps and all the original transversals.

Equations

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

theorem Complexity.FiniteAutomaton.Pairing.splitLeft_splitRight {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) : e.splitLeft.compose e.splitRight = e

theorem Complexity.FiniteAutomaton.Pairing.splitLeft_inverse {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) : e.splitLeft.flip.compose e.splitLeft = identity ↥e.lefts

theorem Complexity.FiniteAutomaton.Pairing.splitRight_inverse {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) : e.splitRight.compose e.splitRight.flip = identity ↥e.lefts

theorem Complexity.FiniteAutomaton.Pairing.splitRight_splitLeft {A : Type u_2} [Fintype A] (e : Pairing (A ⊕ A)) (he : e.compose e = e) : e.splitRight.compose e.splitLeft = identity ↥e.lefts