OAI/Computability/WLIdentification/AffineTranslations.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.WLIdentification.AffineBlocks.OffsetFamily line 11
2. structure OAI.WLIdentification.AffineBlocks.OwnedTranslations line 21

   Source documentation

   Purely local interfaces for the actual affine vertex translations. The piecewise field is a bijection on vertices, not an asserted game strategy.

   structure OwnedTranslations (D : AffineBlocks C B) (beta : B → Bit)
       {V W : Type} (G : SimpleGraph V) (H : SimpleGraph W) where
   …

   Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit

3. def OAI.WLIdentification.AffineBlocks.OwnedTranslations.bijectionSystem line 40

   Source documentation

   Combining independently selected owner bijections gives one announced vertex bijection before the next vertex is selected.

   noncomputable def bijectionSystem (T : OwnedTranslations D beta G H)
       {K : ℕ} (F : OffsetFamily D beta K) :
       BijectionSystem (graphOfSimple G) (graphOfSimple H) K := by
   …

   Mentions: OAI.WLIdentification.AffineBlocks.OwnedTranslations, OAI.WLIdentification.AffineBlocks.OffsetFamily, OAI.WLIdentification.BijectionSystem, OAI.WLIdentification.graphOfSimple

4. theorem OAI.WLIdentification.AffineBlocks.OwnedTranslations.equivalent line 107

   Source documentation

   Exact projection implies the literal joint-WL equivalence.

   theorem equivalent (T : OwnedTranslations D beta G H) {K k : ℕ}
       (F : OffsetFamily D beta K) (hk : 2 ≤ k) (hkK : k < K) :
       Equivalent k (graphOfSimple G) (graphOfSimple H) :=
   …

   Mentions: OAI.WLIdentification.AffineBlocks.OwnedTranslations, OAI.WLIdentification.AffineBlocks.OffsetFamily, OAI.WLIdentification.Equivalent, OAI.WLIdentification.graphOfSimple

5. abbrev OAI.WLIdentification.AffineBlocks.BareVertex line 119
6. def OAI.WLIdentification.AffineBlocks.erase line 121
7. theorem OAI.WLIdentification.AffineBlocks.erase_injective line 125
8. def OAI.WLIdentification.AffineBlocks.bareTranslation line 142
9. def OAI.WLIdentification.AffineBlocks.BaseImages line 147
10. def OAI.WLIdentification.AffineBlocks.BareAdj line 151
11. theorem OAI.WLIdentification.AffineBlocks.bareAdj_erase line 156
12. theorem OAI.WLIdentification.AffineBlocks.bareAdj_translation line 160
13. theorem OAI.WLIdentification.AffineBlocks.baseImages_atomic line 178
14. def OAI.WLIdentification.AffineBlocks.vertexOwner line 187
15. theorem OAI.WLIdentification.AffineBlocks.baseImages_locality line 191
16. def OAI.WLIdentification.AffineBlocks.piecewiseTranslation line 210
17. theorem OAI.WLIdentification.AffineBlocks.piecewiseTranslation_images line 218
18. theorem OAI.WLIdentification.AffineBlocks.baseImages_color line 223
19. def OAI.WLIdentification.AffineBlocks.baseTranslations line 236

    Source documentation

    The finite affine construction realizes the local interfaces with no assumed graph isomorphism or winning strategy.

    def baseTranslations (D : AffineBlocks C B) (owner : C → B)
        (ho : ∀ c, c ∈ D.coordinates (owner c)) (beta : B → Bit) :
        OwnedTranslations D beta (D.baseGraph 0) (D.baseGraph beta) where
    …

    Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit, OAI.WLIdentification.AffineBlocks.OwnedTranslations

20. def OAI.WLIdentification.leafParent line 249

    Source documentation

    Parent and private index give an injective description of leaf-coded vertices.

    def leafParent {V : Type} {ell : V → ℕ} : LeafVertex ell → V
      | .inl v => v
      | .inr v => v.1

    Mentions: OAI.WLIdentification.LeafVertex

21. def OAI.WLIdentification.leafIndex line 253
22. theorem OAI.WLIdentification.leaf_eq_iff line 257
23. theorem OAI.WLIdentification.withLeaves_adj_iff line 278
24. def OAI.WLIdentification.AffineBlocks.OwnedTranslations.withLeaves line 294

    Source documentation

    Private leaves extend local translations exactly, retaining each private index; this is used before the owner pieces are combined into a game bijection.

    def withLeaves (T : OwnedTranslations D beta G H) (ell : V → ℕ) (ell' : W → ℕ)
        (hl : ∀ {x v w}, T.images x v w → ell v = ell' w) :
        OwnedTranslations D beta (WLIdentification.withLeaves G ell)
          (WLIdentification.withLeaves H ell') where
    …

    Mentions: OAI.WLIdentification.AffineBlocks.OwnedTranslations, OAI.WLIdentification.withLeaves

25. def OAI.WLIdentification.AffineBlocks.taggedTranslations line 332

    Source documentation

    Complete interface from exact-projection coordinate families to the actual uncolored graphs, with every private leaf and its owner included.

    noncomputable def taggedTranslations (D : AffineBlocks C B) (owner : C → B)
        (ho : ∀ c, c ∈ D.coordinates (owner c)) (beta : B → Bit) :
        OwnedTranslations D beta
          (withLeaves (D.baseGraph 0) (tagSize D.colorNat))
          (withLeaves (D.baseGraph beta) (tagSize D.colorNat)) :=
    …

    Mentions: OAI.WLIdentification.AffineBlocks, OAI.WLIdentification.Bit, OAI.WLIdentification.AffineBlocks.OwnedTranslations, OAI.WLIdentification.withLeaves, OAI.WLIdentification.tagSize

26. theorem OAI.WLIdentification.AffineBlocks.graph_equivalent_of_offsetFamily line 344