32.3. Ordered colours constrain isomorphisms🔗

nauty's colours are ordered: an isomorphism preserves each colour index and may not permute the cells. Marking an adjacent pair of Petersen vertices with colour zero is therefore a different constraint from marking a non-adjacent pair, although the cell sizes agree. Adjacency of the colour-zero pair is an invariant, and the tactic's negative proof is obtained from its general checked routes rather than a handwritten special-purpose lemma. These claims do mention colours, so they are the ones stated on Colored.

def markPair (a b : Fin 10) : Coloring 10 2 :=
  (Coloring.ofVector? (Hex.Vector.ofFn' fun i =>
    if i = a ∨ i = b then 0 else 1)).getD
      (Coloring.mod 10 2)

-- 0-1 is an outer pentagon edge; 2-3 likewise;
-- 0-2 is a non-edge.
def edgeMarkA : Colored 10 2 := ⟨petersen, markPair 0 1⟩
def edgeMarkB : Colored 10 2 := ⟨petersen, markPair 2 3⟩
def nonedgeMark : Colored 10 2 := ⟨petersen, markPair 0 2⟩

example : Isomorphic edgeMarkA edgeMarkB := by⊢ Isomorphic edgeMarkA edgeMarkB graph_isoAll goals completed! 🐙
example : ¬ Isomorphic edgeMarkA nonedgeMark := by⊢ ¬Isomorphic edgeMarkA nonedgeMark graph_isoAll goals completed! 🐙
example : ¬ Isomorphic edgeMarkB nonedgeMark := by⊢ ¬Isomorphic edgeMarkB nonedgeMark graph_isoAll goals completed! 🐙

end HexGraphIsoChapterExample