OAI/Combinatorics/Automata/Wiring.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.OneWayLiveness.Pairing line 7
2. def OAI.OneWayLiveness.Pairing.mate line 15
3. lemma OAI.OneWayLiveness.Pairing.mate_link line 16
4. lemma OAI.OneWayLiveness.Pairing.eq_mate line 17
5. lemma OAI.OneWayLiveness.Pairing.mate_involutive line 19
6. lemma OAI.OneWayLiveness.Pairing.mate_ne line 22
7. lemma OAI.OneWayLiveness.Pairing.link_iff line 25
8. instance OAI.OneWayLiveness.Pairing.(instance at line 27) line 27
9. def OAI.OneWayLiveness.Pairing.Compatible line 36

   Source documentation

   An assignment obeys all wire equalities.

   def Compatible {C : Type*} (color : P → C) : Prop :=
   …

10. def OAI.OneWayLiveness.Pairing.connected line 40

    Source documentation

    The equivalence relation whose classes are the pairs.

    def connected (x y : P) : Prop := x = y ∨ a.link x y

11. lemma OAI.OneWayLiveness.Pairing.connected_refl line 42
12. lemma OAI.OneWayLiveness.Pairing.connected_symm line 43
13. lemma OAI.OneWayLiveness.Pairing.connected_trans line 47
14. def OAI.OneWayLiveness.Pairing.testColor line 55
15. lemma OAI.OneWayLiveness.Pairing.testColor_self line 59
16. lemma OAI.OneWayLiveness.Pairing.compatible_testColor line 63
17. lemma OAI.OneWayLiveness.Pairing.eq_of_compatible line 76

    Source documentation

    Two-color constraints remember an entire matching, not just rank or connectivity among one side of its ports.

    lemma eq_of_compatible {b : Pairing P}
        (h : ∀ c : P → Bool, a.Compatible c ↔ b.Compatible c) : a = b := by
    …

    Mentions: OAI.OneWayLiveness.Pairing

18. lemma OAI.OneWayLiveness.FiniteWiring.leaves_card_le_two line 102

    Source documentation

    A finite connected graph with degrees at most two has at most two leaves. The proof uses the degree-sum formula and the edge-count bound for a connected graph.

    lemma leaves_card_le_two [DecidableRel G.Adj] (hc : G.Connected) (hd : ∀ v, G.degree v ≤ 2) :
        (Finset.univ.filter fun v => G.degree v = 1).card ≤ 2 := by
    …

19. lemma OAI.OneWayLiveness.FiniteWiring.unique_other_leaf line 123

    Source documentation

    In a finite connected graph of maximum degree two, a leaf has exactly one other leaf.

    lemma unique_other_leaf [DecidableRel G.Adj] (hc : G.Connected) (hd : ∀ v, G.degree v ≤ 2) (x : V) (hx : G.degree x = 1) :
        ∃! y : V, y ≠ x ∧ G.degree y = 1 := by
    …

20. lemma OAI.OneWayLiveness.FiniteWiring.component_degree line 146

    Source documentation

    Passing to a connected component preserves every vertex degree.

    lemma component_degree [DecidableRel G.Adj]
        (C : G.ConnectedComponent) [Fintype C] [DecidableRel C.toSimpleGraph.Adj] (v : C) :
        C.toSimpleGraph.degree v = G.degree v.val := by
    …

21. lemma OAI.OneWayLiveness.FiniteWiring.unique_reachable_leaf line 162

    Source documentation

    Maximum degree two makes the reachable boundary pairing unique, even when other connected components are cycles.

    lemma unique_reachable_leaf [DecidableRel G.Adj]
        (hd : ∀ v, G.degree v ≤ 2) (x : V) (hx : G.degree x = 1) :
        ∃! y : V, y ≠ x ∧ G.degree y = 1 ∧ G.Reachable x y := by
    …

22. def OAI.OneWayLiveness.FiniteWiring.boundaryPairing line 194

    Source documentation

    Contract all path components onto their boundary. The degree assumptions are precisely degree one at the exposed ports and degree zero or two elsewhere. Closed components disappear.

    noncomputable def boundaryPairing {P : Type*} (port : P ↪ V)
        [DecidableRel G.Adj] (hd : ∀ v, G.degree v ≤ 2)
        (hb : ∀ v, G.degree v = 1 ↔ ∃ p, port p = v) : Pairing P where
    …

    Mentions: OAI.OneWayLiveness.Pairing

23. lemma OAI.OneWayLiveness.FiniteWiring.color_eq_of_reachable line 215

    Source documentation

    Edge-compatible colors are constant along any finite path.

    lemma color_eq_of_reachable {C : Type*} (color : V → C)
        (hc : ∀ x y, G.Adj x y → color x = color y) {x y : V}
        (h : G.Reachable x y) : color x = color y := by
    …

24. lemma OAI.OneWayLiveness.FiniteWiring.coloring_extension line 225

    Source documentation

    Every compatible boundary coloring extends through the wiring. This justifies replacing a cell's wiring by its boundary matching.

    lemma coloring_extension {P : Type*} (port : P ↪ V)
        [DecidableRel G.Adj] (hd : ∀ v, G.degree v ≤ 2)
        (hb : ∀ v, G.degree v = 1 ↔ ∃ p, port p = v) (color : P → Bool) :
        (boundaryPairing G port hd hb).Compatible color ↔
          ∃ c : V → Bool, (∀ p, c (port p) = color p) ∧
            ∀ x y, G.Adj x y → c x = c y := by
    …

    Mentions: OAI.OneWayLiveness.FiniteWiring.boundaryPairing

25. def OAI.OneWayLiveness.Pairing.glueAdj line 267
26. def OAI.OneWayLiveness.Pairing.glueGraph line 277

    Source documentation

    Keep the two copies of the interface separate and join them by edges. This subdivision avoids parallel edges without changing boundary paths.

    def glueGraph (a : Pairing (A ⊕ B)) (b : Pairing (B ⊕ C)) : SimpleGraph ((A ⊕ B) ⊕ (B ⊕ C)) where
    …

    Mentions: OAI.OneWayLiveness.Pairing

27. def OAI.OneWayLiveness.Pairing.outer line 291
28. instance OAI.OneWayLiveness.Pairing.glueDec line 299
29. lemma OAI.OneWayLiveness.Pairing.glue_degree_LL line 304
30. lemma OAI.OneWayLiveness.Pairing.glue_degree_RR line 315
31. lemma OAI.OneWayLiveness.Pairing.glue_degree_LR line 326
32. lemma OAI.OneWayLiveness.Pairing.glue_degree_RL line 337
33. lemma OAI.OneWayLiveness.Pairing.glue_degree_le_two line 348
34. lemma OAI.OneWayLiveness.Pairing.glue_boundary line 356
35. def OAI.OneWayLiveness.Pairing.compose line 370
36. lemma OAI.OneWayLiveness.Pairing.compose_compatible line 376

    Source documentation

    Boolean boundary behavior composes as ordinary relational composition.

    lemma compose_compatible (f : A → Bool) (g : C → Bool) :
        (compose a b).Compatible (Sum.elim f g) ↔
          ∃ k : B → Bool, a.Compatible (Sum.elim f k) ∧ b.Compatible (Sum.elim k g) := by
    …

    Mentions: OAI.OneWayLiveness.Pairing.compose, OAI.OneWayLiveness.Pairing.Compatible

37. def OAI.OneWayLiveness.Pairing.ofInvolution line 416
38. def OAI.OneWayLiveness.Pairing.transport line 422
39. def OAI.OneWayLiveness.Pairing.bijection line 437

    Source documentation

    A rectangular permutation diagram; arbitrary equivalences also allow renumbering finite port sets without changing the underlying diagram.

    def bijection (e : A ≃ B) : Pairing (A ⊕ B) :=
    …

    Mentions: OAI.OneWayLiveness.Pairing

40. def OAI.OneWayLiveness.Pairing.identity line 441
41. lemma OAI.OneWayLiveness.Pairing.bijection_compatible line 443
42. lemma OAI.OneWayLiveness.Pairing.identity_compatible line 459
43. lemma OAI.OneWayLiveness.Pairing.ext_colors line 464
44. lemma OAI.OneWayLiveness.Pairing.connected_of_color_eq line 474

    Source documentation

    The Boolean equality semantics is faithful even for a single pair.

    lemma connected_of_color_eq (a : Pairing P) (x y : P)
        (h : ∀ c : P → Bool, a.Compatible c → c x = c y) : a.connected x y := by
    …

    Mentions: OAI.OneWayLiveness.Pairing

45. lemma OAI.OneWayLiveness.Pairing.link_of_color_eq line 480
46. lemma OAI.OneWayLiveness.Pairing.compose_assoc line 486
47. lemma OAI.OneWayLiveness.Pairing.identity_compose line 493
48. lemma OAI.OneWayLiveness.Pairing.compose_identity line 498