OAI/Computability/WLIdentification/FiniteRefinement.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.WLIdentification.FiniteRefinement.map_eq_of_kernel line 10

   Source documentation

   Only equality kernels matter; no full color trees need be stored.

   theorem map_eq_of_kernel {A B C : Type} (f : A → B) (g : A → C) (L M : Multiset A)
       (h : ∀ a b, f a = f b → g a = g b) (he : L.map f = M.map f) : L.map g = M.map g := by
   …

2. theorem OAI.WLIdentification.FiniteRefinement.map_eq_iff_kernel line 19
3. def OAI.WLIdentification.FiniteRefinement.KernelEq line 26
4. def OAI.WLIdentification.FiniteRefinement.kernel line 28
5. theorem OAI.WLIdentification.FiniteRefinement.kernel_eq_iff line 31
6. theorem OAI.WLIdentification.FiniteRefinement.kernel_step_subset line 42
7. theorem OAI.WLIdentification.FiniteRefinement.exists_adjacent line 51

   Source documentation

   A descending Boolean relation on N objects must settle by N² rounds. This coarse bound avoids an implicit unit-cost operation on full color names.

   theorem exists_adjacent (h : ∀ s a b, color (s+1) a = color (s+1) b → color s a = color s b) :
       ∃ s ≤ Fintype.card A ^ 2, KernelEq color s (s+1) := by
   …

   Mentions: OAI.WLIdentification.FiniteRefinement.KernelEq

8. theorem OAI.WLIdentification.FiniteRefinement.KernelEq.refl line 73
9. theorem OAI.WLIdentification.FiniteRefinement.KernelEq.symm line 76
10. theorem OAI.WLIdentification.FiniteRefinement.KernelEq.trans line 80
11. theorem OAI.WLIdentification.FiniteRefinement.earlier line 88
12. theorem OAI.WLIdentification.FiniteRefinement.stable_tail line 96
13. theorem OAI.WLIdentification.FiniteRefinement.cutoff line 107

    Source documentation

    The one stored Boolean relation after the explicit cutoff decides equality at every refinement depth, including all later rounds.

    theorem cutoff (a b : A) (s : ℕ) :
        color (Fintype.card A ^ 2) a = color (Fintype.card A ^ 2) b → color s a = color s b := by
    …

14. theorem OAI.WLIdentification.FiniteRefinement.histogram_cutoff line 121
15. theorem OAI.WLIdentification.FiniteRefinement.successor_kernel line 132

    Source documentation

    Equality of replacement-vector histograms is determined by the old kernel, so the same stored relation supports ordinary and joint tuple updates.

    theorem successor_kernel {I : Type} (N : A → Multiset (I → A))
        (hupdate : ∀ s a b, color (s+1) a = color (s+1) b ↔
          color s a = color s b ∧
            (N a).map (fun v i => color s (v i)) = (N b).map (fun v i => color s (v i))) :
        ∀ s t, KernelEq color s t → KernelEq color (s+1) (t+1) := by
    …

    Mentions: OAI.WLIdentification.FiniteRefinement.KernelEq

16. theorem OAI.WLIdentification.FiniteRefinement.successor_kernel_scalar line 148
17. def OAI.WLIdentification.FiniteWL.neighbor line 162
18. def OAI.WLIdentification.FiniteWL.neighbors line 165
19. theorem OAI.WLIdentification.FiniteWL.neighbor_update line 169
20. theorem OAI.WLIdentification.FiniteWL.neighbor_cutoff line 178
21. def OAI.WLIdentification.FiniteWL.tuple line 193
22. def OAI.WLIdentification.FiniteWL.vectors line 197
23. theorem OAI.WLIdentification.FiniteWL.tuple_update line 203
24. theorem OAI.WLIdentification.FiniteWL.tuple_cutoff line 214
25. theorem OAI.WLIdentification.FiniteWL.equivalent_cutoff line 231

    Source documentation

    Explicit finite stopping criteria, retaining neighbor refinement precisely at k=1.

    theorem equivalent_cutoff (G H : Graph) (k : ℕ) :
        Equivalent k G H ↔
          if k = 1 then
            neighborHistogram G ((G.order+H.order)^2) = neighborHistogram H ((G.order+H.order)^2)
          else tupleHistogram G k ((G.order^k+H.order^k)^2) =
            tupleHistogram H k ((G.order^k+H.order^k)^2) := by
    …

    Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.Equivalent, OAI.WLIdentification.neighborHistogram, OAI.WLIdentification.tupleHistogram

26. theorem OAI.WLIdentification.FiniteRefinement.map_eq_iff_counts line 247

    Source documentation

    Image multiset equality is checked by finite class counts; there is no unit-cost comparison of recursively expanded color trees.

    theorem map_eq_iff_counts {A C : Type} [DecidableEq C] (f : A → C) (L M : Multiset A) :
        L.map f = M.map f ↔ ∀ a, L.countP (fun b => f b = f a) = M.countP (fun b => f b = f a) := by
    …

27. def OAI.WLIdentification.FiniteRefinement.vectorMatch line 267
28. def OAI.WLIdentification.FiniteRefinement.tableStep line 270
29. theorem OAI.WLIdentification.FiniteRefinement.tableStep_correct line 277

    Source documentation

    Reusable correctness of a table update, including the joint vector test.

    theorem tableStep_correct {C D : Type} [DecidableEq C] (old : A → C) (next : A → D)
        (N : A → Multiset (I → A)) (R : A → A → Bool)
        (hR : ∀ a b, R a b = true ↔ old a = old b)
        (hnext : ∀ a b, next a = next b ↔ old a = old b ∧
          (N a).map (fun v i => old (v i)) = (N b).map (fun v i => old (v i))) (a b : A) :
        tableStep N R a b = true ↔ next a = next b := by
    …

    Mentions: OAI.WLIdentification.FiniteRefinement.tableStep

30. def OAI.WLIdentification.FiniteRefinement.table line 294

    Source documentation

    Literal finite Boolean relation iteration.

    def table (N : A → Multiset (I → A)) (initial : A → A → Bool) (rounds : ℕ) : A → A → Bool :=
    …

    Mentions: OAI.WLIdentification.initial

31. theorem OAI.WLIdentification.FiniteRefinement.table_correct line 298