BijectionGames.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

structure OAI.WLIdentification.BijectionSystem line 9
Source documentation
A finite-slot bijective extension system. The extra slot is genuine: a k-tuple is extended before any one of its slots is discarded.
```
structure BijectionSystem (G H : Graph) (K : ℕ) where
…
```
Mentions: OAI.WLIdentification.Graph

theorem OAI.WLIdentification.BijectionSystem.replace line 25

Source documentation

Deleting a slot after an extension simultaneously preserves every possible replacement, as required by the joint (not independent-marginal) WL update.

theorem replace {G H : Graph} {K m : ℕ} (S : BijectionSystem G H K)
    {v : Fin m → Fin G.order} {w : Fin m → Fin H.order}
    {z : Fin G.order} {z' : Fin H.order}
    (h : S.relates (m + 1) (Fin.snoc v z) (Fin.snoc w z')) (i : Fin m) :
    S.relates m (Function.update v i z) (Function.update w i z') := by
…

Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.BijectionSystem

theorem OAI.WLIdentification.BijectionSystem.tupleColor_eq line 44
Source documentation
Every maintained tuple has equal colors at every actual finite joint round.
```
theorem tupleColor_eq {G H : Graph} {K k : ℕ} (S : BijectionSystem G H K)
    (hk : k < K) {v : Fin k → Fin G.order} {w : Fin k → Fin H.order}
    (h : S.relates k v w) (round : ℕ) : tupleColor G k round v = tupleColor H k round w := by
…
```
Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.BijectionSystem, OAI.WLIdentification.tupleColor
def OAI.WLIdentification.BijectionSystem.tupleSnocEquiv line 63
theorem OAI.WLIdentification.BijectionSystem.tupleBijection line 71
Source documentation
Sequentially chosen vertex bijections give a bijection of all ordered tuples; there is no unsupported inference from mere existence of a mate for each tuple.
```
theorem tupleBijection {G H : Graph} {K : ℕ} (S : BijectionSystem G H K)
    (m : ℕ) (hm : m ≤ K) :
    ∃ E : (Fin m → Fin G.order) ≃ (Fin m → Fin H.order), ∀ v, S.relates m v (E v) := by
…
```
Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.BijectionSystem
theorem OAI.WLIdentification.BijectionSystem.equivalent line 92
Source documentation
A genuine k+1-slot system proves equivalence for the literal joint k-WL colors.
```
theorem equivalent {G H : Graph} {K k : ℕ} (S : BijectionSystem G H K)
    (hk : 2 ≤ k) (hkK : k < K) : Equivalent k G H := by
…
```
Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.BijectionSystem, OAI.WLIdentification.Equivalent

theorem OAI.WLIdentification.finite_descending_choice line 102

Source documentation

Finite descending choice, used only for actual finite vertex/tuple bijections.

theorem finite_descending_choice {A : Type} [Fintype A]
    (P : ℕ → A → Prop) (hm : ∀ n a, P (n + 1) a → P n a)
    (he : ∀ n, ∃ a, P n a) : ∃ a, ∀ n, P n a := by
…

def OAI.WLIdentification.StableTuple line 119
theorem OAI.WLIdentification.stableTuple_exists line 122
theorem OAI.WLIdentification.stableTuple_extension line 135
Source documentation
Stable joint colors supply one permanent finite vertex bijection for all replacement coordinates and all refinement rounds, not a separate round choice.
```
theorem stableTuple_extension {G H : Graph} {k : ℕ}
    {v : Fin k → Fin G.order} {w : Fin k → Fin H.order} (h : StableTuple k v w) :
    ∃ e : Fin G.order ≃ Fin H.order, ∀ z i,
      StableTuple k (Function.update v i z) (Function.update w i (e z)) := by
…
```
Mentions: OAI.WLIdentification.Graph, OAI.WLIdentification.StableTuple

theorem OAI.WLIdentification.stableTuple_extension_local line 156

Source documentation

Such an extension fixes all currently paired vertices and preserves adjacency to every current slot, as can be tested in a different replacement coordinate.

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

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