One-way-liveness proof: Diagram

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

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

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

Only edge constraints in the starting component are needed.

noncomputable def Complexity.FiniteAutomaton.Pairing.marked {A : Type u_1} {B : Type u_2} [Fintype A] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (J : Finset B) : Finset A

Index the outer identity paths touched by a specified set of interface edges. The definition is made once, independently of a replacement diagram.

Equations

• v.marked u J = {x : A | ∃ i ∈ J, (v.glueGraph u).Reachable (Complexity.FiniteAutomaton.Pairing.outer (Sum.inl x)) (Sum.inl (Sum.inr i))}

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.mem_marked {A : Type u_1} {B : Type u_2} [Fintype A] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (J : Finset B) (x : A) : x ∈ v.marked u J ↔ ∃ i ∈ J, (v.glueGraph u).Reachable (outer (Sum.inl x)) (Sum.inl (Sum.inr i))

theorem Complexity.FiniteAutomaton.Pairing.left_reachable_eq {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (huv : v.compose u = identity A) {x y : A} (h : (v.glueGraph u).Reachable (outer (Sum.inl x)) (outer (Sum.inl y))) : x = y

theorem Complexity.FiniteAutomaton.Pairing.marked_card_le {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (huv : v.compose u = identity A) (J : Finset B) : (v.marked u J).card ≤ J.card

theorem Complexity.FiniteAutomaton.Pairing.support_sandwich_subset_marked {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (huv : v.compose u = identity A) (J : Finset B) (a : Pairing (B ⊕ B)) (ha : a.support ⊆ J) : ((v.compose a).compose u).support ⊆ v.marked u J

Unmarked original identity paths retain their equality constraints through every supported perturbation of the middle diagram.

theorem Complexity.FiniteAutomaton.Pairing.common_support {A : Type u_1} {B : Type u_2} [Fintype A] [Fintype B] (v : Pairing (A ⊕ B)) (u : Pairing (B ⊕ A)) (huv : v.compose u = identity A) (J : Finset B) : ∃ (K : Finset A), K.card ≤ J.card ∧ ∀ (a : Pairing (B ⊕ B)), a.support ⊆ J → ((v.compose a).compose u).support ⊆ K

The simultaneous support estimate: a single small set works for every middle diagram supported in the original set, including products and powers.

@[instance_reducible]

noncomputable instance Complexity.FiniteAutomaton.Pairing.instMonoidSum {A : Type u_1} [Fintype A] : Monoid (Pairing (A ⊕ A))

Equations

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

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.mul_eq_compose {A : Type u_1} [Fintype A] (a b : Pairing (A ⊕ A)) : a * b = a.compose b

@[simp]

theorem Complexity.FiniteAutomaton.Pairing.one_eq_identity {A : Type u_1} [Fintype A] : 1 = identity A

theorem Complexity.FiniteAutomaton.Pairing.rank_one {A : Type u_1} [Fintype A] : rank 1 = Fintype.card A

theorem Complexity.FiniteAutomaton.Pairing.support_one {A : Type u_1} [Fintype A] : support 1 = ∅

theorem Complexity.FiniteAutomaton.Pairing.rank_mul_le_left {A : Type u_1} [Fintype A] (a b : Pairing (A ⊕ A)) : (a * b).rank ≤ a.rank

theorem Complexity.FiniteAutomaton.Pairing.rank_mul_le_right {A : Type u_1} [Fintype A] (a b : Pairing (A ⊕ A)) : (a * b).rank ≤ b.rank

theorem Complexity.FiniteAutomaton.Pairing.full_rank_isUnit {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) (h : a.rank = Fintype.card A) : IsUnit a

theorem Complexity.FiniteAutomaton.Pairing.rank_eq_card_of_isUnit {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) (h : IsUnit a) : a.rank = Fintype.card A

theorem Complexity.FiniteAutomaton.Pairing.rank_mul_unit {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) (u : (Pairing (A ⊕ A))ˣ) : (a * ↑u).rank = a.rank

theorem Complexity.FiniteAutomaton.Pairing.rank_unit_mul {A : Type u_1} [Fintype A] (u : (Pairing (A ⊕ A))ˣ) (a : Pairing (A ⊕ A)) : (↑u * a).rank = a.rank

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

theorem Complexity.FiniteAutomaton.Pairing.support_pow_subset {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) (n : ℕ) : (a ^ n).support ⊆ a.support

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

Delete the prescribed caps of an idempotent. Its retained left endpoints are used as the smaller index set, avoiding an arbitrary numbering.

Equations

• e.reduce z = (e.splitRight.compose z).compose e.splitLeft

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

Expand a pairing on the surviving transversal ports back to the full boundary.

Equations

• e.expand z = (e.splitLeft.compose z).compose e.splitRight

theorem Complexity.FiniteAutomaton.Pairing.expand_reduce {A : Type u_1} [Fintype A] (e z : Pairing (A ⊕ A)) : e.expand (e.reduce z) = e * z * e

theorem Complexity.FiniteAutomaton.Pairing.reduce_expand {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e * e = e) (z : Pairing (↥e.lefts ⊕ ↥e.lefts)) : e.reduce (e.expand z) = z

theorem Complexity.FiniteAutomaton.Pairing.splitRight_absorb {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e * e = e) : e.splitRight.compose e = e.splitRight

theorem Complexity.FiniteAutomaton.Pairing.splitLeft_absorb {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e * e = e) : e.compose e.splitLeft = e.splitLeft

theorem Complexity.FiniteAutomaton.Pairing.reduce_self {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e * e = e) : e.reduce e = 1

theorem Complexity.FiniteAutomaton.Pairing.reduce_mul {A : Type u_1} [Fintype A] (e x y : Pairing (A ⊕ A)) (hxe : x * e = x) : e.reduce (x * y) = e.reduce x * e.reduce y

theorem Complexity.FiniteAutomaton.Pairing.reduce_sandwich {A : Type u_1} [Fintype A] (e a : Pairing (A ⊕ A)) (he : e * e = e) : e.reduce (e * a * e) = e.reduce a

theorem Complexity.FiniteAutomaton.Pairing.rank_reduce {A : Type u_1} [Fintype A] (e z : Pairing (A ⊕ A)) (hzl : e * z = z) (hzr : z * e = z) : (e.reduce z).rank = z.rank

theorem Complexity.FiniteAutomaton.Pairing.reduce_injective {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) {x y : Pairing (A ⊕ A)} (hxl : e * x = x) (hxr : x * e = x) (hyl : e * y = y) (hyr : y * e = y) (h : e.reduce x = e.reduce y) : x = y

theorem Complexity.FiniteAutomaton.Pairing.reduce_common_support {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) (he : e * e = e) (J : Finset A) : ∃ (K : Finset ↥e.lefts), K.card ≤ J.card ∧ ∀ (a : Pairing (A ⊕ A)), a.support ⊆ J → (e.reduce (e * a * e)).support ⊆ K

theorem Complexity.FiniteAutomaton.Pairing.card_reduced {A : Type u_1} [Fintype A] (e : Pairing (A ⊕ A)) : Fintype.card ↥e.lefts = e.rank