structure Hex.GraphIso.Nauty.Sparse.Max.Cell (n : Nat) : Type

A prepared native target, frozen before sibling permutations and filters.

• level : Nat
• numcells : Nat
• tc : Nat
• len : Nat
• codes : List Nat
• entry : State n

def Hex.GraphIso.Nauty.Sparse.Max.Cell.vertices {n : Nat} (c : Cell n) : VSet n

Equations

• c.vertices = Hex.GraphIso.Nauty.windowSet n c.entry.lab c.tc c.len

def Hex.GraphIso.Nauty.Sparse.Max.Cell.key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (c : Cell n) (v : Nat) : Key n

Equations

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

def Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (c : Cell n) (live : Nat → Prop) (best : Option (Key n)) : Prop

Equations

• Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover G tcLevel c live best = Hex.GraphIso.Nauty.Sparse.CellCover G tcLevel (n - c.level) c.level c.numcells c.tc c.len c.codes c.entry live best

structure Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid {n k : Nat} (G : Sparse.Colored n k) (c : Cell n) : Prop

Frozen target facts are about the executed native partition and cache.

• positive : 1 ≤ c.level
• length : c.codes.length = c.level
• ready : Ready G c.level c.numcells c.entry
• window : IsCell c.entry.ptn c.level c.tc c.len
• size : 1 < c.len
• range : c.tc + c.len ≤ n

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.depth {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} (h : Valid G c) : c.level ≤ n

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.fuel {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} (h : Valid G c) : n < n - c.level + (c.numcells + 1)

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.target {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} {st : State n} (h : Valid G c) (he : FrameOut G c.level c.level c.entry st) : Generic.Target State.frame c.level c.tc c.vertices st

Recovery retains the complete original window, including removed vertices.

def Hex.GraphIso.Nauty.Sparse.Max.Cell.child {n : Nat} (c : Cell n) (first : Bool) (st : State n) (v : Nat) : Frame n

The actual individualized entry of a child visited in a reordered parent.

Equations

• c.child first st v = { level := c.level + 1, numcells := c.numcells + 1, codes := c.codes, entry := Hex.GraphIso.Nauty.Generic.Policy.child first c.level c.tc v st }

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.child {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} {st : State n} (h : Valid G c) (he : FrameOut G c.level c.level c.entry st) (hs : Ready G c.level c.numcells st) (first : Bool) {v : Nat} (hv : c.vertices.mem v = true) : Frame.Valid G (c.child first st v)

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.child_key {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} {st : State n} (h : Valid G c) (he : FrameOut G c.level c.level c.entry st) (hs : Ready G c.level c.numcells st) (first : Bool) {v : Nat} (hv : c.vertices.mem v = true) (tcLevel : Nat) : Frame.key G.graph tcLevel (c.child first st v) = key G.graph tcLevel c v

The recursive child's frozen key is the original target's vertex key. The equality includes the exact sparse individualization and every unpruned descendant; parent recovery may reorder the labelling array.

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.grow {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {c : Cell n} {live : Nat → Prop} {before after : Option (Key n)} (h : Cover G tcLevel c live before) (hg : Grows before after) : Cover G tcLevel c live after

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Cover.finish {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {c : Cell n} {live : Nat → Prop} {best : Option (Key n)} (h : Cover G tcLevel c live best) (he : ∀ (v : Nat), ¬live v) (v : Nat) : c.vertices.mem v = true → Covers (key G tcLevel c v) best