Two-way complementation: classes

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Classes.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.Diagram.corner_comp {m : ℕ} {e z w : Diagram m} (hz : z ∈ e.corner) (hw : w ∈ e.corner) : z.comp w ∈ e.corner

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_pow_succ {m : ℕ} {e z : Diagram m} (hz : z ∈ e.corner) (k : ℕ) : z ^ (k + 1) ∈ e.corner

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nesting_refl {m : ℕ} {e : Diagram m} (he : e.comp e = e) : (e, e) ∈ nesting m

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nesting_trans {m : ℕ} {d e f : Diagram m} (hde : (d, e) ∈ nesting m) (hef : (e, f) ∈ nesting m) : (d, f) ∈ nesting m

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.comp_mono {m : ℕ} {a a' b b' : Diagram m} (ha : (a, a') ∈ inclusion m) (hb : (b, b') ∈ inclusion m) : (a.comp b, a'.comp b') ∈ inclusion m

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.through_loop_through {m : ℕ} (e : Diagram m) (he : e.comp e = e) (positive : Bool) : ((e.through positive).comp (e.loopClosure positive)).comp (e.through positive) = e.through positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.recurrence_idempotent {m : ℕ} (e : Diagram m) (he : e.comp e = e) (positive : Bool) : (e.recurrence positive).comp (e.recurrence positive) = e.recurrence positive

Idempotence of the recurrence relation.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_returns {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) : e.left ⊆ z.left ∧ e.right ⊆ z.right

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_forward_absorption {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) : (e.forward.comp (e.loopClosure true)).comp z.forward ⊆ z.forward ∧ (z.forward.comp (e.loopClosure true)).comp e.forward ⊆ z.forward

Positive through-edge absorption in a corner.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_through_absorption {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) (positive : Bool) : ((e.through positive).comp (e.loopClosure positive)).comp (z.through positive) ⊆ z.through positive ∧ ((z.through positive).comp (e.loopClosure positive)).comp (e.through positive) ⊆ z.through positive

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.loopClosure_comp_self {m : ℕ} (e : Diagram m) (positive : Bool) : (e.loopClosure positive).comp (e.loopClosure positive) = e.loopClosure positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.loopClosure_comp {m : ℕ} (e : Diagram m) (positive : Bool) (R : SetRel (Fin m) (Fin m)) : (e.loopClosure positive).comp ((e.loopClosure positive).comp R) = (e.loopClosure positive).comp R

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.surviving_absorption {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) (positive : Bool) : (e.recurrence positive).comp (e.surviving z positive) ⊆ e.surviving z positive ∧ (e.surviving z positive).comp (e.recurrence positive) ⊆ e.surviving z positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.recurrence_trans {m : ℕ} (e : Diagram m) (he : e.comp e = e) {positive : Bool} {x y z : Fin m} (hxy : (x, y) ∈ e.recurrence positive) (hyz : (y, z) ∈ e.recurrence positive) : (x, z) ∈ e.recurrence positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.class_nonempty {m : ℕ} {e : Diagram m} {c : Bool × Set (Fin m)} (hc : c ∈ e.classes) : c.2.Nonempty

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.class_related {m : ℕ} (e : Diagram m) (he : e.comp e = e) {c : Bool × Set (Fin m)} (hc : c ∈ e.classes) {x y : Fin m} (hx : x ∈ c.2) (hy : y ∈ c.2) : (x, y) ∈ e.recurrence c.1 ∧ (y, x) ∈ e.recurrence c.1

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.class_eq_of_mem {m : ℕ} (e : Diagram m) (he : e.comp e = e) {c : Bool × Set (Fin m)} (hc : c ∈ e.classes) {x : Fin m} (hx : x ∈ c.2) : c.2 = {y : Fin m | (x, y) ∈ e.recurrence c.1 ∧ (y, x) ∈ e.recurrence c.1}

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.class_eq_of_common {m : ℕ} (e : Diagram m) (he : e.comp e = e) {c d : Bool × Set (Fin m)} (hc : c ∈ e.classes) (hd : d ∈ e.classes) (hsign : c.1 = d.1) {x : Fin m} (hx : x ∈ c.2) (hxd : x ∈ d.2) : c = d

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.surviving_loop_iff {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) {c : Bool × Set (Fin m)} (hc : c ∈ e.classes) {x y : Fin m} (hx : x ∈ c.2) (hy : y ∈ c.2) : (x, x) ∈ e.surviving z c.1 ↔ (y, y) ∈ e.surviving z c.1

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.not_mem_missing_iff {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) {c : Bool × Set (Fin m)} (hc : c ∈ e.classes) {x : Fin m} (hx : x ∈ c.2) : c ∉ e.missing z ↔ (x, x) ∈ e.surviving z c.1

@[simp]

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.missing_self {m : ℕ} (e : Diagram m) : e.missing e = ∅

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.surviving_comp {m : ℕ} (e z w : Diagram m) (hz : z ∈ e.corner) (hw : w ∈ e.corner) (positive : Bool) : (if positive = true then (e.surviving z positive).comp (e.surviving w positive) else (e.surviving w positive).comp (e.surviving z positive)) ⊆ e.surviving (z.comp w) positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.missing_comp {m : ℕ} (e z w : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) (hw : w ∈ e.corner) : e.missing (z.comp w) ⊆ e.missing z ∪ e.missing w

A class can disappear from a product only if it disappears from a factor.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.missing_pow_succ {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) (k : ℕ) : e.missing (z ^ (k + 1)) ⊆ e.missing z

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.class_count {m : ℕ} (e : Diagram m) : e.classes.ncard ≤ 2 * m

There are at most two signed recurrent classes per boundary label.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.through_comp_recurrence {m : ℕ} (e : Diagram m) (he : e.comp e = e) (positive : Bool) : (e.through positive).comp (e.recurrence positive) = (e.through positive).comp (e.loopClosure positive)

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.recurrence_comp_through {m : ℕ} (e : Diagram m) (he : e.comp e = e) (positive : Bool) : (e.recurrence positive).comp (e.through positive) = (e.loopClosure positive).comp (e.through positive)

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.rectangle_subset {m : ℕ} (e : Diagram m) (he : e.comp e = e) (positive : Bool) (p : Fin m) : e.rectangle positive p ⊆ e.through positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.rectangle_eq_of_related {m : ℕ} (e : Diagram m) (he : e.comp e = e) {positive : Bool} {p q : Fin m} (hpq : (p, q) ∈ e.recurrence positive) (hqp : (q, p) ∈ e.recurrence positive) : e.rectangle positive p = e.rectangle positive q

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.rectangle_cover {m : ℕ} (e : Diagram m) (he : e.comp e = e) {positive : Bool} {u v : Fin m} (huv : (u, v) ∈ e.through positive) : ∃ (p : Fin m), (p, p) ∈ e.recurrence positive ∧ (u, v) ∈ e.rectangle positive p

The recurrent rectangles cover every through edge, including for an empty boundary.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.rectangle_survives {m : ℕ} (e z : Diagram m) (hz : z ∈ e.corner) {positive : Bool} {p : Fin m} (hp : (p, p) ∈ e.surviving z positive) : e.rectangle positive p ⊆ z.through positive