OAI/Computability/WLIdentification/PrivateLeaves.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.WLIdentification.graphOfSimple line 7
2. theorem OAI.WLIdentification.graphOfSimple_edge line 16
3. theorem OAI.WLIdentification.graphOfSimple_degree line 23
4. abbrev OAI.WLIdentification.LeafVertex line 35
5. def OAI.WLIdentification.withLeaves line 37
6. instance OAI.WLIdentification.withLeaves_decidable line 50
7. def OAI.WLIdentification.baseNeighborEquiv line 53
8. theorem OAI.WLIdentification.withLeaves_base_degree line 79
9. theorem OAI.WLIdentification.withLeaves_leaf_degree line 88
10. def OAI.WLIdentification.tagSize line 99
11. def OAI.WLIdentification.taggedGraph line 102
12. theorem OAI.WLIdentification.tag_degree_color line 106

    Source documentation

    The color is recovered literally by the indicated disjoint degree intervals.

    theorem tag_degree_color {V : Type} [Fintype V] (G : SimpleGraph V)
        [DecidableRel G.Adj] (color : V → ℕ) (v : V) :
        (withLeaves G (tagSize color)).degree (.inl v) / (Fintype.card V + 1) = color v := by
    …

    Mentions: OAI.WLIdentification.withLeaves, OAI.WLIdentification.tagSize, OAI.WLIdentification.degree

13. theorem OAI.WLIdentification.tag_base_degree_gt_one line 114
14. def OAI.WLIdentification.withLeavesIso line 123

    Source documentation

    Color-preserving base isomorphisms extend to all private leaves.

    def withLeavesIso {V W : Type} {G : SimpleGraph V} {H : SimpleGraph W}
        (e : G ≃g H) (ell : V → ℕ) (ell' : W → ℕ) (hell : ∀ v, ell v = ell' (e v)) :
        withLeaves G ell ≃g withLeaves H ell' where
    …

    Mentions: OAI.WLIdentification.withLeaves

15. def OAI.WLIdentification.baseDegreeEquiv line 137
16. theorem OAI.WLIdentification.taggedIso_iff line 159

    Source documentation

    The leaf gadget really erases colors: uncolored isomorphism forces one color-preserving base isomorphism, not a separate choice in each block.

    theorem taggedIso_iff {V W : Type} [Fintype V] [Fintype W]
        (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
        (color : V → ℕ) (color' : W → ℕ)
        (hc : ∀ v, 0 < color v) (hc' : ∀ w, 0 < color' w)
        (hN : Fintype.card V = Fintype.card W) :
        Nonempty (withLeaves G (tagSize color) ≃g withLeaves H (tagSize color')) ↔
          ∃ e : G ≃g H, ∀ v, color v = color' (e v) := by
    …

    Mentions: OAI.WLIdentification.withLeaves, OAI.WLIdentification.tagSize

17. theorem OAI.WLIdentification.isomorphic_graphOfSimple_iff line 199