Two-way complementation: diagram

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

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

structure Complexity.FiniteAutomaton.Complementation.Internal.Diagram (m : ℕ) : Type

Four boundary relations; the direction distinguishes the two copies of Fin m.

• forward : SetRel (Fin m) (Fin m)

  Enter on the left and exit on the right.

• backward : SetRel (Fin m) (Fin m)

  Enter on the right and exit on the left.

• left : SetRel (Fin m) (Fin m)

  Enter and exit on the left.

• right : SetRel (Fin m) (Fin m)

  Enter and exit on the right.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.ext {m : ℕ} {x y : Diagram m} (forward : x.forward = y.forward) (backward : x.backward = y.backward) (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.ext_iff {m : ℕ} {x y : Diagram m} : x = y ↔ x.forward = y.forward ∧ x.backward = y.backward ∧ x.left = y.left ∧ x.right = y.right

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp {m : ℕ} (a b : Diagram m) : Diagram m

Composition of boundary diagrams in path order.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.identity (m : ℕ) : Diagram m

Identity boundary diagram.

Equations

• Complexity.FiniteAutomaton.Complementation.Internal.Diagram.identity m = { forward := SetRel.id, backward := SetRel.id, left := ∅, right := ∅ }

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.inclusion (m : ℕ) : SetRel (Diagram m) (Diagram m)

Componentwise edge inclusion, as a relation on diagrams.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.inclusion_refl {m : ℕ} (a : Diagram m) : (a, a) ∈ inclusion m

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.reflect {m : ℕ} (a : Diagram m) : Diagram m

Reflection reverses the order of multiplication.

Equations

• a.reflect = { forward := a.backward, backward := a.forward, left := a.right, right := a.left }

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.through {m : ℕ} (a : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m)

true denotes the positive sign; false denotes the negative sign.

Equations

• a.through positive = if positive = true then a.forward else a.backward

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.loopClosure {m : ℕ} (e : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m)

Closure of alternating returns at a boundary.

Equations

• e.loopClosure positive = Complexity.FiniteAutomaton.Complementation.Internal.relStar (if positive = true then e.left.comp e.right else e.right.comp e.left)

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.recurrence {m : ℕ} (e : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m)

The recurrent relation obtained by closing through traversals.

Equations

• e.recurrence positive = ((e.loopClosure positive).comp (e.through positive)).comp (e.loopClosure positive)

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classes {m : ℕ} (e : Diagram m) : Set (Bool × Set (Fin m))

Signed recurrent equivalence classes of an idempotent diagram.

Equations

• e.classes = {c : Bool × Set (Fin m) | ∃ (x : Fin m), (x, x) ∈ e.recurrence c.1 ∧ c.2 = {y : Fin m | (x, y) ∈ e.recurrence c.1 ∧ (y, x) ∈ e.recurrence c.1}}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner {m : ℕ} (e : Diagram m) : Set (Diagram m)

The corner membership equations for an idempotent e.

Equations

• e.corner = {z : Complexity.FiniteAutomaton.Complementation.Internal.Diagram m | e.comp z = z ∧ z.comp e = z}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nesting (m : ℕ) : SetRel (Diagram m) (Diagram m)

Nesting of idempotents; distinct from edge inclusion.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.surviving {m : ℕ} (e z : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m)

The surviving through relation U relative to e.

Equations

• e.surviving z positive = ((e.loopClosure positive).comp (z.through positive)).comp (e.loopClosure positive)

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.missing {m : ℕ} (e z : Diagram m) : Set (Bool × Set (Fin m))

Classes whose recurrent loops are absent after replacement by z.

Equations

• e.missing z = {c : Bool × Set (Fin m) | c ∈ e.classes ∧ ∀ x ∈ c.2, (x, x) ∉ e.surviving z c.1}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.unprotected {m : ℕ} (e : Diagram m) (P : Set (Bool × Fin m)) : Set (Bool × Set (Fin m))

Classes containing none of a fixed set of signed protected labels.

Equations

• e.unprotected P = {c : Bool × Set (Fin m) | c ∈ e.classes ∧ ∀ x ∈ c.2, (c.1, x) ∉ P}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.rectangle {m : ℕ} (e : Diagram m) (positive : Bool) (p : Fin m) : SetRel (Fin m) (Fin m)

Rectangle associated with a recurrent representative.

Equations

• e.rectangle positive p = {u : Fin m | (u, p) ∈ (e.through positive).comp (e.loopClosure positive)} ×ˢ {v : Fin m | (p, v) ∈ (e.loopClosure positive).comp (e.through positive)}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.portRelation {m : ℕ} (e : Diagram m) : SetRel (Bool × Fin m) (Bool × Fin m)

Boundary ports: false is left and true is right.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.bounceRelation {m : ℕ} (R L : SetRel (Fin m) (Fin m)) : SetRel (Bool × Fin m) (Bool × Fin m)

Returns from an exit port through the surrounding left or right context.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.feedback {m : ℕ} (e : Diagram m) (R L : SetRel (Fin m) (Fin m)) : SetRel (Bool × Fin m) (Bool × Fin m)

A middle traversal followed by any finite number of context returns and traversals.

Equations

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.mem_port_through {m : ℕ} (e : Diagram m) (positive : Bool) (p q : Fin m) : ((!positive, p), positive, q) ∈ e.portRelation ↔ (p, q) ∈ e.through positive

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classRectangle {m : ℕ} (e : Diagram m) (C : Bool × Set (Fin m)) : SetRel (Bool × Fin m) (Bool × Fin m)

The rectangular port edges belonging to a signed recurrent class.

Equations

• e.classRectangle C = {pair : (Bool × Fin m) × Bool × Fin m | pair.1.1 = !C.1 ∧ pair.2.1 = C.1 ∧ ∃ p ∈ C.2, (pair.1.2, pair.2.2) ∈ e.rectangle C.1 p}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.contextEntry {m : ℕ} (d u v : Diagram m) (positive : Bool) : SetRel (Fin m) (Bool × Fin m)

Initial traversal of the outer context, including recurrence closure.

Equations

• d.contextEntry u v positive = {pair : Fin m × Bool × Fin m | pair.2.1 = !positive ∧ (pair.1, pair.2.2) ∈ (d.loopClosure positive).comp (if positive = true then u.forward else v.backward)}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.contextExit {m : ℕ} (d u v : Diagram m) (positive : Bool) : SetRel (Bool × Fin m) (Fin m)

Final traversal of the outer context, including recurrence closure.

Equations

• d.contextExit u v positive = {pair : (Bool × Fin m) × Fin m | pair.1.1 = positive ∧ (pair.1.2, pair.2) ∈ (if positive = true then v.forward else u.backward).comp (d.loopClosure positive)}

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classInfluence {m : ℕ} (e d u v : Diagram m) (positive : Bool) (C : Bool × Set (Fin m)) : SetRel (Fin m) (Fin m)

Traversals with one designated occurrence of a recurrent rectangle in the middle factor.

Equations

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

def Complexity.FiniteAutomaton.Complementation.Internal.Diagram.transportMarked {m : ℕ} (e d u v : Diagram m) (J : Set (Bool × Set (Fin m))) : Set (Bool × Set (Fin m))

Target classes whose original traversals can use a rectangle from the fixed set J.

Equations

• e.transportMarked d u v J = {D : Bool × Set (Fin m) | D ∈ d.classes ∧ ∃ C ∈ J, ∃ x ∈ D.2, (x, x) ∈ e.classInfluence d u v D.1 C}

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.feedback_forward {m : ℕ} (e : Diagram m) (R L : SetRel (Fin m) (Fin m)) {p q : Fin m} : ((false, p), true, q) ∈ e.feedback R L ↔ (p, q) ∈ ((relStar (e.left.comp R)).comp e.forward).comp (relStar (L.comp (e.right ∪ ((e.backward.comp R).comp (relStar (e.left.comp R))).comp e.forward)))

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.identity_comp {m : ℕ} (a : Diagram m) : (identity m).comp a = a

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp_identity {m : ℕ} (a : Diagram m) : a.comp (identity m) = a

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.reflect_comp {m : ℕ} (a b : Diagram m) : (a.comp b).reflect = b.reflect.comp a.reflect

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.feedback_reflect_map {m : ℕ} (e : Diagram m) (R L : SetRel (Fin m) (Fin m)) {s t : Bool} {p q : Fin m} (h : ((s, p), t, q) ∈ e.feedback R L) : ((!s, p), !t, q) ∈ e.reflect.feedback L R

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.mem_feedback_reflect {m : ℕ} (e : Diagram m) (R L : SetRel (Fin m) (Fin m)) {s t : Bool} {p q : Fin m} : ((s, p), t, q) ∈ e.reflect.feedback L R ↔ ((!s, p), !t, q) ∈ e.feedback R L

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp_assoc_forward {m : ℕ} (a b c : Diagram m) : ((a.comp b).comp c).forward = (a.comp (b.comp c)).forward

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp_assoc_left {m : ℕ} (a b c : Diagram m) : ((a.comp b).comp c).left = (a.comp (b.comp c)).left

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp_assoc {m : ℕ} (a b c : Diagram m) : (a.comp b).comp c = a.comp (b.comp c)

The product of boundary diagrams is associative.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.context_forward_iff {m : ℕ} (u e v : Diagram m) {p q : Fin m} : (p, q) ∈ ((u.comp e).comp v).forward ↔ ∃ (a : Fin m) (b : Fin m), (p, a) ∈ u.forward ∧ ((false, a), true, b) ∈ e.feedback u.right v.left ∧ (b, q) ∈ v.forward

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.context_through_iff {m : ℕ} (u e v : Diagram m) (positive : Bool) {p q : Fin m} : (p, q) ∈ ((u.comp e).comp v).through positive ↔ ∃ (a : Fin m) (b : Fin m), ((p, a) ∈ if positive = true then u.forward else v.backward) ∧ ((!positive, a), positive, b) ∈ e.feedback u.right v.left ∧ (b, q) ∈ if positive = true then v.forward else u.backward

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.context_surviving {m : ℕ} (d u e v : Diagram m) (positive : Bool) : d.surviving ((u.comp e).comp v) positive = ((d.contextEntry u v positive).comp (e.feedback u.right v.left)).comp (d.contextExit u v positive)

@[instance_reducible]

instance Complexity.FiniteAutomaton.Complementation.Internal.Diagram.instMonoid {m : ℕ} : Monoid (Diagram m)

Equations

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

instance Complexity.FiniteAutomaton.Complementation.Internal.Diagram.finite_diagram {m : ℕ} : Finite (Diagram m)