Two-way complementation: source

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Source.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.relationProduct {H : Type u_1} (w : List (SetRel H H)) : SetRel H H

Relation product for an input word; the empty product is the identity.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.relationProduct w = List.foldr SetRel.comp SetRel.id w

theorem Complexity.FiniteAutomaton.Complementation.Internal.relationProduct_append {H : Type u_1} (u v : List (SetRel H H)) : relationProduct (u ++ v) = (relationProduct u).comp (relationProduct v)

def Complexity.FiniteAutomaton.Complementation.Internal.sourceLanguage (H : Type u_1) : Set (List (SetRel H H))

The source language consists of the words with nonempty relation product.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.sourceLanguage H = {w : List (SetRel H H) | Set.Nonempty (Complexity.FiniteAutomaton.Complementation.Internal.relationProduct w)}

def Complexity.FiniteAutomaton.Complementation.Internal.sourceAutomaton (H : Type u_1) : TwoNFA (SetRel H H) (Option (Option H))

The explicit source machine: none starts, some none accepts, and some (some h) is the state labelled by h.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.sourceProductive {H : Type u_1} (w : List (SetRel H H)) : Set (Option (Option H) × Fin (w.length + 2))

Configurations from which the explicit source machine has a suffix witness.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.sourceProductive_of_step {H : Type u_1} (w : List (SetRel H H)) {c d : Option (Option H) × Fin (w.length + 2)} (hstep : (c, d) ∈ (sourceAutomaton H).step w) (hd : d ∈ sourceProductive w) : c ∈ sourceProductive w

theorem Complexity.FiniteAutomaton.Complementation.Internal.sourceAutomaton_sound {H : Type u_1} (w : List (SetRel H H)) (hw : w ∈ (sourceAutomaton H).language) : Set.Nonempty (relationProduct w)

theorem Complexity.FiniteAutomaton.Complementation.Internal.sourceAutomaton_suffix_run {H : Type u_1} (w u v : List (SetRel H H)) (hw : w = u ++ v) {p q : H} (hpq : (p, q) ∈ relationProduct v) : ((some (some p), ⟨u.length + 1, ⋯⟩), some none, ⟨w.length + 1, ⋯⟩) ∈ relStar ((sourceAutomaton H).step w)

theorem Complexity.FiniteAutomaton.Complementation.Internal.sourceAutomaton_language (H : Type u_1) : (sourceAutomaton H).language = sourceLanguage H

The explicit machine recognizes nonempty relation products.

theorem Complexity.FiniteAutomaton.Complementation.Internal.sourceLanguage_state_bound (H : Type u_1) [Fintype H] : ∃ (A : TwoNFA (SetRel H H) (Fin (Fintype.card H + 2))), A.language = sourceLanguage H

The source language on h labels is recognized using exactly h + 2 states.

theorem Complexity.FiniteAutomaton.Complementation.Internal.singleton_word_context {H : Type u_1} (w : List (SetRel H H)) (p q : H) : Set.Nonempty (relationProduct ([restrictedIdentity {p}] ++ w ++ [restrictedIdentity {q}])) ↔ (p, q) ∈ relationProduct w

Singleton letters on the two sides test one edge of a word's relation product.