Two-way complementation: recognition #
Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a.
Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Recognition.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.word_diagram_order_reversal
{H : Type u_1}
{m : ℕ}
(τ : List (SetRel H H) → Diagram m)
(hmul : ∀ (u v : List (SetRel H H)), τ (u ++ v) = (τ u).comp (τ v))
(l r : Diagram m)
(a b : Fin m)
(hlanguage : ∀ (w : List (SetRel H H)), (a, b) ∈ ((l.comp (τ w)).comp r).forward ↔ ¬Set.Nonempty (relationProduct w))
{u v : List (SetRel H H)}
(huv : (τ u, τ v) ∈ Diagram.inclusion m)
:
Singleton contexts force reversal of relation inclusion.
theorem
Complexity.FiniteAutomaton.Complementation.Internal.diagram_relation_image
{H : Type u_1}
{m : ℕ}
(τ : List (SetRel H H) → Diagram m)
(hzero : τ [] = Diagram.identity m)
(hmul : ∀ (u v : List (SetRel H H)), τ (u ++ v) = (τ u).comp (τ v))
(l r : Diagram m)
(a b : Fin m)
(hlanguage : ∀ (w : List (SetRel H H)), (a, b) ∈ ((l.comp (τ w)).comp r).forward ↔ ¬Set.Nonempty (relationProduct w))
:
∃ (S : Submonoid (Diagram m)) (φ : ↥S →* RelationMonoid H),
Function.Surjective ⇑φ ∧ ∀ (z w : ↥S), (↑z, ↑w) ∈ Diagram.inclusion m → (φ w).toRel ⊆ (φ z).toRel
The relation product descends to the diagram image by singleton-context tests.
theorem
Complexity.FiniteAutomaton.Complementation.Internal.diagram_recognition_lower_bound
(h m : ℕ)
(hh : 2 ≤ h)
(hm : 1 ≤ m)
(τ : List (SetRel (Fin h) (Fin h)) → Diagram m)
(hzero : τ [] = Diagram.identity m)
(hmul : ∀ (u v : List (SetRel (Fin h) (Fin h))), τ (u ++ v) = (τ u).comp (τ v))
(l r : Diagram m)
(a b : Fin m)
(hlanguage :
∀ (w : List (SetRel (Fin h) (Fin h))), (a, b) ∈ ((l.comp (τ w)).comp r).forward ↔ ¬Set.Nonempty (relationProduct w))
:
Recognition of relation-product emptiness forces the image theorem's state bound.