Two-way complementation: transport

Adapted from OpenAI's formalization at revision adc7f1241b42e322a6451854ab7e4b4c146bf78a. Source: https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/OAI/Combinatorics/TwoWayAutomata/Transport.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.inclusion_of_missing_empty {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) (hmissing : e.missing z = ∅) : (e, z) ∈ inclusion m

Losing no recurrent class forces componentwise inclusion.

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classRectangle_subset {m : ℕ} (e : Diagram m) (he : e.comp e = e) (C : Bool × Set (Fin m)) : e.classRectangle C ⊆ e.portRelation

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classRectangle_cross {m : ℕ} (e : Diagram m) (he : e.comp e = e) {C : Bool × Set (Fin m)} (hC : C ∈ e.classes) {a b c d : Bool × Fin m} (hab : (a, b) ∈ e.classRectangle C) (hcd : (c, d) ∈ e.classRectangle C) : (a, d) ∈ e.classRectangle C

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classRectangle_survives {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) {C : Bool × Set (Fin m)} (hC : C ∈ e.classes) (hmissing : C ∉ e.missing z) : e.classRectangle C ⊆ z.portRelation

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.portRelation_covered {m : ℕ} (e z : Diagram m) (he : e.comp e = e) (hz : z ∈ e.corner) {a b : Bool × Fin m} (hab : (a, b) ∈ e.portRelation) : (a, b) ∈ z.portRelation ∨ ∃ C ∈ e.missing z, (a, b) ∈ e.classRectangle C

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classInfluence_cross {m : ℕ} (e d u v : Diagram m) (he : e.comp e = e) (positive : Bool) {C : Bool × Set (Fin m)} (hC : C ∈ e.classes) {a b c f : Fin m} (hab : (a, b) ∈ e.classInfluence d u v positive C) (hcf : (c, f) ∈ e.classInfluence d u v positive C) : (a, f) ∈ e.classInfluence d u v positive C

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.classInfluence_subset {m : ℕ} (e d u v : Diagram m) (he : e.comp e = e) (hcontext : (u.comp e).comp v = d) (positive : Bool) (C : Bool × Set (Fin m)) : e.classInfluence d u v positive C ⊆ d.recurrence positive

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.transportMarked_card {m : ℕ} (e d u v : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hcontext : (u.comp e).comp v = d) (J : Set (Bool × Set (Fin m))) (hJ : J ⊆ e.classes) : (e.transportMarked d u v J).ncard ≤ 2 * J.ncard

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.missing_context_subset_marked {m : ℕ} (e d u v z : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hcontext : (u.comp e).comp v = d) (hz : z ∈ e.corner) (J : Set (Bool × Set (Fin m))) (hJz : e.missing z ⊆ J) : d.missing ((u.comp z).comp v) ⊆ e.transportMarked d u v J

theorem Complexity.FiniteAutomaton.Complementation.Internal.Diagram.transport {m : ℕ} (e d u v : Diagram m) (he : e.comp e = e) (hd : d.comp d = d) (hcontext : (u.comp e).comp v = d) (J : Set (Bool × Set (Fin m))) (hJ : J ⊆ e.classes) : ∃ J' ⊆ d.classes, J'.ncard ≤ 2 * J.ncard ∧ ∀ z ∈ e.corner, e.missing z ⊆ J → (u.comp z).comp v ∈ d.corner → d.missing ((u.comp z).comp v) ⊆ J'

One fixed target set covers every admissible replacement.