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

A native sweep frozen at the node whose target it traverses.

• node : Frame n
• first : Bool

def Hex.GraphIso.Nauty.Sparse.Max.Loop.prepare {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (l : Loop n) : Nat × Int × VSet n × Nat × State n

The literal native preparation, including code comparison, target hinting and the cheap guard.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Max.Loop.cell {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (l : Loop n) : Cell n

The complete selected cell, before any orbit skip or target filter. Its coordinates come from the actual dispatch, including hinted targets; its frozen ordering is the actual cached visit's ordering.

Equations

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

def Hex.GraphIso.Nauty.Sparse.Max.Loop.parent {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (l : Loop n) (st : State n) (bs : List Nat) (cell : VSet n) (tv : Nat) : Parent n

Suspending a selected child retains the actual sweep's target coordinate while its state and remaining bitset may have changed.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.first_parent {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : have l := { node := f, first := true }; parent G tcLevel l (prepare G tcLevel l).snd.snd.snd.snd bs (prepare G tcLevel l).snd.snd.fst tv = Frame.firstParent G tcLevel f bs tv

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.other_parent {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) (bs : List Nat) (tv : Nat) : have l := { node := f, first := false }; parent G tcLevel l (prepare G tcLevel l).snd.snd.snd.snd bs (prepare G tcLevel l).snd.snd.fst tv = Frame.otherParent G tcLevel f bs tv

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.prepared {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {l : Loop n} (h : Frame.Valid G l.node) : have c := cell G.graph tcLevel l; have st := (prepare G.graph tcLevel l).snd.snd.snd.snd; Ready G c.level c.numcells st ∧ FrameOut G c.level c.level c.entry st

Every prepared sweep retains the equitable visit and its exact partition frame through recording, comparison, selection and the guard.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.preserve {n : Nat} {G : SparseGraph n} {inf tcLevel : Nat} {l : Loop n} {P : State n → Prop} (h : Generic.Preserve (Graph.ofGraph G) inf tcLevel P) (hi : P l.node.entry) : P (prepare G tcLevel l).snd.snd.snd.snd

Persistent native bookkeeping invariants pass through the literal preparation sequence for either kind of sweep.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.selected {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {l : Loop n} (h : Frame.Valid G l.node) (hc : (visit (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry).fst < n) (hi : l.first = false → (classify (Graph.ofGraph G.graph) l.node.level (prepareOther (Graph.ofGraph G.graph) tcLevel l.node.level l.node.numcells l.node.entry).fst (prepareOther (Graph.ofGraph G.graph) tcLevel l.node.level l.node.numcells l.node.entry).snd.snd.snd.snd.snd).fst = Generic.Leaf.internal) : Cell.Valid G (cell G.graph tcLevel l) ∧ (prepare G.graph tcLevel l).snd.snd.fst = (cell G.graph tcLevel l).vertices

Internal native preparation selects the whole actual cell. Off-path classification supplies the enabled target guard, without assuming an unhinted target or any search-maximum theorem.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.child {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (l : Loop n) (st : State n) (bs : List Nat) (cell : VSet n) (tv : Nat) : Parent.child G tcLevel (parent G tcLevel l st bs cell tv) = (Loop.cell G tcLevel l).child l.first st tv

The generic child entry is literally the individualization represented by the complete selected cell, with the parent's current native state.

theorem Hex.GraphIso.Nauty.Sparse.Max.Loop.vertex_key {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {l : Loop n} {st : State n} {bs : List Nat} {cell : VSet n} {tv v : Nat} (hc : Cell.Valid G (Loop.cell G.graph tcLevel l)) (he : FrameOut G l.node.level l.node.level (Loop.cell G.graph tcLevel l).entry st) (hs : Ready G l.node.level (Loop.cell G.graph tcLevel l).numcells st) (hv : (Loop.cell G.graph tcLevel l).vertices.mem v = true) : Parent.key G.graph tcLevel (parent G.graph tcLevel l st bs cell tv) v = Cell.key G.graph tcLevel (Loop.cell G.graph tcLevel l) v

Recovered sibling order changes neither the actual selected target's vertex key nor the child subtree represented by that key.