Two-way complementation: network

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

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

def Complexity.FiniteAutomaton.Complementation.Internal.cellDiagram (m : ℕ) (stay right left : SetRel (Fin m) (Fin m)) : Diagram m

Single-cell diagram from stay, rightward, and leftward augmented transitions.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.wordDiagram {Sigma : Type u_1} {m : ℕ} (d : Sigma → Diagram m) (w : List Sigma) : Diagram m

Multiply the single-letter diagrams in input order, using identity for the empty word.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.wordDiagram d w = (List.map d w).prod

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.wordDiagram_nil {Sigma : Type u_1} {m : ℕ} (d : Sigma → Diagram m) : wordDiagram d [] = Diagram.identity m

theorem Complexity.FiniteAutomaton.Complementation.Internal.wordDiagram_append {Sigma : Type u_1} {m : ℕ} (d : Sigma → Diagram m) (u v : List Sigma) : wordDiagram d (u ++ v) = (wordDiagram d u).comp (wordDiagram d v)

theorem Complexity.FiniteAutomaton.Complementation.Internal.blockRelation_star_swap {α : Type u_1} {β : Type u_2} (E : SetRel α α) (F : SetRel α β) (G : SetRel β α) (H : SetRel β β) (x y : α ⊕ β) : (x.swap, y.swap) ∈ relStar (blockRelation H G F E) ↔ (x, y) ∈ relStar (blockRelation E F G H)

Swap the two vertex blocks without changing the finite-path semantics.

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

The left-left version of block elimination.

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

The right-left version of block elimination.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_entry_feedback {Q : Type u_1} {V : Type u_2} (I : SetRel Q V) (E : SetRel V V) (O R : SetRel V Q) (X : SetRel Q Q) : (I.comp (relStar (E ∪ (R.comp X).comp I))).comp O = (relStar (((I.comp (relStar E)).comp R).comp X)).comp ((I.comp (relStar E)).comp O)

Eliminate an internal graph while retaining arbitrary repeated feedback at its entry.

theorem Complexity.FiniteAutomaton.Complementation.Internal.relStar_general_feedback {Q : Type u_1} {V : Type u_2} (I J : SetRel Q V) (E : SetRel V V) (O R : SetRel V Q) (X : SetRel Q Q) : (I.comp (relStar (E ∪ (R.comp X).comp J))).comp O = (I.comp (relStar E)).comp O ∪ ((((((I.comp (relStar E)).comp R).comp (relStar (((X.comp J).comp (relStar E)).comp R))).comp X).comp J).comp (relStar E)).comp O

Internal paths either avoid the feedback edge or use it after a first internal segment.

structure Complexity.FiniteAutomaton.Complementation.Internal.Network (m : ℕ) (V : Type u_1) : Type u_1

A finite-path network with labelled entrances and exits at both boundaries.

• edge : SetRel V V

  Internal transitions.

• leftIn : SetRel (Fin m) V

  Left boundary entrance.

• rightIn : SetRel (Fin m) V

  Right boundary entrance.

• leftOut : SetRel V (Fin m)

  Left boundary exit.

• rightOut : SetRel V (Fin m)

  Right boundary exit.

def Complexity.FiniteAutomaton.Complementation.Internal.Network.summary {m : ℕ} {V : Type u_1} (N : Network m V) : Diagram m

Summarize all finite internal paths between the four boundary pairs.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Network.join {m : ℕ} {V : Type u_1} {W : Type u_2} (N : Network m V) (M : Network m W) : Network m (V ⊕ W)

Join two networks, wiring the adjacent exits to entrances in both directions.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.Network.summary_join {m : ℕ} {V : Type u_1} {W : Type u_2} (N : Network m V) (M : Network m W) : (N.join M).summary = N.summary.comp M.summary

Joining path networks implements exactly the four diagram multiplication formulas.