One-way-liveness proof: Relations

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/Automata/Relations.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.BRel.restrictedId_holds {H : Type u_1} (F : Set H) (x y : H) : (restrictedId F).holds x y ↔ x = y ∧ x ∈ F

theorem Complexity.FiniteAutomaton.BRel.restrictedId_idem {H : Type u_1} (F : Set H) : restrictedId F * restrictedId F = restrictedId F

theorem Complexity.FiniteAutomaton.BRel.restrictedId_mul {H : Type u_1} (F : Set H) (a : BRel H) (x y : H) : (restrictedId F * a).holds x y ↔ x ∈ F ∧ a.holds x y

theorem Complexity.FiniteAutomaton.BRel.mul_restrictedId {H : Type u_1} (F : Set H) (a : BRel H) (x y : H) : (a * restrictedId F).holds x y ↔ a.holds x y ∧ y ∈ F

theorem Complexity.FiniteAutomaton.BRel.corner_supported {H : Type u_1} {F : Set H} (z : Corner (restrictedId F) ⋯) {x y : H} (h : z.val.holds x y) : x ∈ F ∧ y ∈ F

def Complexity.FiniteAutomaton.BRel.restriction {H : Type u_1} (F : Set H) : Corner (restrictedId F) ⋯ →* BRel ↑F

Restrict a relation in the corner of a partial identity to its underlying subset.

Equations

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

def Complexity.FiniteAutomaton.BRel.extend {H : Type u_1} (F : Set H) (a : BRel ↑F) : BRel H

Extend a relation on a subset by leaving all other pairs unrelated.

Equations

• Complexity.FiniteAutomaton.BRel.extend F a = { holds := fun (x y : H) => ∃ (hx : x ∈ F) (hy : y ∈ F), a.holds ⟨x, hx⟩ ⟨y, hy⟩ }

def Complexity.FiniteAutomaton.BRel.extension {H : Type u_1} (F : Set H) (a : BRel ↑F) : Corner (restrictedId F) ⋯

View an extended relation as an element of the partial-identity corner.

Equations

• Complexity.FiniteAutomaton.BRel.extension F a = { val := Complexity.FiniteAutomaton.BRel.extend F a, left := ⋯, right := ⋯ }

def Complexity.FiniteAutomaton.BRel.restrictionEquiv {H : Type u_1} (F : Set H) : Corner (restrictedId F) ⋯ ≃* BRel ↑F

The corner of a partial identity is the relation monoid on its subset.

Equations

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

theorem Complexity.FiniteAutomaton.BRel.relation_corner {H : Type u_1} {P : BRel H} (hP : P * P = P) (F : Set H) (hF : restrictedId F * P * restrictedId F = restrictedId F) : have Q := P * restrictedId F * P; ∃ (hQ : Q * Q = Q) (θ : Corner Q hQ ≃* BRel ↑F), (∀ (z : Corner Q hQ) (x y : ↑F), (θ z).holds x y ↔ z.val.holds ↑x ↑y) ∧ P * Q = Q ∧ Q * P = Q

Restrict a relation corner with a split subidentity.

def Complexity.FiniteAutomaton.BRel.permGraph {H : Type u_1} (σ : Equiv.Perm H) : BRel H

The graph relation of a permutation.

Equations

• Complexity.FiniteAutomaton.BRel.permGraph σ = { holds := fun (x y : H) => σ x = y }

@[simp]

theorem Complexity.FiniteAutomaton.BRel.permGraph_holds {H : Type u_1} (σ : Equiv.Perm H) (x y : H) : (permGraph σ).holds x y ↔ σ x = y

def Complexity.FiniteAutomaton.BRel.permUnit {H : Type u_1} (σ : Equiv.Perm H) : (BRel H)ˣ

The invertible relation represented by a permutation.

Equations

• Complexity.FiniteAutomaton.BRel.permUnit σ = { val := Complexity.FiniteAutomaton.BRel.permGraph σ, inv := Complexity.FiniteAutomaton.BRel.permGraph (Equiv.symm σ), val_inv := ⋯, inv_val := ⋯ }

def Complexity.FiniteAutomaton.BRel.addEdge {H : Type u_1} (x y : H) : BRel H

The identity with one extra pair.

Equations

• Complexity.FiniteAutomaton.BRel.addEdge x y = { holds := fun (u v : H) => u = v ∨ u = x ∧ v = y }

@[simp]

theorem Complexity.FiniteAutomaton.BRel.addEdge_holds {H : Type u_1} (x y u v : H) : (addEdge x y).holds u v ↔ u = v ∨ u = x ∧ v = y

theorem Complexity.FiniteAutomaton.BRel.addEdge_idem {H : Type u_1} (x y : H) : addEdge x y * addEdge x y = addEdge x y

theorem Complexity.FiniteAutomaton.BRel.addEdge_ne_one {H : Type u_1} {x y : H} (hxy : x ≠ y) : addEdge x y ≠ 1

theorem Complexity.FiniteAutomaton.BRel.conjugate_addEdge {H : Type u_1} (σ : Equiv.Perm H) (x y : H) : ↑(permUnit σ)⁻¹ * addEdge x y * ↑(permUnit σ) = addEdge (σ x) (σ y)

theorem Complexity.FiniteAutomaton.BRel.exists_perm_pair {H : Type u_1} {x y u v : H} (hxy : x ≠ y) (huv : u ≠ v) : ∃ (σ : Equiv.Perm H), σ x = u ∧ σ y = v

def Complexity.FiniteAutomaton.HasUnitLifts {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (f : M →* N) : Prop

Every target unit admits a unit lift (unitality included in the homomorphism).

Equations

• Complexity.FiniteAutomaton.HasUnitLifts f = ∀ (u : Nˣ), ∃ (v : Mˣ), f ↑v = ↑u

theorem Complexity.FiniteAutomaton.unit_image_inv {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] (f : M →* N) (u : Mˣ) (v : Nˣ) (h : f ↑u = ↑v) : f ↑u⁻¹ = ↑v⁻¹

theorem Complexity.FiniteAutomaton.conjugate_lift {M : Type u_1} {H : Type u_2} {A : Type u_3} [Monoid M] [Fintype A] (ρ : M →* Pairing (A ⊕ A)) (f : M →* BRel H) (hl : HasUnitLifts f) (a : M) (ha : a * a = a) (x y : H) (hxy : x ≠ y) (hfa : f a = BRel.addEdge x y) (u v : H) (huv : u ≠ v) : ∃ (b : M), b * b = b ∧ f b = BRel.addEdge u v ∧ (ρ b).rank = (ρ a).rank

structure Complexity.FiniteAutomaton.RectangleFrame (H : Type u_1) (I : Type u_2) (J : Type u_3) : Type (max (max u_1 u_2) u_3)

Disjoint source/target points and a separate intermediate hub.

• left : I → H

  The row vertices of the frame.

• right : J → H

  The column vertices of the frame.

• hub : H

  The distinguished vertex outside the rows and columns.

• left_injective : Function.Injective self.left
• right_injective : Function.Injective self.right
• disjoint (i : I) (j : J) : self.left i ≠ self.right j
• left_ne_hub (i : I) : self.left i ≠ self.hub
• right_ne_hub (j : J) : self.right j ≠ self.hub

def Complexity.FiniteAutomaton.RectangleFrame.base {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) : BRel H

The partial identity outside the frame hub.

Equations

• F.base = Complexity.FiniteAutomaton.BRel.restrictedId {x : H | x ≠ F.hub}

def Complexity.FiniteAutomaton.RectangleFrame.rel {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E : Set (I × J)) : BRel H

Add the selected row-to-column edges to the identity outside the hub.

Equations

• F.rel E = { holds := fun (x y : H) => x = y ∧ x ≠ F.hub ∨ ∃ p ∈ E, x = F.left p.1 ∧ y = F.right p.2 }

@[simp]

theorem Complexity.FiniteAutomaton.RectangleFrame.rel_holds {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E : Set (I × J)) (x y : H) : (F.rel E).holds x y ↔ x = y ∧ x ≠ F.hub ∨ ∃ p ∈ E, x = F.left p.1 ∧ y = F.right p.2

theorem Complexity.FiniteAutomaton.RectangleFrame.rel_empty {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) : F.rel ∅ = F.base

theorem Complexity.FiniteAutomaton.RectangleFrame.rel_mul {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E D : Set (I × J)) : F.rel E * F.rel D = F.rel (E ∪ D)

theorem Complexity.FiniteAutomaton.RectangleFrame.rel_idem {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E : Set (I × J)) : F.rel E * F.rel E = F.rel E

theorem Complexity.FiniteAutomaton.RectangleFrame.rel_absorb {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) {E D : Set (I × J)} (h : E ⊆ D) : F.rel E * F.rel D = F.rel D ∧ F.rel D * F.rel E = F.rel D

theorem Complexity.FiniteAutomaton.RectangleFrame.generator_image {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (i : I) (j : J) : F.base * BRel.addEdge (F.left i) F.hub * BRel.addEdge F.hub (F.right j) * F.base = F.rel {(i, j)}

theorem Complexity.FiniteAutomaton.RectangleFrame.restricted_old {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E : Set (I × J)) (K : Set H) (hK : ∀ x ∈ K, x ≠ F.hub) (hE : ∀ p ∈ E, F.left p.1 ∉ K ∨ F.right p.2 ∉ K) : BRel.restrictedId K * F.rel E * BRel.restrictedId K = BRel.restrictedId K

theorem Complexity.FiniteAutomaton.RectangleFrame.restricted_new {H : Type u_1} {I : Type u_2} {J : Type u_3} (F : RectangleFrame H I J) (E : Set (I × J)) (K : Set H) (hK : ∀ x ∈ K, x ≠ F.hub) (hE : ∀ p ∈ E, F.left p.1 ∉ K ∨ F.right p.2 ∉ K) (i : I) (j : J) (hi : F.left i ∈ K) (hj : F.right j ∈ K) : have u := ⟨F.left i, hi⟩; have v := ⟨F.right j, hj⟩; ∀ (x y : ↑K), (F.rel (insert (i, j) E)).holds ↑x ↑y ↔ (BRel.addEdge u v).holds x y

def Complexity.FiniteAutomaton.Corner.flattenEquiv {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} (q : Corner e he) (hq : q * q = q) : Corner q hq ≃* Corner q.val ⋯

Flatten an iterated corner into the corner of the underlying idempotent.

Equations

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

theorem Complexity.FiniteAutomaton.HasUnitLifts.comp_equiv {M : Type u_1} {N : Type u_2} {P : Type u_3} [Monoid M] [Monoid N] [Monoid P] {f : M →* N} (hf : HasUnitLifts f) (e : N ≃* P) : HasUnitLifts (e.toMonoidHom.comp f)

theorem Complexity.FiniteAutomaton.min_rank_corner_unitLifts {M : Type u_1} {N : Type u_2} {A : Type u_3} [Monoid M] [Monoid N] [Finite M] [Fintype A] (ρ : M →* Pairing (A ⊕ A)) (hρ : Function.Injective ⇑ρ) (f : M →* N) (hs : Function.Surjective ⇑f) (e : M) (he : e * e = e) (q : N) (hq : q * q = q) (hf : f e = q) (hmin : ∀ (z : M), z * z = z → f z = q → (ρ e).rank ≤ (ρ z).rank) : HasUnitLifts (Corner.mapTo f hf)

theorem Complexity.FiniteAutomaton.BRel.restricted_sandwich {H : Type u_1} {P N : BRel H} (F : Set H) (hF : restrictedId F * P * restrictedId F = restrictedId F) (hPN : P * N = N) (hNP : N * P = N) : have Q := P * restrictedId F * P; restrictedId F * (Q * N * Q) * restrictedId F = restrictedId F * N * restrictedId F

theorem Complexity.FiniteAutomaton.BRel.sandwich_holds_on {H : Type u_1} {P N : BRel H} (F : Set H) (hF : restrictedId F * P * restrictedId F = restrictedId F) (hPN : P * N = N) (hNP : N * P = N) (x y : ↑F) : (P * restrictedId F * P * N * (P * restrictedId F * P)).holds ↑x ↑y ↔ N.holds ↑x ↑y