Documentation

Complexitylib.Models.FiniteAutomaton.Complementation.Internal.Chain

Two-way complementation: chain #

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

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

source
def Complexity.FiniteAutomaton.Complementation.Internal.ChainNode (m : ℕ) :
ℕ → Type

Internal vertices of a chain with one distinguished final cell.

Equations
Instances For
    source
    def Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.position {m n : ℕ} :
    ChainNode m n → ℕ

    Zero-based cell coordinate.

    Equations
    Instances For
      source
      def Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.label {m n : ℕ} :
      ChainNode m n → Fin m

      State label carried at a cell.

      Equations
      Instances For
        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.position_le {m n : ℕ} (c : ChainNode m n) :
        c.position ≤ n

        Every vertex belongs to one of the chain's cells.

        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.coordinates_injective {m n : ℕ} (c d : ChainNode m n) (hp : c.position = d.position) (hq : c.label = d.label) :
        c = d

        A cell coordinate and a state label uniquely identify an internal vertex.

        source
        theorem Complexity.FiniteAutomaton.Complementation.Internal.ChainNode.coordinates_surjective {m n : ℕ} (q : Fin m) (p : ℕ) (hp : p ≤ n) :
        ∃ (c : ChainNode m n), c.label = q ∧ c.position = p

        Every valid cell coordinate and state label occurs.

        source
        def Complexity.FiniteAutomaton.Complementation.Internal.chainSymbol {Sigma : Type u_1} {m : ℕ} (w : List Sigma) (last : Sigma) :
        ChainNode m w.length → Sigma

        The symbol at a vertex in a nonempty cell chain.

        Equations
        Instances For
          source
          def Complexity.FiniteAutomaton.Complementation.Internal.cellNetwork {m : ℕ} (moves : Fin 3 → SetRel (Fin m) (Fin m)) :
          Network m (Fin m)

          A single cell retains stays internally and exposes its two moving transitions.

          Equations
          Instances For
            source
            def Complexity.FiniteAutomaton.Complementation.Internal.chainNetwork {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) :
            Network m (ChainNode m w.length)

            Join a list of cells to a distinguished final cell.

            Equations
            Instances For
              source
              theorem Complexity.FiniteAutomaton.Complementation.Internal.chainNetwork_summary {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) :
              (chainNetwork moves w last).summary = wordDiagram (fun (a : Sigma) => cellDiagram m (moves a 1) (moves a 2) (moves a 0)) (w ++ [last])

              The path summary of a cell chain is the product of its cell diagrams.

              source
              theorem Complexity.FiniteAutomaton.Complementation.Internal.chainNetwork_entrances {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) (q : Fin m) (c : ChainNode m w.length) :
              ((q, c) ∈ (chainNetwork moves w last).leftIn ↔ c.position = 0 ∧ q = c.label) ∧ ((q, c) ∈ (chainNetwork moves w last).rightIn ↔ c.position = w.length ∧ q = c.label)

              Entrances attach exactly to the first and last cells with their unchanged labels.

              source
              theorem Complexity.FiniteAutomaton.Complementation.Internal.chainNetwork_exits {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) (c : ChainNode m w.length) (q : Fin m) :
              ((c, q) ∈ (chainNetwork moves w last).leftOut ↔ c.position = 0 ∧ (c.label, q) ∈ moves (chainSymbol w last c) 0) ∧ ((c, q) ∈ (chainNetwork moves w last).rightOut ↔ c.position = w.length ∧ (c.label, q) ∈ moves (chainSymbol w last c) 2)

              Only the endpoint cells can exit a chain, using the appropriate moving transition.

              source
              theorem Complexity.FiniteAutomaton.Complementation.Internal.chainNetwork_edges {Sigma : Type u_1} {m : ℕ} (moves : Sigma → Fin 3 → SetRel (Fin m) (Fin m)) (w : List Sigma) (last : Sigma) (c d : ChainNode m w.length) :
              (c, d) ∈ (chainNetwork moves w last).edge ↔ ∃ (move : Fin 3), (c.label, d.label) ∈ moves (chainSymbol w last c) move ∧ ↑d.position = ↑c.position + ↑↑move - 1

              Internal edges are precisely local transitions that stay within the chain.