Two-way complementation: relations

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

Imports, namespaces, module visibility, documentation, and formatting are adapted for complexitylib. The source theorem statements and mathematical arguments are retained.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_mono {α : Type u_1} {R S : SetRel α α} (h : R ⊆ S) : relStar R ⊆ relStar S

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_empty {α : Type u_1} : relStar ∅ = SetRel.id

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_comp_self {α : Type u_1} (R : SetRel α α) : (relStar R).comp (relStar R) = relStar R

def Complexity.FiniteAutomaton.Complementation.Internal.blockRelation {α : Type u_1} {β : Type u_2} (E : SetRel α α) (F : SetRel α β) (G : SetRel β α) (H : SetRel β β) : SetRel (α ⊕ β) (α ⊕ β)

A directed graph partitioned into two kinds of vertices.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.blockRelation_star_right {α : Type u_1} {β : Type u_2} (E : SetRel α α) (F : SetRel α β) (G : SetRel β α) (H : SetRel β β) (x y : β) : (Sum.inr x, Sum.inr y) ∈ relStar (blockRelation E F G H) ↔ (x, y) ∈ relStar (H ∪ (G.comp (relStar E)).comp F)

Eliminate the left block by replacing each finite excursion with one edge.

theorem Complexity.FiniteAutomaton.Complementation.Internal.blockRelation_star_cross {α : Type u_1} {β : Type u_2} (E : SetRel α α) (F : SetRel α β) (G : SetRel β α) (H : SetRel β β) (x : α) (y : β) : (Sum.inl x, Sum.inr y) ∈ relStar (blockRelation E F G H) ↔ (x, y) ∈ ((relStar E).comp F).comp (relStar (H ∪ (G.comp (relStar E)).comp F))

A path from the left block first leaves it once, then makes arbitrary finite excursions.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_union {α : Type u_1} (A B : SetRel α α) : relStar (A ∪ B) = (relStar A).comp (relStar (B.comp (relStar A)))

Closure of a union factors into alternating finite paths.

theorem Complexity.FiniteAutomaton.Complementation.Internal.comp_relStar_rotate {α : Type u_1} {β : Type u_2} (A : SetRel α β) (B : SetRel β α) : A.comp (relStar (B.comp A)) = (relStar (A.comp B)).comp A

A finite alternating path can be rotated between its endpoint types.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relComp_union {α : Type u_1} {β : Type u_2} {γ : Type u_3} (A : SetRel α β) (B C : SetRel β γ) : A.comp (B ∪ C) = A.comp B ∪ A.comp C

theorem Complexity.FiniteAutomaton.Complementation.Internal.union_relComp {α : Type u_1} {β : Type u_2} {γ : Type u_3} (A B : SetRel α β) (C : SetRel β γ) : (A ∪ B).comp C = A.comp C ∪ B.comp C

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_unfold {α : Type u_1} (R : SetRel α α) : relStar R = SetRel.id ∪ (relStar R).comp R

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_block_forward {α : Type u_1} (A B C D : SetRel α α) : ((relStar (A ∪ (B.comp (relStar D)).comp C)).comp B).comp (relStar D) = ((relStar A).comp B).comp (relStar (D ∪ (C.comp (relStar A)).comp B))

Eliminating two internal boundaries in either order gives the same through relation.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_block_return {α : Type u_1} (A B C D : SetRel α α) : relStar (A ∪ (B.comp (relStar D)).comp C) = relStar A ∪ ((((relStar A).comp B).comp (relStar (D ∪ (C.comp (relStar A)).comp B))).comp C).comp (relStar A)

The corresponding return relation when eliminating two internal boundaries.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_comp_unfold {α : Type u_1} {β : Type u_2} (R : SetRel α β) (L : SetRel β α) : relStar (R.comp L) = SetRel.id ∪ (R.comp (relStar (L.comp R))).comp L

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_block_exit {α : Type u_1} (L R B E D : SetRel α α) : (relStar (L.comp R ∪ ((B.comp (relStar D)).comp E).comp R)).comp (L ∪ (B.comp (relStar D)).comp E) = (relStar (L.comp R)).comp L ∪ ((((relStar (L.comp R)).comp B).comp (relStar (D ∪ ((E.comp R).comp (relStar (L.comp R))).comp B))).comp E).comp (relStar (R.comp L))

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_lost_edge {α : Type u_1} (R S : SetRel α α) {x y : α} (hxy : (x, y) ∈ relStar R) (hnot : (x, y) ∉ relStar S) : ∃ (a : α) (b : α), (x, a) ∈ relStar R ∧ (a, b) ∈ R ∧ (a, b) ∉ S ∧ (b, y) ∈ relStar R

A path lost after an edge replacement contains a lost edge between old path segments.

theorem Complexity.FiniteAutomaton.Complementation.Internal.feedback_lost_edge {α : Type u_1} (E E' B : SetRel α α) {x y : α} (hxy : (x, y) ∈ E.comp (relStar (B.comp E))) (hnot : (x, y) ∉ E'.comp (relStar (B.comp E'))) : ∃ (a : α) (b : α), (x, a) ∈ relStar (E.comp B) ∧ (a, b) ∈ E ∧ (a, b) ∉ E' ∧ (b, y) ∈ relStar (B.comp E)

A lost alternating traversal has a lost edge, allowing earlier and later bounces.

theorem Complexity.FiniteAutomaton.Complementation.Internal.feedback_insert {α : Type u_1} (E B : SetRel α α) : ((relStar (E.comp B)).comp E).comp (relStar (B.comp E)) = E.comp (relStar (B.comp E))

theorem Complexity.FiniteAutomaton.Complementation.Internal.weighted_class_bound {α : Type u_1} {β : Type u_2} (X M : Finset α) (Y : Finset β) (R : β → α → Prop) (hM : M ⊆ X) (hunique : ∀ y ∈ Y, ∀ z ∈ Y, ∀ x ∈ X, R y x → R z x → y = z) (hcover : ∀ y ∈ Y, (∃ x ∈ X, x ∉ M ∧ R y x) ∨ ∃ x ∈ X, ∃ z ∈ X, x ≠ z ∧ R y x ∧ R y z) : 2 * Y.card + M.card ≤ 2 * X.card

A bound for weighted classes with integer weights one and two.

theorem Complexity.FiniteAutomaton.Complementation.Internal.idempotent_relation_factor {α : Type u_1} [Finite α] (P : SetRel α α) (hP : P.comp P = P) {u v : α} (huv : (u, v) ∈ P) : ∃ (p : α), (u, p) ∈ P ∧ (p, p) ∈ P ∧ (p, v) ∈ P

Every edge of a finite idempotent relation factors through a recurrent point.