OAI/Computability/WLIdentification/Refinement.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WLIdentification.exists_colorEquiv line 8

   Source documentation

   Equality of finite color histograms admits a color-preserving bijection.

   theorem exists_colorEquiv {α β γ : Type} [Fintype α] [Fintype β]
       (f : α → γ) (g : β → γ)
       (h : Finset.univ.val.map f = Finset.univ.val.map g) :
       ∃ e : α ≃ β, ∀ a, f a = g (e a) := by
   …

2. theorem OAI.WLIdentification.tupleRound_bijection line 26

   Source documentation

   A round witness is a bijection on the entire tuple table.

   theorem tupleRound_bijection {G H : Graph} {k s : ℕ}
       (h : tupleHistogram G k s = tupleHistogram H k s) :
       ∃ e : (Fin k → Fin G.order) ≃ (Fin k → Fin H.order),
         ∀ v, tupleColor G k s v = tupleColor H k s (e v) :=
   …

   Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleHistogram, OAI.WLIdentification.tupleColor

3. def OAI.WLIdentification.degree line 32
4. def OAI.WLIdentification.degreeOfColor line 36

   Source documentation

   Degree is already recoverable from a joint-update round, with two distinct slots.

   def degreeOfColor {k : ℕ} (i j : Fin k) (c : TupleColor k 1) : ℕ :=
   …

   Mentions: OAI.WLIdentification.TupleColor

5. theorem OAI.WLIdentification.degreeOfColor_tuple line 40
6. theorem OAI.WLIdentification.round_one_local line 56

   Source documentation

   Equal one-round tuple colors preserve adjacency, equality and the degrees of its slots.

   theorem round_one_local {G H : Graph} {k : ℕ} (hk : 2 ≤ k)
       {v : Fin k → Fin G.order} {w : Fin k → Fin H.order}
       (h : tupleColor G k 1 v = tupleColor H k 1 w) :
       (∀ i j, v i = v j ↔ w i = w j) ∧
       (∀ i j, G.edge (v i) (v j) = H.edge (w i) (w j)) ∧
       (∀ i, degree G (v i) = degree H (w i)) := by
   …

   Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleColor, OAI.WLIdentification.degree

7. def OAI.WLIdentification.diagonalEquiv line 84
8. theorem OAI.WLIdentification.round_one_degreeBijection line 95

   Source documentation

   Matching diagonal tuples yields exactly a degree-preserving vertex bijection.

   theorem round_one_degreeBijection {G H : Graph} {k : ℕ} (hk : 2 ≤ k)
       (h : tupleHistogram G k 1 = tupleHistogram H k 1) :
       ∃ e : Fin G.order ≃ Fin H.order, ∀ v, degree G v = degree H (e v) := by
   …

   Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleHistogram, OAI.WLIdentification.degree

9. theorem OAI.WLIdentification.equivalent_degreeBijection line 112

   Source documentation

   The needed local reconstruction information follows from the literal r-WL definition.

   theorem equivalent_degreeBijection {G H : Graph} {k : ℕ} (hk : 2 ≤ k)
       (h : Equivalent k G H) :
       ∃ e : Fin G.order ≃ Fin H.order, ∀ v, degree G v = degree H (e v) := by
   …

   Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.degree

10. theorem OAI.WLIdentification.equivalent_local_match line 121

    Source documentation

    Any at most k distinguished vertices have a simultaneous degree-and-incidence match. This is enough to recover a whole bounded-size incidence piece, not just one valuation.

    theorem equivalent_local_match {G H : Graph} {k m : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k G H) (hm : m ≤ k) (hm0 : 0 < m) (v : Fin m → Fin G.order) :
        ∃ w : Fin m → Fin H.order,
          (∀ i j, v i = v j ↔ w i = w j) ∧
          (∀ i j, G.edge (v i) (v j) = H.edge (w i) (w j)) ∧
          (∀ i, degree G (v i) = degree H (w i)) := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.degree

11. theorem OAI.WLIdentification.round_two_neighborBijection line 144

    Source documentation

    A second joint round gives a single vertex bijection preserving adjacency to any distinguished slot and the degrees of all possible next vertices.

    theorem round_two_neighborBijection {G H : Graph} {k : ℕ} (hk : 2 ≤ k)
        {v : Fin k → Fin G.order} {w : Fin k → Fin H.order}
        (h : tupleColor G k 2 v = tupleColor H k 2 w) (i : Fin k) :
        ∃ e : Fin G.order ≃ Fin H.order, ∀ z,
          G.edge (v i) z = H.edge (w i) (e z) ∧ degree G z = degree H (e z) := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.tupleColor, OAI.WLIdentification.degree

12. def OAI.WLIdentification.degreeNeighbors line 171
13. theorem OAI.WLIdentification.round_two_degreeNeighbors line 174
14. theorem OAI.WLIdentification.equivalent_symm line 183
15. theorem OAI.WLIdentification.equivalent_local_neighborhood_match line 190

    Source documentation

    In particular private-leaf counts, rather than just total degrees, are preserved by a simultaneous local match in every equivalent mate.

    theorem equivalent_local_neighborhood_match {G H : Graph} {k m : ℕ} (hk : 2 ≤ k)
        (h : Equivalent k G H) (hm : m ≤ k) (hm0 : 0 < m) (v : Fin m → Fin G.order) :
        ∃ w : Fin m → Fin H.order,
          (∀ i j, v i = v j ↔ w i = w j) ∧
          (∀ i j, G.edge (v i) (v j) = H.edge (w i) (w j)) ∧
          (∀ i, degree G (v i) = degree H (w i)) ∧
          (∀ i d, degreeNeighbors G (v i) d = degreeNeighbors H (w i) d) := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.degree, OAI.WLIdentification.degreeNeighbors