One-way-liveness proof: Corners

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

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

theorem Complexity.FiniteAutomaton.exists_idempotent_power {M : Type u_1} [Monoid M] [Finite M] (a : M) : ∃ (n : ℕ), 0 < n ∧ a ^ n * a ^ n = a ^ n

Positive powers in any finite monoid contain an idempotent.

structure Complexity.FiniteAutomaton.Corner {M : Type u_1} [Monoid M] (e : M) (he : e * e = e) : Type u_1

The local monoid at an idempotent, with its genuine local identity.

• val : M

  The underlying element of the ambient monoid.

• left : e * self.val = self.val
• right : self.val * e = self.val

theorem Complexity.FiniteAutomaton.Corner.ext_iff {M : Type u_1} {inst✝ : Monoid M} {e : M} {he : e * e = e} {x y : Corner e he} : x = y ↔ x.val = y.val

theorem Complexity.FiniteAutomaton.Corner.ext {M : Type u_1} {inst✝ : Monoid M} {e : M} {he : e * e = e} {x y : Corner e he} (val : x.val = y.val) : x = y

@[instance_reducible]

instance Complexity.FiniteAutomaton.Corner.instCoeOut {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} : CoeOut (Corner e he) M

Equations

• Complexity.FiniteAutomaton.Corner.instCoeOut = { coe := Complexity.FiniteAutomaton.Corner.val }

@[instance_reducible]

instance Complexity.FiniteAutomaton.Corner.instMonoid {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} : Monoid (Corner e he)

Equations

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

@[simp]

theorem Complexity.FiniteAutomaton.Corner.val_one {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} : val 1 = e

@[simp]

theorem Complexity.FiniteAutomaton.Corner.val_mul {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} (x y : Corner e he) : (x * y).val = x.val * y.val

instance Complexity.FiniteAutomaton.Corner.instFinite {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} [Finite M] : Finite (Corner e he)

def Complexity.FiniteAutomaton.Corner.sandwich {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} (x : M) : Corner e he

Project an element into the corner by multiplication by the idempotent on both sides.

Equations

• Complexity.FiniteAutomaton.Corner.sandwich x = { val := e * x * e, left := ⋯, right := ⋯ }

theorem Complexity.FiniteAutomaton.Corner.val_pow_pos {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} (x : Corner e he) {n : ℕ} (hn : 0 < n) : (x ^ n).val = x.val ^ n

theorem Complexity.FiniteAutomaton.isUnit_of_injective_map_finite {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [Finite M] (f : M →* N) (hf : Function.Injective ⇑f) (a : M) (ha : IsUnit (f a)) : IsUnit a

def Complexity.FiniteAutomaton.Corner.mapTo {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {e : M} {he : e * e = e} {q : N} {hq : q * q = q} (f : M →* N) (hf : f e = q) : Corner e he →* Corner q hq

The monoid homomorphism induced on corners by an idempotent-preserving homomorphism.

Equations

• Complexity.FiniteAutomaton.Corner.mapTo f hf = { toFun := fun (x : Complexity.FiniteAutomaton.Corner e he) => { val := f x.val, left := ⋯, right := ⋯ }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Complexity.FiniteAutomaton.Corner.mapTo_val {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {e : M} {he : e * e = e} {q : N} {hq : q * q = q} (f : M →* N) (hf : f e = q) (x : Corner e he) : ((mapTo f hf) x).val = f x.val

theorem Complexity.FiniteAutomaton.Corner.mapTo_surjective {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] {e : M} {he : e * e = e} {q : N} {hq : q * q = q} (f : M →* N) (hf : f e = q) (hs : Function.Surjective ⇑f) : Function.Surjective ⇑(mapTo f hf)

theorem Complexity.FiniteAutomaton.Corner.val_idempotent {M : Type u_1} [Monoid M] {e : M} {he : e * e = e} (x : Corner e he) (hx : x * x = x) : x.val * x.val = x.val

theorem Complexity.FiniteAutomaton.Pairing.image_idempotent {A : Type u_1} [Fintype A] {M : Type u_2} [Monoid M] (ρ : M →* Pairing (A ⊕ A)) (e : M) (he : e * e = e) : ρ e * ρ e = ρ e

noncomputable def Complexity.FiniteAutomaton.Pairing.reduceHom {A : Type u_1} [Fintype A] {M : Type u_2} [Monoid M] (ρ : M →* Pairing (A ⊕ A)) (e : M) (he : e * e = e) : Corner e he →* Pairing (↥(ρ e).lefts ⊕ ↥(ρ e).lefts)

Compress a pairing representation to the transversal ports of an idempotent.

Equations

• Complexity.FiniteAutomaton.Pairing.reduceHom ρ e he = { toFun := fun (x : Complexity.FiniteAutomaton.Corner e he) => (ρ e).reduce (ρ x.val), map_one' := ⋯, map_mul' := ⋯ }

theorem Complexity.FiniteAutomaton.Pairing.reduceHom_injective {A : Type u_1} [Fintype A] {M : Type u_2} [Monoid M] (ρ : M →* Pairing (A ⊕ A)) (e : M) (he : e * e = e) (hρ : Function.Injective ⇑ρ) : Function.Injective ⇑(reduceHom ρ e he)

theorem Complexity.FiniteAutomaton.Pairing.reduceHom_rank {A : Type u_1} [Fintype A] {M : Type u_2} [Monoid M] (ρ : M →* Pairing (A ⊕ A)) (e : M) (he : e * e = e) (x : Corner e he) : ((reduceHom ρ e he) x).rank = (ρ x.val).rank

theorem Complexity.FiniteAutomaton.Pairing.reduceHom_common_support {A : Type u_1} [Fintype A] {M : Type u_2} [Monoid M] (ρ : M →* Pairing (A ⊕ A)) (e : M) (he : e * e = e) (J : Finset A) : ∃ (K : Finset ↥(ρ e).lefts), K.card ≤ J.card ∧ ∀ (a : M), (ρ a).support ⊆ J → ((reduceHom ρ e he) (Corner.sandwich a)).support ⊆ K

theorem Complexity.FiniteAutomaton.Pairing.rank_pow_le {A : Type u_1} [Fintype A] (a : Pairing (A ⊕ A)) {n : ℕ} (hn : 0 < n) : (a ^ n).rank ≤ a.rank

theorem Complexity.FiniteAutomaton.exists_idempotent_lift {M : Type u_1} {N : Type u_2} [Monoid M] [Monoid N] [Finite M] (f : M →* N) (hf : Function.Surjective ⇑f) (q : N) (hq : q * q = q) : ∃ (e : M), e * e = e ∧ f e = q

A lift of an idempotent can always be made idempotent without changing its image.

theorem Complexity.FiniteAutomaton.exists_min_rank_lift {M : Type u_1} {N : Type u_2} {A : Type u_3} [Monoid M] [Monoid N] [Finite M] [Fintype A] (ρ : M →* Pairing (A ⊕ A)) (f : M →* N) (hf : Function.Surjective ⇑f) (q : N) (hq : q * q = q) : ∃ (e : M), e * e = e ∧ f e = q ∧ ∀ (z : M), z * z = z → f z = q → (ρ e).rank ≤ (ρ z).rank

theorem Complexity.FiniteAutomaton.min_rank_corner_isUnit {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) (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) (y : Corner e he) (hy : IsUnit ((Corner.mapTo f hf) y)) : IsUnit y

Minimum rank over the local identity forces all local unit lifts to be units.

def Complexity.FiniteAutomaton.Corner.transfer {M : Type u_1} [Monoid M] {e f : M} {he : e * e = e} {hf : f * f = f} (u v : M) (huv : u * v = e) (hvu : v * u = f) (hu : u * f = u) (hv : f * v = v) : Corner e he →* Corner f hf

Transport a local monoid across a split pair.

Equations

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

def Complexity.FiniteAutomaton.Corner.equivOfSplit {M : Type u_1} [Monoid M] {e f : M} {he : e * e = e} {hf : f * f = f} (u v : M) (huv : u * v = e) (hvu : v * u = f) (hu : u * f = u) (hv : f * v = v) : Corner e he ≃* Corner f hf

The corner equivalence induced by a split pair of elements.

Equations

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