structure Hex.GraphIso.Nauty.Key (n : Nat) : Type

A leaf key of the unpruned search tree: the level codes ending with the sentinel, then the leaf's adjacency rows.

• codes : List Nat

  The refinement codes along the path, ending with the sentinel.

• rows : List (VSet n)

  The leaf's g^lab rows in nauty's row order.

@[instance_reducible]

instance Hex.GraphIso.Nauty.instInhabitedKey {a✝ : Nat} : Inhabited (Key a✝)

Equations

• Hex.GraphIso.Nauty.instInhabitedKey = { default := Hex.GraphIso.Nauty.instInhabitedKey.default }

def Hex.GraphIso.Nauty.listCmp {α : Type} (cmp : α → α → Ordering) : List α → List α → Ordering

Lexicographic list comparison from an element comparison.

Equations

• Hex.GraphIso.Nauty.listCmp cmp [] [] = Ordering.eq
• Hex.GraphIso.Nauty.listCmp cmp [] (head :: tail) = Ordering.lt
• Hex.GraphIso.Nauty.listCmp cmp (head :: tail) [] = Ordering.gt
• Hex.GraphIso.Nauty.listCmp cmp (a :: as) (b :: bs) = match cmp a b with | Ordering.eq => Hex.GraphIso.Nauty.listCmp cmp as bs | Ordering.lt => Ordering.lt | Ordering.gt => Ordering.gt

def Hex.GraphIso.Nauty.keyCmp {n : Nat} (k1 k2 : Key n) : Ordering

The order on keys: level codes first, then rows in nauty's row order.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.keyMax {n : Nat} (k1 k2 : Key n) : Key n

The greater key, the first argument winning ties.

Equations

• Hex.GraphIso.Nauty.keyMax k1 k2 = if Hex.GraphIso.Nauty.keyCmp k1 k2 = Ordering.lt then k2 else k1

def Hex.GraphIso.Nauty.keysMax {n : Nat} (k : Key n) : List (Key n) → Key n

The maximum of a list of keys, seeded by an initial key.

Equations

• Hex.GraphIso.Nauty.keysMax k [] = k
• Hex.GraphIso.Nauty.keysMax k (k' :: rest) = Hex.GraphIso.Nauty.keysMax (Hex.GraphIso.Nauty.keyMax k k') rest

def Hex.GraphIso.Nauty.incMax {n : Nat} : Option (Key n) → Key n → Key n

The incumbent absorbed into a subtree's best key, an absent incumbent contributing nothing.

Equations

• Hex.GraphIso.Nauty.incMax none x✝ = x✝
• Hex.GraphIso.Nauty.incMax (some b) x✝ = Hex.GraphIso.Nauty.keyMax b x✝

def Hex.GraphIso.Nauty.discreteAt (ptn : Array Nat) (level nn : Nat) : Bool

Discreteness of the partition at level: every cell a singleton.

Equations

• Hex.GraphIso.Nauty.discreteAt ptn level nn = (Hex.GraphIso.Nauty.cells ptn level nn).all fun (p : Nat × Nat) => p.fst == p.snd

def Hex.GraphIso.Nauty.joinTest {n : Nat} (ctx : Ctx n) (lab : Array Nat) (wset : VSet n) (c1 c2 : Nat) : Bool

The specification's nontrivial-join test: some member of the cell starting at c1 has a neighbour in the splitter set, and some member misses part of it. Representative-independent, agreeing with nauty's first-vertex test on every equitable partition.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.specBestcellRow {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) (startArr : Array Nat) (workset : VSet n) (v2 : Nat) : List Nat → Array Nat → Array Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRow ctx lab ptn level startArr workset v2 [] x✝ = x✝

def Hex.GraphIso.Nauty.specBestcellRows {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) (startArr : Array Nat) : List Nat → Array Nat → Array Nat

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specBestcellRows ctx lab ptn level startArr [] x✝ = x✝

def Hex.GraphIso.Nauty.specBestcell {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level : Nat) : Nat

The specification's bestcell: nauty's rule with the join test on count multisets.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.specTargetcell {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level tcLevel : Nat) : Nat

The specification's hint-free target cell.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.specMaketargetcell {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level tcLevel : Nat) : Nat × VSet n × Nat

The specification's target cell with its contents and size.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.specNode {n : Nat} (ctx : Ctx n) (tcLevel : Nat) : Nat → Nat → Array Nat → Array Nat → VSet n → Nat → Key n

The key of the maximal leaf of the unpruned search tree below one node.

Equations

• One or more equations did not get rendered due to their size.
• Hex.GraphIso.Nauty.specNode ctx tcLevel 0 x✝⁴ x✝³ x✝² x✝¹ x✝ = { codes := [], rows := [] }

def Hex.GraphIso.Nauty.canonSpec (n : Nat) (g : Array (VSet n)) (lab0 : Array Nat) (cellEnds : List Nat) : Key n

The canonical key of the unpruned nauty search on n vertices with adjacency rows g and initial ordered partition (lab0, cellEnds).

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.canonSpecKey {n k : Nat} (G : Colored n k) : Key n

The nauty-semantic canonical key of a coloured graph.

Equations

• Hex.GraphIso.Nauty.canonSpecKey G = Hex.GraphIso.Nauty.canonSpec n (Hex.GraphIso.Nauty.rowsOf G) (Hex.GraphIso.Nauty.initialPartition G).fst (Hex.GraphIso.Nauty.initialPartition G).snd

theorem Hex.GraphIso.Nauty.listCmp_eq_iff {α : Type} {cmp : α → α → Ordering} (heq : ∀ (a b : α), cmp a b = Ordering.eq ↔ a = b) (l1 l2 : List α) : listCmp cmp l1 l2 = Ordering.eq ↔ l1 = l2

theorem Hex.GraphIso.Nauty.listCmp_gt_iff_lt {α : Type} {cmp : α → α → Ordering} (heq : ∀ (a b : α), cmp a b = Ordering.eq ↔ a = b) (hgl : ∀ (a b : α), cmp a b = Ordering.gt ↔ cmp b a = Ordering.lt) (l1 l2 : List α) : listCmp cmp l1 l2 = Ordering.gt ↔ listCmp cmp l2 l1 = Ordering.lt

theorem Hex.GraphIso.Nauty.listCmp_gt_trans {α : Type} {cmp : α → α → Ordering} (heq : ∀ (a b : α), cmp a b = Ordering.eq ↔ a = b) (htr : ∀ (a b c : α), cmp a b = Ordering.gt → cmp b c = Ordering.gt → cmp a c = Ordering.gt) (l1 l2 l3 : List α) : listCmp cmp l1 l2 = Ordering.gt → listCmp cmp l2 l3 = Ordering.gt → listCmp cmp l1 l3 = Ordering.gt

theorem Hex.GraphIso.Nauty.keyCmp_eq_iff {n : Nat} {k1 k2 : Key n} : keyCmp k1 k2 = Ordering.eq ↔ k1 = k2

theorem Hex.GraphIso.Nauty.keyCmp_gt_iff_lt {n : Nat} {k1 k2 : Key n} : keyCmp k1 k2 = Ordering.gt ↔ keyCmp k2 k1 = Ordering.lt

theorem Hex.GraphIso.Nauty.keyCmp_gt_trans {n : Nat} {k1 k2 k3 : Key n} (h1 : keyCmp k1 k2 = Ordering.gt) (h2 : keyCmp k2 k3 = Ordering.gt) : keyCmp k1 k3 = Ordering.gt

theorem Hex.GraphIso.Nauty.keyCmp_self {n : Nat} (k : Key n) : keyCmp k k = Ordering.eq

theorem Hex.GraphIso.Nauty.keyCmp_ge_trans {n : Nat} {k1 k2 k3 : Key n} (h1 : keyCmp k1 k2 ≠ Ordering.lt) (h2 : keyCmp k2 k3 ≠ Ordering.lt) : keyCmp k1 k3 ≠ Ordering.lt

theorem Hex.GraphIso.Nauty.keyCmp_antisym {n : Nat} {k1 k2 : Key n} (h1 : keyCmp k1 k2 ≠ Ordering.lt) (h2 : keyCmp k2 k1 ≠ Ordering.lt) : k1 = k2

theorem Hex.GraphIso.Nauty.keyMax_mem {n : Nat} (x y : Key n) : keyMax x y = x ∨ keyMax x y = y

theorem Hex.GraphIso.Nauty.keyMax_not_lt_left {n : Nat} (x y : Key n) : keyCmp (keyMax x y) x ≠ Ordering.lt

theorem Hex.GraphIso.Nauty.keyMax_not_lt_right {n : Nat} (x y : Key n) : keyCmp (keyMax x y) y ≠ Ordering.lt

theorem Hex.GraphIso.Nauty.keyMax_comm2 {n : Nat} (b a1 a2 : Key n) : keyMax (keyMax b a1) a2 = keyMax (keyMax b a2) a1

Folding the pairwise maximum is right-commutative, so the running maximum is permutation-invariant.

theorem Hex.GraphIso.Nauty.keysMax_eq_foldl {n : Nat} (l : List (Key n)) (k : Key n) : keysMax k l = List.foldl keyMax k l

theorem Hex.GraphIso.Nauty.keysMax_perm {n : Nat} {l l' : List (Key n)} (h : l.Perm l') (k : Key n) : keysMax k l = keysMax k l'

The running key maximum is invariant under permutation of the list.

theorem Hex.GraphIso.Nauty.joinTest_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab : Array Nat} (hlab : LabOk lab n) {wset : VSet n} {c1 c2 : Nat} (h2 : c2 < lab.size) : joinTest ctx' (Array.map σ.toFun lab) (VSet.image σ.toFun wset) c1 c2 = joinTest ctx lab wset c1 c2

theorem Hex.GraphIso.Nauty.specBestcellRow_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} {level : Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) {startArr : Array Nat} (hstart : ∀ (v : Nat), startArr[v]! < n) {workset : VSet n} (v2 : Nat) (vs : List Nat) (bucket : Array Nat) : specBestcellRow ctx' (Array.map σ.toFun lab) ptn level startArr (VSet.image σ.toFun workset) v2 vs bucket = specBestcellRow ctx lab ptn level startArr workset v2 vs bucket

theorem Hex.GraphIso.Nauty.specBestcellRows_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} {level : Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) {startArr : Array Nat} (hstart : ∀ (v : Nat), startArr[v]! < n) (vs : List Nat) (bucket : Array Nat) : specBestcellRows ctx' (Array.map σ.toFun lab) ptn level startArr vs bucket = specBestcellRows ctx lab ptn level startArr vs bucket

theorem Hex.GraphIso.Nauty.specBestcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level : Nat} (hend : ptn[ptn.size - 1]! ≤ level) : specBestcell ctx' (Array.map σ.toFun lab) ptn level = specBestcell ctx lab ptn level

The specification's bestcell is position-valued and invariant under a renaming.

theorem Hex.GraphIso.Nauty.specTargetcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level tcLevel : Nat} (hend : ptn[ptn.size - 1]! ≤ level) : specTargetcell ctx' (Array.map σ.toFun lab) ptn level tcLevel = specTargetcell ctx lab ptn level tcLevel

The specification's target cell is position-valued and invariant under a renaming.

theorem Hex.GraphIso.Nauty.specMaketargetcell_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) {lab ptn : Array Nat} (hlab : LabOk lab n) (hsl : lab.size = n) (hsp : ptn.size = n) {level tcLevel : Nat} (hend : ptn[ptn.size - 1]! ≤ level) (hi : specTargetcell ctx lab ptn level tcLevel + 1 < n) : specMaketargetcell ctx' (Array.map σ.toFun lab) ptn level tcLevel = ((specMaketargetcell ctx lab ptn level tcLevel).fst, VSet.image σ.toFun (specMaketargetcell ctx lab ptn level tcLevel).snd.fst, (specMaketargetcell ctx lab ptn level tcLevel).snd.snd)

The specification's target-cell data transports position and size unchanged and the cell set to its image.

theorem Hex.GraphIso.Nauty.specBestcell_mem {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} (hex : List.filter (fun (x : Nat × Nat) => match x with | (c1, c2) => decide (c1 ≠ c2)) (cells ptn level n) ≠ []) : specBestcell ctx lab ptn level ∈ List.map (fun (x : Nat × Nat) => x.fst) (List.filter (fun (x : Nat × Nat) => match x with | (c1, c2) => decide (c1 ≠ c2)) (cells ptn level n))

The specification's bestcell returns a nonsingleton cell start when one exists.

theorem Hex.GraphIso.Nauty.specTargetcell_nontrivial {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tcLevel : Nat} (hex : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd) : ∃ (p : Nat × Nat), p ∈ cells ptn level n ∧ p.fst ≠ p.snd ∧ specTargetcell ctx lab ptn level tcLevel = p.fst

With a nonsingleton cell present, the specification's target cell is a nonsingleton cell start.

theorem Hex.GraphIso.Nauty.joinTest_perm {n : Nat} {ctx : Ctx n} {lab lab' : Array Nat} {wset : VSet n} {c1 c2 : Nat} (hseg : (segN lab c1 (c2 + 1 - c1)).Perm (segN lab' c1 (c2 + 1 - c1))) : joinTest ctx lab wset c1 c2 = joinTest ctx lab' wset c1 c2

theorem Hex.GraphIso.Nauty.specBestcellRow_perm {n : Nat} {ctx : Ctx n} {lab lab' ptn : Array Nat} {level : Nat} (hcp : cellsPerm ptn level lab lab') (hend : ptn[ptn.size - 1]! ≤ level) {startArr : Array Nat} (hstart : ∀ (v : Nat), startArr[v]! < ptn.size) (hstart2 : ∀ (v : Nat), startArr[v]! = 0 ∨ ptn[startArr[v]! - 1]! ≤ level) (workset : VSet n) (v2 : Nat) (vs : List Nat) (bucket : Array Nat) : specBestcellRow ctx lab ptn level startArr workset v2 vs bucket = specBestcellRow ctx lab' ptn level startArr workset v2 vs bucket

theorem Hex.GraphIso.Nauty.specBestcellRows_perm {n : Nat} {ctx : Ctx n} {lab lab' ptn : Array Nat} {level : Nat} (hcp : cellsPerm ptn level lab lab') (hend : ptn[ptn.size - 1]! ≤ level) {startArr : Array Nat} (hstart : ∀ (v : Nat), startArr[v]! < ptn.size) (hstart2 : ∀ (v : Nat), startArr[v]! = 0 ∨ ptn[startArr[v]! - 1]! ≤ level) (vs : List Nat) (bucket : Array Nat) : specBestcellRows ctx lab ptn level startArr vs bucket = specBestcellRows ctx lab' ptn level startArr vs bucket

theorem Hex.GraphIso.Nauty.specBestcell_perm {n : Nat} {ctx : Ctx n} {lab lab' ptn : Array Nat} {level : Nat} (hcp : cellsPerm ptn level lab lab') (hnn : n ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : specBestcell ctx lab ptn level = specBestcell ctx lab' ptn level

The specification's bestcell depends on the labelling only through cell contents.

theorem Hex.GraphIso.Nauty.specTargetcell_perm {n : Nat} {ctx : Ctx n} {lab lab' ptn : Array Nat} {level tcLevel : Nat} (hcp : cellsPerm ptn level lab lab') (hnn : n ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) : specTargetcell ctx lab ptn level tcLevel = specTargetcell ctx lab' ptn level tcLevel

The specification's target cell depends on the labelling only through cell contents.

theorem Hex.GraphIso.Nauty.cells_go_cover {ptn : Array Nat} {level nn : Nat} (fuel c1 i : Nat) : c1 ≤ i → i < nn → nn ≤ fuel + c1 → ∃ (p : Nat × Nat), p ∈ cells.go ptn level nn fuel c1 ∧ p.fst ≤ i ∧ i ≤ p.snd

theorem Hex.GraphIso.Nauty.cells_cover {ptn : Array Nat} {level nn : Nat} (i : Nat) (hi : i < nn) : ∃ (p : Nat × Nat), p ∈ cells ptn level nn ∧ p.fst ≤ i ∧ i ≤ p.snd

theorem Hex.GraphIso.Nauty.discrete_pointwise {ptn : Array Nat} {level nn : Nat} {lab lab' : Array Nat} (hcp : cellsPerm ptn level lab lab') (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hdisc : discreteAt ptn level nn = true) (i : Nat) : i < nn → lab[i]! = lab'[i]!

On a discrete partition, cell-equivalent labellings agree pointwise.

theorem Hex.GraphIso.Nauty.invPerm_congr {lab lab' : Array Nat} (hsz : lab.size = lab'.size) (h : ∀ (i : Nat), i < lab.size → lab[i]! = lab'[i]!) : invPerm lab = invPerm lab'

theorem Hex.GraphIso.Nauty.leafRows_congr {n : Nat} {ctx : Ctx n} {lab lab' : Array Nat} (hsz : lab.size = lab'.size) (hnn : n ≤ lab.size) (h : ∀ (i : Nat), i < lab.size → lab[i]! = lab'[i]!) : leafRows ctx lab = leafRows ctx lab'

theorem Hex.GraphIso.Nauty.range_map_eq_segN_map {n : Nat} (lab : Array Nat) (lo len : Nat) (F : Nat → Key n) : List.map (fun (o : Nat) => F lab[lo + o]!) (List.range len) = List.map F (segN lab lo len)

theorem Hex.GraphIso.Nauty.keysMax_mem {n : Nat} (l : List (Key n)) (k : Key n) : keysMax k l = k ∨ keysMax k l ∈ l

theorem Hex.GraphIso.Nauty.keysMax_ge {n : Nat} (l : List (Key n)) (k y : Key n) : y = k ∨ y ∈ l → keyCmp (keysMax k l) y ≠ Ordering.lt

theorem Hex.GraphIso.Nauty.keysMax_cons_perm {n : Nat} {c c' : Key n} {cs cs' : List (Key n)} (h : (c :: cs).Perm (c' :: cs')) : keysMax c cs = keysMax c' cs'

The head-seeded key maximum is invariant under permutation of the whole list.

theorem Hex.GraphIso.Nauty.cellEnd_go_unique {ptn : Array Nat} {level : Nat} (fuel start e : Nat) : start ≤ e → (∀ (i : Nat), start ≤ i → i < e → ptn[i]! > level) → ptn[e]! ≤ level → e - start < fuel → cellEnd.go ptn level fuel start = e

theorem Hex.GraphIso.Nauty.cellEnd_of_isCell_start {ptn : Array Nat} {level a len : Nat} (h : IsCell ptn level a len) (hin : a + len - 1 < ptn.size) : cellEnd ptn level a = a + len - 1

A maximal run's end from its start is what cellEnd computes.

theorem Hex.GraphIso.Nauty.cellEnd_of_isCell {ptn : Array Nat} {level a len : Nat} (h : IsCell ptn level a len) (h2 : 2 ≤ len) (hsz : a + len ≤ ptn.size) : cellEnd ptn level (a + 1) = a + len - 1

For a nonsingleton run, the cell end from one past the start is the run's last position.

theorem Hex.GraphIso.Nauty.specNode_map {n : Nat} (σ : Renaming n) {ctx ctx' : Ctx n} (hg : RowsMap σ ctx.g ctx'.g) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (active : VSet n) (numcells : Nat) : lab.size = n → LabOk lab n → ptn.size = n → ptn[ptn.size - 1]! ≤ level → specNode ctx' tcLevel fuel level (Array.map σ.toFun lab) ptn active numcells = specNode ctx tcLevel fuel level lab ptn active numcells

The unpruned search tree's maximal leaf key is invariant under a vertex renaming: on the renamed graph with the transported labelling, every node produces the same key.

theorem Hex.GraphIso.Nauty.specNode_perm {n : Nat} {ctx : Ctx n} (tcLevel fuel level : Nat) (lab lab' ptn : Array Nat) (active : VSet n) (numcells : Nat) : cellsPerm ptn level lab lab' → lab'.size = lab.size → lab.size = n → LabOk lab n → LabOk lab' n → ptn.size = n → ptn[ptn.size - 1]! ≤ level → (∀ (v : Nat), active.mem v = true → v = 0 ∨ ptn[v - 1]! ≤ level) → (∀ (q : Nat), ptn[q]! ≤ level ∨ ptn[q]! = n + 2) → level + fuel ≤ n + 1 → specNode ctx tcLevel fuel level lab ptn active numcells = specNode ctx tcLevel fuel level lab' ptn active numcells

The unpruned search tree's maximal leaf key depends on the labelling only through cell contents.

structure Hex.GraphIso.Nauty.SeedShift {n : Nat} (δ : Nat) (st st' : RefineSt n) : Prop

Refine states equal up to a numcells shift of δ and the longcode accumulator.

• lab : st'.lab = st.lab
• ptn : st'.ptn = st.ptn
• active : st'.active = st.active
• hint : st'.hint = st.hint
• maxpos : st'.maxpos = st.maxpos
• numcells : st'.numcells = st.numcells + δ

theorem Hex.GraphIso.Nauty.seedShift_mk {n δ : Nat} {l p : Array Nat} {a : VSet n} {nc hi mp lc nc' lc' : Nat} (h : nc' = nc + δ) : SeedShift δ { lab := l, ptn := p, active := a, numcells := nc, hint := hi, maxpos := mp, longcode := lc } { lab := l, ptn := p, active := a, numcells := nc', hint := hi, maxpos := mp, longcode := lc' }

theorem Hex.GraphIso.Nauty.trivialSplit_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (level cell1 cell2 : Nat) (c1 c2 : Int) : SeedShift δ (trivialSplit level cell1 cell2 c1 c2 st) (trivialSplit level cell1 cell2 c1 c2 st')

theorem Hex.GraphIso.Nauty.trivialCell_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (level : Nat) (gRow : VSet n) (cell1 cell2 : Nat) : SeedShift δ (trivialCell level gRow cell1 cell2 st) (trivialCell level gRow cell1 cell2 st')

theorem Hex.GraphIso.Nauty.refineTrivial_go_seed {n δ : Nat} (level : Nat) (gRow : VSet n) (l : List (Nat × Nat)) (st st' : RefineSt n) : SeedShift δ st st' → SeedShift δ (refineTrivial.go level gRow l st) (refineTrivial.go level gRow l st')

theorem Hex.GraphIso.Nauty.refineTrivial_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (ctx : Ctx n) (level split1 : Nat) : SeedShift δ (refineTrivial ctx level split1 st) (refineTrivial ctx level split1 st')

theorem Hex.GraphIso.Nauty.windowStep_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (level cell1 cell2 v c1 c2 : Nat) (maxcell : Int) : SeedShift δ (windowStep level cell1 cell2 v c1 c2 maxcell st) (windowStep level cell1 cell2 v c1 c2 maxcell st')

theorem Hex.GraphIso.Nauty.windowScan_seed {n δ : Nat} (level cell1 cell2 : Nat) (counts vs : List Nat) (c1 : Nat) (maxcell : Int) (st st' : RefineSt n) : SeedShift δ st st' → SeedShift δ (windowScan level cell1 cell2 counts vs c1 maxcell st) (windowScan level cell1 cell2 counts vs c1 maxcell st')

theorem Hex.GraphIso.Nauty.nontrivialFix_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (cell1 : Nat) : SeedShift δ (nontrivialFix cell1 st) (nontrivialFix cell1 st')

theorem Hex.GraphIso.Nauty.nontrivialCell_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (ctx : Ctx n) (level : Nat) (workset : VSet n) (cell1 cell2 : Nat) : SeedShift δ (nontrivialCell ctx level workset cell1 cell2 st) (nontrivialCell ctx level workset cell1 cell2 st')

theorem Hex.GraphIso.Nauty.refineNontrivial_go_seed {n δ : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (l : List (Nat × Nat)) (st st' : RefineSt n) : SeedShift δ st st' → SeedShift δ (refineNontrivial.go ctx level workset l st) (refineNontrivial.go ctx level workset l st')

theorem Hex.GraphIso.Nauty.refineNontrivial_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (ctx : Ctx n) (level split1 split2 : Nat) : SeedShift δ (refineNontrivial ctx level split1 split2 st) (refineNontrivial ctx level split1 split2 st')

theorem Hex.GraphIso.Nauty.refineStep_seed {n δ : Nat} {st st' : RefineSt n} (h : SeedShift δ st st') (ctx : Ctx n) (level split1 : Nat) : SeedShift δ (refineStep ctx level split1 st) (refineStep ctx level split1 st')

theorem Hex.GraphIso.Nauty.cells_eq_of_discreteAt {ptn : Array Nat} {level nn : Nat} (hdisc : discreteAt ptn level nn = true) (q : Nat × Nat) : q ∈ cells ptn level nn → (q.fst == q.snd) = true

theorem Hex.GraphIso.Nauty.refineTrivial_go_of_discrete {n : Nat} (level : Nat) (gRow : VSet n) (l : List (Nat × Nat)) (st : RefineSt n) : (∀ (q : Nat × Nat), q ∈ l → (q.fst == q.snd) = true) → refineTrivial.go level gRow l st = st

theorem Hex.GraphIso.Nauty.refineNontrivial_go_of_discrete {n : Nat} (ctx : Ctx n) (level : Nat) (workset : VSet n) (l : List (Nat × Nat)) (st : RefineSt n) : (∀ (q : Nat × Nat), q ∈ l → (q.fst == q.snd) = true) → refineNontrivial.go ctx level workset l st = st

theorem Hex.GraphIso.Nauty.refineStep_of_discrete {n : Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (hdisc : discreteAt st.ptn level n = true) (split1 : Nat) : ∃ (c : Nat), refineStep ctx level split1 st = { lab := st.lab, ptn := st.ptn, active := st.active.erase split1, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := c }

theorem Hex.GraphIso.Nauty.refineLoop_of_discrete {n : Nat} {ctx : Ctx n} {level : Nat} (fuel : Nat) (st : RefineSt n) : discreteAt st.ptn level n = true → ∃ (a : VSet n), ∃ (c : Nat), refineLoop ctx level fuel st = { lab := st.lab, ptn := st.ptn, active := a, numcells := st.numcells, hint := st.hint, maxpos := st.maxpos, longcode := c }

structure Hex.GraphIso.Nauty.SeedExit {n : Nat} (ctx : Ctx n) (level δ : Nat) (st st' : RefineSt n) : Prop

The exit relation of refine_seed: labelling, partition, hint and maxpos agree, cell counts differ by exactly the seed shift, and the active sets agree whenever the exit partition is not discrete.

• lab : st'.lab = st.lab
• ptn : st'.ptn = st.ptn
• hint : st'.hint = st.hint
• maxpos : st'.maxpos = st.maxpos
• numcells : st'.numcells = st.numcells + δ
• active : discreteAt st'.ptn level n = false → st'.active = st.active

theorem Hex.GraphIso.Nauty.refineLoop_seed {n : Nat} {ctx : Ctx n} {level δ : Nat} (fuel : Nat) (st st' : RefineSt n) : SeedShift δ st st' → (n ≤ (refineLoop ctx level fuel st').numcells → discreteAt (refineLoop ctx level fuel st').ptn level n = true) → SeedExit ctx level δ (refineLoop ctx level fuel st) (refineLoop ctx level fuel st')

theorem Hex.GraphIso.Nauty.refine_seed {n : Nat} {ctx : Ctx n} {level : Nat} {lab ptn : Array Nat} {active : VSet n} (m δ : Nat) (hd : n ≤ (refine ctx level lab ptn active (m + δ)).numcells → discreteAt (refine ctx level lab ptn active (m + δ)).ptn level n = true) : SeedExit ctx level δ (refine ctx level lab ptn active m) (refine ctx level lab ptn active (m + δ))

Seed-independence of refine: two runs whose numcells seeds differ by δ produce the same lab, ptn, hint and maxpos, cell counts differing by exactly δ, and the same active set whenever the exit partition is not discrete. Only longcode and numcells carry the seed. The hypothesis rules out a guard exit on a non-discrete partition. It holds whenever the larger seed is at most the true cell count of (ptn, level), in particular for the counts the search maintains.