OAI/Computability/WLIdentification/MateReconstruction.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WLIdentification.histogram_eq_of_equiv line 7
2. theorem OAI.WLIdentification.filteredHistogram_eq_of_equiv line 13
3. theorem OAI.WLIdentification.isomorphic_refl line 23
4. theorem OAI.WLIdentification.isomorphic_symm line 25
5. theorem OAI.WLIdentification.isomorphic_trans line 31
6. theorem OAI.WLIdentification.neighborColor_isomorphic line 37
7. theorem OAI.WLIdentification.tupleColor_isomorphic line 48
8. theorem OAI.WLIdentification.isomorphic_equivalent line 66
9. theorem OAI.WLIdentification.equivalent_trans line 76
10. def OAI.WLIdentification.simpleOfGraph line 81
11. instance OAI.WLIdentification.simpleOfGraph_decidable line 86
12. theorem OAI.WLIdentification.graph_simple_isomorphic line 89
13. theorem OAI.WLIdentification.simpleOfGraph_degree line 97
14. theorem OAI.WLIdentification.degree_one_neighbors_eq line 106

    Source documentation

    A degree-one vertex has the same unique neighbor in every incident edge.

    theorem degree_one_neighbors_eq {V : Type} [Fintype V] (G : SimpleGraph V)
        [DecidableRel G.Adj] {v x y : V} (hd : G.degree v = 1)
        (hx : G.Adj v x) (hy : G.Adj v y) : x = y := by
    …

15. theorem OAI.WLIdentification.private_leaf_reconstruction line 114

    Source documentation

    Private-leaf reconstruction by exact finite counting. The prescribed leaf counts exhaust all leaf vertices; no separate leaf-only component can remain.

    theorem private_leaf_reconstruction {V : Type} [Fintype V] (ell : V → ℕ)
        (H : SimpleGraph (LeafVertex ell)) [DecidableRel H.Adj]
        (hleaf : ∀ (v : V) (j : Fin (ell v)), H.degree (.inr ⟨v, j⟩) = 1)
        (hcount : ∀ v, Fintype.card {l : Σ v, Fin (ell v) // H.Adj (.inl v) (.inr l)} = ell v) :
        ∃ e : withLeaves (H.comap Sum.inl) ell ≃g H, ∀ v, e (.inl v) = .inl v := by
    …

    Mentions: OAI.WLIdentification.LeafVertex, OAI.WLIdentification.withLeaves

16. def OAI.WLIdentification.simpleDegreeNeighbors line 161
17. theorem OAI.WLIdentification.graphOfSimple_degree_at line 166
18. theorem OAI.WLIdentification.graphOfSimple_degreeNeighbors line 173
19. theorem OAI.WLIdentification.simple_equivalent_local line 187

    Source documentation

    Transfer the literal WL local information to any finite graph vertex types.

    theorem simple_equivalent_local {V W : Type} [Fintype V] [Fintype W]
        (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
        {k m : ℕ} (hk : 2 ≤ k) (h : Equivalent k (graphOfSimple G) (graphOfSimple H))
        (hm : m ≤ k) (hm0 : 0 < m) (v : Fin m → V) :
        ∃ w : Fin m → W,
          (∀ i j, v i = v j ↔ w i = w j) ∧
          (∀ i j, G.Adj (v i) (v j) ↔ H.Adj (w i) (w j)) ∧
          (∀ i, G.degree (v i) = H.degree (w i)) ∧
          (∀ i d, simpleDegreeNeighbors G (v i) d = simpleDegreeNeighbors H (w i) d) := by
    …

    Mentions: OAI.WLIdentification.Equivalent, OAI.WLIdentification.graphOfSimple, OAI.WLIdentification.simpleDegreeNeighbors

20. theorem OAI.WLIdentification.simple_equivalent_local_finite line 221
21. theorem OAI.WLIdentification.simple_equivalent_degreeBijection line 245

    Source documentation

    The diagonal-tuple degree bijection is independent of the chosen finite encoding.

    theorem simple_equivalent_degreeBijection {V W : Type} [Fintype V] [Fintype W]
        (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
        {k : ℕ} (hk : 2 ≤ k) (h : Equivalent k (graphOfSimple G) (graphOfSimple H)) :
        ∃ e : V ≃ W, ∀ v, G.degree v = H.degree (e v) := by
    …

    Mentions: OAI.WLIdentification.Equivalent, OAI.WLIdentification.graphOfSimple

22. theorem OAI.WLIdentification.leaf_count_eq_degreeNeighbors line 256
23. theorem OAI.WLIdentification.tagged_degreeNeighbors_one line 280
24. theorem OAI.WLIdentification.tagged_arbitrary_mate line 301

    Source documentation

    An arbitrary WL mate of a leaf-coded graph has exactly the same leaf-coded shape. This theorem quantifies over all finite mate graphs, with no gadget promise.

    theorem tagged_arbitrary_mate {V W : Type} [Fintype V] [Fintype W]
        (G : SimpleGraph V) (H : SimpleGraph W) [DecidableRel G.Adj] [DecidableRel H.Adj]
        (color : V → ℕ) (hc : ∀ v, 0 < color v) {k : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k (taggedGraph G color) (graphOfSimple H)) :
        ∃ G' : SimpleGraph V, Nonempty (withLeaves G' (tagSize color) ≃g H) := by
    …

    Mentions: OAI.WLIdentification.Equivalent, OAI.WLIdentification.taggedGraph, OAI.WLIdentification.graphOfSimple, OAI.WLIdentification.withLeaves, OAI.WLIdentification.tagSize

25. theorem OAI.WLIdentification.tagged_equivalent_local line 346

    Source documentation

    A bounded set of base vertices of equivalent tagged graphs has a simultaneous color-preserving induced-graph match. Degree coding recovers the original colors.

    theorem tagged_equivalent_local {A V W : Type} [Fintype A] [Nonempty A]
        [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)
        (hN : Fintype.card V = Fintype.card W) {k : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k (taggedGraph G color) (taggedGraph H color'))
        (hA : Fintype.card A ≤ k) (v : A → V) :
        ∃ w : A → W, (∀ i j, v i = v j ↔ w i = w j) ∧
          (∀ i j, G.Adj (v i) (v j) ↔ H.Adj (w i) (w j)) ∧
          (∀ i, color (v i) = color' (w i)) := by
    …

    Mentions: OAI.WLIdentification.Equivalent, OAI.WLIdentification.taggedGraph

26. def OAI.WLIdentification.AffineBlocks.AllowedName line 384
27. theorem OAI.WLIdentification.AffineBlocks.allowed_name line 390
28. theorem OAI.WLIdentification.AffineBlocks.piece_contains_color line 394
29. theorem OAI.WLIdentification.AffineBlocks.tagged_equivalent_allowed line 409

    Source documentation

    Bounded local WL information excludes every edge between forbidden colors.

    theorem tagged_equivalent_allowed (D : AffineBlocks C B) (H : SimpleGraph (D.Vertex 0))
        [DecidableRel H.Adj] {k : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k (D.graph 0) (taggedGraph H D.colorNat)) :
        ∀ x y, H.Adj x y → D.Allowed x y := by
    …

    Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Equivalent, OAI.WLIdentification.taggedGraph

30. theorem OAI.WLIdentification.AffineBlocks.tagged_equivalent_piece line 430

    Source documentation

    Match a complete incidence piece at once. Finite cardinality upgrades the injective local match into an isomorphism of the entire piece.

    theorem tagged_equivalent_piece (D : AffineBlocks C B) (H : SimpleGraph (D.Vertex 0))
        [DecidableRel H.Adj] {k : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k (D.graph 0) (taggedGraph H D.colorNat)) (b : B)
        (hb : Fintype.card (D.Piece 0 b) ≤ k) :
        ∃ e : D.pieceGraph 0 b ≃g H.comap (D.pieceEmbed b),
          ∀ v, D.colorName (D.pieceEmbed b (e v)) = D.colorName (D.pieceEmbed b v) := by
    …

    Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Equivalent, OAI.WLIdentification.taggedGraph

31. theorem OAI.WLIdentification.AffineBlocks.graph_arbitrary_mate line 462

    Source documentation

    Full arbitrary-mate reconstruction, not pair-equivalence hardness: every finite uncolored WL mate is isomorphic to some affine shift of the same system.

    theorem graph_arbitrary_mate (D : AffineBlocks C B) {k : ℕ} (hk : 2 ≤ k)
        (hbound : ∀ b, Fintype.card (D.Piece 0 b) ≤ k) (H : Graph)
        (h : Equivalent k (D.graph 0) H) :
        ∃ beta : B → Bit, Isomorphic H (D.graph beta) := by
    …

    Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.Bit, OAI.WLIdentification.Isomorphic