Recognition.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TwoWayComplementation.word_diagram_order_reversal line 11

Source documentation

Singleton contexts force reversal of relation inclusion.

theorem word_diagram_order_reversal {H : Type*} {m : ℕ}
    (τ : List (SetRel H H) → Diagram m)
    (hmul : ∀ u v, τ (u ++ v) = Diagram.comp (τ u) (τ v))
    (l r : Diagram m) (a b : Fin m)
    (hlanguage : ∀ w, (a, b) ∈ (Diagram.comp (Diagram.comp l (τ w)) r).forward ↔
      ¬ (relationProduct w).Nonempty)
    {u v : List (SetRel H H)} (huv : (τ u, τ v) ∈ Diagram.inclusion m) :
    relationProduct v ⊆ relationProduct u := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp, OAI.TwoWayComplementation.relationProduct, OAI.TwoWayComplementation.Diagram.inclusion

theorem OAI.TwoWayComplementation.diagram_relation_image line 37

Source documentation

The relation product descends to the diagram image by singleton-context tests.

theorem diagram_relation_image {H : Type*} {m : ℕ}
    (τ : List (SetRel H H) → Diagram m)
    (hzero : τ [] = Diagram.identity m)
    (hmul : ∀ u v, τ (u ++ v) = Diagram.comp (τ u) (τ v))
    (l r : Diagram m) (a b : Fin m)
    (hlanguage : ∀ w, (a, b) ∈ (Diagram.comp (Diagram.comp l (τ w)) r).forward ↔
      ¬ (relationProduct w).Nonempty) :
    ∃ S : Submonoid (Diagram m), ∃ φ : S →* RelationMonoid H,
      Function.Surjective φ ∧
      (∀ z w : S, (z.val, w.val) ∈ Diagram.inclusion m → (φ w).toRel ⊆ (φ z).toRel) := by
…

Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.identity, OAI.TwoWayComplementation.Diagram.comp, OAI.TwoWayComplementation.relationProduct, OAI.TwoWayComplementation.RelationMonoid, OAI.TwoWayComplementation.Diagram.inclusion

theorem OAI.TwoWayComplementation.diagram_recognition_lower_bound line 91

Source documentation

Recognition of relation-product emptiness forces the image theorem's state bound.

theorem diagram_recognition_lower_bound (h m : ℕ) (hh : 2 ≤ h) (hm : 1 ≤ m)
    (τ : List (SetRel (Fin h) (Fin h)) → Diagram m)
    (hzero : τ [] = Diagram.identity m)
    (hmul : ∀ u v, τ (u ++ v) = Diagram.comp (τ u) (τ v))
    (l r : Diagram m) (a b : Fin m)
    (hlanguage : ∀ w, (a, b) ∈ (Diagram.comp (Diagram.comp l (τ w)) r).forward ↔
      ¬ (relationProduct w).Nonempty) : lossBound h ≤ 2 * m := by
…