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

A native node frozen at entry, together with its preceding refinement codes.

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

def Hex.GraphIso.Nauty.Sparse.Max.Frame.key {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : Key n

The complete sparse subtree with a depth-derived sufficient fuel bound.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Max.Frame.code {n : Nat} (G : SparseGraph n) (f : Frame n) : Nat

The literal code computed by the cached native visit.

Equations

• Hex.GraphIso.Nauty.Sparse.Max.Frame.code G f = (Hex.GraphIso.Nauty.Sparse.visit (Hex.GraphIso.Nauty.Sparse.Graph.ofGraph G) f.level f.numcells f.entry).snd.fst

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

Frozen entries retain the native structural invariant and code depth.

• positive : 1 ≤ f.level
• length : f.codes.length + 1 = f.level
• node : NodeInv G f.level f.numcells f.entry

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.tail {n k : Nat} {G : Sparse.Colored n k} {f : Frame n} (h : Valid G f) (tcLevel : Nat) : ∃ (tail : Key n), key G.graph tcLevel f = prefixKey (f.codes ++ [code G.graph f]) tail

The complete subtree starts with the code of its executed cached visit.

def Hex.GraphIso.Nauty.Sparse.Max.Frame.Witness {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (best : Option (Key n)) : Prop

A returned ancestor is covered directly or by rejection of every continuation of its first actual refinement code.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Witness.resolve {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {best : Option (Key n)} (h : Witness G.graph tcLevel f best) (hv : Valid G f) : Covers (key G.graph tcLevel f) best

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Witness.grow {n : Nat} {G : SparseGraph n} {tcLevel : Nat} {f : Frame n} {before after : Option (Key n)} (h : Witness G tcLevel f before) (hg : Grows before after) : Witness G tcLevel f after

@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Sparse.Max.Frames (n : Nat) : Type

Frozen native subtrees indexed by the sweep receiving their return.

Equations

• Hex.GraphIso.Nauty.Sparse.Max.Frames n = (Nat → Option (Hex.GraphIso.Nauty.Sparse.Max.Frame n))

def Hex.GraphIso.Nauty.Sparse.Max.Frames.insert {n : Nat} (frames : Frames n) (f : Frame n) : Frames n

Equations

• frames.insert f level = if level = f.level - 1 then some f else frames level

def Hex.GraphIso.Nauty.Sparse.Max.Witness {n k : Nat} (G : Sparse.Colored n k) (tcLevel : Nat) (frames : Frames n) (target : Nat) (best : Option (Key n)) : Prop

A nonlocal exit names a valid frozen ancestor and its coverage witness.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Witness.resolve {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {frames : Frames n} {f : Frame n} {best : Option (Key n)} (h : Witness G tcLevel (frames.insert f) (f.level - 1) best) : Covers (Frame.key G.graph tcLevel f) best

theorem Hex.GraphIso.Nauty.Sparse.Max.Witness.below {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {frames : Frames n} {f : Frame n} {best : Option (Key n)} (ht : target < f.level - 1) : Witness G tcLevel (frames.insert f) target best ↔ Witness G tcLevel frames target best

theorem Hex.GraphIso.Nauty.Sparse.Max.Witness.grow {n k : Nat} {G : Sparse.Colored n k} {tcLevel target : Nat} {frames : Frames n} {before after : Option (Key n)} (h : Witness G tcLevel frames target before) (hg : Grows before after) : Witness G tcLevel frames target after