Diagram.lean`

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.TwoWayComplementation.Diagram line 11
Source documentation
Four boundary relations; the direction distinguishes the two copies of Fin m.
```
structure Diagram (m : ℕ) where
…
```
def OAI.TwoWayComplementation.Diagram.comp line 24
Source documentation
Composition of boundary diagrams in path order.
```
def comp {m : ℕ} (a b : Diagram m) : Diagram m where
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.identity line 31
Source documentation
Identity boundary diagram.
```
def identity (m : ℕ) : Diagram m := ⟨SetRel.id, SetRel.id, ∅, ∅⟩
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.inclusion line 34
Source documentation
Componentwise edge inclusion, as a relation on diagrams.
```
def inclusion (m : ℕ) : SetRel (Diagram m) (Diagram m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
theorem OAI.TwoWayComplementation.Diagram.inclusion_refl line 38
def OAI.TwoWayComplementation.Diagram.reflect line 42
Source documentation
Reflection reverses the order of multiplication.
```
def reflect {m : ℕ} (a : Diagram m) : Diagram m :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.through line 46
Source documentation
true denotes the positive sign; false denotes the negative sign.
```
def through {m : ℕ} (a : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.loopClosure line 50
Source documentation
Closure of alternating returns at a boundary.
```
def loopClosure {m : ℕ} (e : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.recurrence line 54
Source documentation
The recurrent relation obtained by closing through traversals.
```
def recurrence {m : ℕ} (e : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.classes line 58
Source documentation
Signed recurrent equivalence classes of an idempotent diagram.
```
def classes {m : ℕ} (e : Diagram m) : Set (Bool × Set (Fin m)) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.corner line 63
Source documentation
The corner membership equations for an idempotent e.
```
def corner {m : ℕ} (e : Diagram m) : Set (Diagram m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.nesting line 67
Source documentation
Nesting of idempotents; distinct from edge inclusion.
```
def nesting (m : ℕ) : SetRel (Diagram m) (Diagram m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.surviving line 71
Source documentation
The surviving through relation U relative to e.
```
def surviving {m : ℕ} (e z : Diagram m) (positive : Bool) : SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.missing line 75
Source documentation
Classes whose recurrent loops are absent after replacement by z.
```
def missing {m : ℕ} (e z : Diagram m) : Set (Bool × Set (Fin m)) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.unprotected line 79
Source documentation
Classes containing none of a fixed set of signed protected labels.
```
def unprotected {m : ℕ} (e : Diagram m) (P : Set (Bool × Fin m)) : Set (Bool × Set (Fin m)) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.rectangle line 83
Source documentation
Rectangle associated with a recurrent representative.
```
def rectangle {m : ℕ} (e : Diagram m) (positive : Bool) (p : Fin m) :
    SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.portRelation line 89
Source documentation
Boundary ports: false is left and true is right.
```
def portRelation {m : ℕ} (e : Diagram m) : SetRel (Bool × Fin m) (Bool × Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.bounceRelation line 97
Source documentation
Returns from an exit port through the surrounding left or right context.
```
def bounceRelation {m : ℕ} (R L : SetRel (Fin m) (Fin m)) :
    SetRel (Bool × Fin m) (Bool × Fin m) :=
…
```
def OAI.TwoWayComplementation.Diagram.feedback line 102
Source documentation
A middle traversal followed by any finite number of context returns and traversals.
```
def feedback {m : ℕ} (e : Diagram m) (R L : SetRel (Fin m) (Fin m)) :
    SetRel (Bool × Fin m) (Bool × Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
theorem OAI.TwoWayComplementation.Diagram.mem_port_through line 106
def OAI.TwoWayComplementation.Diagram.classRectangle line 111
Source documentation
The rectangular port edges belonging to a signed recurrent class.
```
def classRectangle {m : ℕ} (e : Diagram m) (C : Bool × Set (Fin m)) :
    SetRel (Bool × Fin m) (Bool × Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.contextEntry line 117
Source documentation
Initial traversal of the outer context, including recurrence closure.
```
def contextEntry {m : ℕ} (d u v : Diagram m) (positive : Bool) :
    SetRel (Fin m) (Bool × Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.contextExit line 124
Source documentation
Final traversal of the outer context, including recurrence closure.
```
def contextExit {m : ℕ} (d u v : Diagram m) (positive : Bool) :
    SetRel (Bool × Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.classInfluence line 131
Source documentation
Traversals with one designated occurrence of a recurrent rectangle in the middle factor.
```
def classInfluence {m : ℕ} (e d u v : Diagram m) (positive : Bool)
    (C : Bool × Set (Fin m)) : SetRel (Fin m) (Fin m) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
def OAI.TwoWayComplementation.Diagram.transportMarked line 138
Source documentation
Target classes whose original traversals can use a rectangle from the fixed set J.
```
def transportMarked {m : ℕ} (e d u v : Diagram m) (J : Set (Bool × Set (Fin m))) :
    Set (Bool × Set (Fin m)) :=
…
```
Mentions: OAI.TwoWayComplementation.Diagram
theorem OAI.TwoWayComplementation.Diagram.feedback_forward line 142
theorem OAI.TwoWayComplementation.Diagram.identity_comp line 204
theorem OAI.TwoWayComplementation.Diagram.comp_identity line 209
theorem OAI.TwoWayComplementation.Diagram.reflect_comp line 213
theorem OAI.TwoWayComplementation.Diagram.feedback_reflect_map line 225
theorem OAI.TwoWayComplementation.Diagram.mem_feedback_reflect line 246
theorem OAI.TwoWayComplementation.Diagram.comp_assoc_forward line 255
theorem OAI.TwoWayComplementation.Diagram.comp_assoc_left line 262
theorem OAI.TwoWayComplementation.Diagram.comp_assoc line 270
Source documentation
The product of boundary diagrams is associative.
```
theorem comp_assoc {m : ℕ} (a b c : Diagram m) :
    comp (comp a b) c = comp a (comp b c) := by
…
```
Mentions: OAI.TwoWayComplementation.Diagram, OAI.TwoWayComplementation.Diagram.comp
theorem OAI.TwoWayComplementation.Diagram.context_forward_iff line 282
theorem OAI.TwoWayComplementation.Diagram.context_through_iff line 289
theorem OAI.TwoWayComplementation.Diagram.context_surviving line 304
instance OAI.TwoWayComplementation.Diagram.(instance at line 320) line 320
theorem OAI.TwoWayComplementation.Diagram.finite_diagram line 328