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

The geometric and path bounds of a frozen node.

• positive : 1 ≤ f.level
• depth : f.level ≤ n
• length : f.codes.length + 1 = f.level
• partition : SearchOk G f.level f.numcells f.entry

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

A frozen node's target selection, before its children are visited.

• node : Frame n
• first : Bool

def Hex.GraphIso.Nauty.Max.Loop.prepare {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (l : Loop n) : Nat × Int × VSet n × Nat × Search n

The search's common preparation of an internal node's sweep.

Equations

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

def Hex.GraphIso.Nauty.Max.Loop.codes {n : Nat} (ctx : Ctx n) (l : Loop n) : List Nat

The common code prefix of the chosen children.

Equations

• Hex.GraphIso.Nauty.Max.Loop.codes ctx l = l.node.codes ++ [Hex.GraphIso.Nauty.Max.Frame.code ctx l.node]

def Hex.GraphIso.Nauty.Max.Loop.key {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (l : Loop n) (v : Nat) : Key n

A child's full specification key in the frozen sweep ordering.

Equations

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

def Hex.GraphIso.Nauty.Max.Loop.Choice {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (l : Loop n) (best : Option (Key n)) : Prop

A target agrees with the specification, or a negative code comparison already bounds the entire frozen node by the incumbent.

Equations

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

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

A suspended parent retains the state at its chosen child's entry, including the incumbent codes used by its already covered references.

• loop : Loop n
• state : Search n
• chosen : Nat
• bs : List Nat
• fs : List Nat

def Hex.GraphIso.Nauty.Max.Parent.child {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (p : Parent n) : Frame n

The actual individualization at a suspended parent.

Equations

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

structure Hex.GraphIso.Nauty.Max.Parent.Valid {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (p : Parent n) : Prop

Reference and geometric facts retained at a suspended parent.

• node : Frame.Valid G p.loop.node
• partition : SearchOk G p.loop.node.level (Loop.prepare ctx tcLevel p.loop).fst p.state
• effect : SearchOut G p.loop.node.level p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd p.state
• equitable : Equitable ctx p.loop.node.level p.state.lab p.state.ptn
• cell : IsCell (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.fst
• len : 2 ≤ (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.fst
• range : (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat + (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.fst ≤ n
• chosen : (windowSet n p.state.lab (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.fst).mem p.chosen = true
• path : PathInv G ctx p.loop.node.level p.state
• choice : Loop.Choice ctx tcLevel p.loop (SearchState.key ctx p.bs p.state)
• canonical : CanonGuide p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd (Loop.key ctx tcLevel p.loop) (SearchState.key ctx p.bs p.state) p.state
• first : p.state.gcaFirst = p.loop.node.level → Generic.Covers (Loop.key ctx tcLevel p.loop p.state.firstlab[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]!) (SearchState.key ctx p.bs p.state) ∧ cellsPerm (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.ptn p.loop.node.level (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab p.state.firstlab
• small : p.state.noncheaplevel ≤ p.loop.node.level → SubtreeOk ctx p.loop.node.level { lab := p.state.lab, ptn := p.state.ptn, active := p.state.active, numcells := (Loop.prepare ctx tcLevel p.loop).fst, hint := 0, maxpos := 0, longcode := 0 }
• earlier (v : Nat) : (windowSet n (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.snd.lab (Loop.prepare ctx tcLevel p.loop).snd.fst.toNat (Loop.prepare ctx tcLevel p.loop).snd.snd.snd.fst).mem v = true → v < p.chosen → Generic.Covers (Loop.key ctx tcLevel p.loop v) (SearchState.key ctx p.bs p.state)

@[reducible, inline]

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

Suspended ancestors indexed by their sweep levels.

Equations

• Hex.GraphIso.Nauty.Max.Parents n = (Nat → Option (Hex.GraphIso.Nauty.Max.Parent n))

def Hex.GraphIso.Nauty.Max.Parents.frames {n : Nat} (ctx : Ctx n) (tcLevel : Nat) (parents : Parents n) : Frames n

Each suspended parent names its current child's specification subtree. The outermost parent also retains the root subtree at return target zero.

Equations

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

structure Hex.GraphIso.Nauty.Max.Scope {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel level : Nat) (cs bs : List Nat) (st : Search n) (parents : Parents n) : Prop

The current call retains each ancestor's cell frame, chosen vertex, reference location, code prefix, and previously installed incumbent.

• complete (t : Nat) : 1 ≤ t → t < level → ∃ (p : Parent n), parents t = some p
• valid (t : Nat) (p : Parent n) : parents t = some p → 1 ≤ t ∧ t < level ∧ p.loop.node.level = t ∧ Parent.Valid G ctx tcLevel p
• codes (t : Nat) (p : Parent n) : parents t = some p → Loop.codes ctx p.loop <+: cs
• code (t : Nat) (p : Parent n) : parents t = some p → t < cs.length → Frame.code ctx (Parent.child ctx tcLevel p) = cs[t]!
• grows (t : Nat) (p : Parent n) : parents t = some p → Generic.Grows (SearchState.key ctx p.bs p.state) (SearchState.key ctx bs st)
• effect (t : Nat) (p : Parent n) : parents t = some p → SearchOut G t t p.state st
• chosen (t : Nat) (p : Parent n) : parents t = some p → st.lab[(Loop.prepare ctx tcLevel p.loop).snd.fst.toNat]! = p.chosen
• canonical (t : Nat) (p : Parent n) : parents t = some p → st.gcaCanon ≤ t → st.gcaCanon = p.state.gcaCanon ∧ st.canonlab = p.state.canonlab
• first (t : Nat) (p : Parent n) : parents t = some p → st.gcaFirst ≤ t → st.gcaFirst = p.state.gcaFirst ∧ st.firstlab = p.state.firstlab
• boundary (t : Nat) (p : Parent n) : parents t = some p → st.noncheaplevel = p.state.noncheaplevel ∨ t + 1 ≤ st.noncheaplevel
• generators (t : Nat) (p : Parent n) : parents t = some p → p.loop.first = true → ∀ (γ : Array Nat), γ ∈ st.genTrace → CellStab p.state.ptn t p.state.lab γ
• coset (t : Nat) (p : Parent n) : parents t = some p → 0 < st.canonlevel → st.gcaFirst = t → p.loop.first = true ∧ st.cosetindex = p.chosen
• chain (t : Nat) (p : Parent n) : parents t = some p → 1 < t → ∃ (prev : Parent n), parents (t - 1) = some prev ∧ Parent.child ctx tcLevel prev = p.loop.node

theorem Hex.GraphIso.Nauty.Max.Scope.root {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (bs : List Nat) (st : Search n) : Scope G ctx tcLevel 1 [] bs st fun (x : Nat) => none

The first node has no suspended ancestors.

def Hex.GraphIso.Nauty.Max.Entry {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel : Nat) (first : Bool) (f : Frame n) (bs fs : List Nat) : Prop

Before the first leaf, only the first path's stored code prefix is needed. Later entries have both comparison machines and an installed incumbent.

Equations

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

structure Hex.GraphIso.Nauty.Max.NodeInput {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel fuel : Nat) (first : Bool) (f : Frame n) (bs fs : List Nat) (parents : Parents n) : Prop

A node contract is quantified over its actual semantic context.

• frame : Frame.Valid G f
• fuel : n + 1 ≤ f.level + fuel
• entry : Entry G ctx tcLevel first f bs fs
• scope : Scope G ctx tcLevel f.level f.codes bs f.entry parents
• parent : 1 < f.level → ∃ (p : Parent n), parents (f.level - 1) = some p ∧ Parent.child ctx tcLevel p = f
• counters : 0 < f.entry.canonlevel → 0 < f.entry.gcaFirst ∧ f.entry.gcaFirst ≤ f.entry.gcaCanon