Two-way complementation: nesting

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Nesting.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.loopClosure_subset_of_corner {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner) (positive : Bool) : e.loopClosure positive ⊆ d.loopClosure positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_forward_loop_absorption {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner) : (e.forward.comp (d.loopClosure true)).comp d.forward ⊆ (d.loopClosure true).comp d.forward ∧ (d.forward.comp (d.loopClosure true)).comp e.forward ⊆ d.forward.comp (d.loopClosure true)

Two finite-path rearrangements for absorption under nesting.

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

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_through_absorption {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner) (positive : Bool) : (e.through positive).comp (d.recurrence positive) ⊆ d.recurrence positive ∧ (d.recurrence positive).comp (e.through positive) ⊆ d.recurrence positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_recurrence_absorption {m : ℕ} (e d : Diagram m) (hd : d ∈ e.corner) (positive : Bool) : (e.recurrence positive).comp (d.recurrence positive) ⊆ d.recurrence positive ∧ (d.recurrence positive).comp (e.recurrence positive) ⊆ d.recurrence positive

Mixed recurrent relations are absorbed under nesting.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_forward_factor {m : ℕ} (e d : Diagram m) (he : e.comp e = e) (hd : d ∈ e.corner) {u v : Fin m} (huv : (u, v) ∈ d.forward) : ∃ (p : Fin m) (q : Fin m), (p, p) ∈ e.recurrence true ∧ (q, q) ∈ e.recurrence true ∧ (u, p) ∈ e.forward.comp (e.loopClosure true) ∧ (p, q) ∈ e.surviving d true ∧ (q, v) ∈ (e.loopClosure true).comp e.forward

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.corner_through_factor {m : ℕ} (e d : Diagram m) (he : e.comp e = e) (hd : d ∈ e.corner) {positive : Bool} {u v : Fin m} (huv : (u, v) ∈ d.through positive) : ∃ (p : Fin m) (q : Fin m), (p, p) ∈ e.recurrence positive ∧ (q, q) ∈ e.recurrence positive ∧ (u, p) ∈ (e.through positive).comp (e.loopClosure positive) ∧ (p, q) ∈ e.surviving d positive ∧ (q, v) ∈ (e.loopClosure positive).comp (e.through positive)

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_recurrent_witness {m : ℕ} (e d : Diagram m) (he : e.comp e = e) (hd : d ∈ e.corner) {positive : Bool} {x : Fin m} (hxx : (x, x) ∈ d.recurrence positive) : ∃ (p : Fin m) (q : Fin m), (p, p) ∈ e.recurrence positive ∧ (q, q) ∈ e.recurrence positive ∧ (x, p) ∈ d.recurrence positive ∧ (p, x) ∈ d.recurrence positive ∧ (x, q) ∈ d.recurrence positive ∧ (q, x) ∈ d.recurrence positive ∧ (p, q) ∈ e.surviving d positive

A recurrent loop in a nested corner contains two recurrent points of its parent.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_class_containment {m : ℕ} (e d : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hde : d ∈ e.corner) {c : Bool × Set (Fin m)} (hc : c ∈ d.classes) : (∃ C ∈ e.classes, C.1 = c.1 ∧ C.2 ⊆ c.2 ∧ C ∉ e.missing d) ∨ ∃ C ∈ e.classes, ∃ D ∈ e.classes, C ≠ D ∧ C.1 = c.1 ∧ D.1 = c.1 ∧ C.2 ⊆ c.2 ∧ D.2 ⊆ c.2

A new class contains a surviving old class or two distinct old classes.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_unprotected_loss {m : ℕ} (e d : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hde : d ∈ e.corner) (P : Set (Bool × Fin m)) (hmissing : e.missing d ⊆ e.unprotected P) : 2 * (d.unprotected P).ncard + (e.missing d).ncard ≤ 2 * (e.unprotected P).ncard

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.nested_chain_bound {m k : ℕ} (b : ℕ → Diagram m) (hidemp : ∀ j ≤ k, (b j).comp (b j) = b j) (hnest : ∀ j < k, (b (j + 1), b j) ∈ nesting m) (J : Set (Bool × Set (Fin m))) (hJ : ∀ j ≤ k, (b 0).missing (b j) ⊆ J) : ∑ j ∈ Finset.range k, ((b j).missing (b (j + 1))).ncard ≤ 2 * J.ncard

A common initial missing set pays for all later losses.