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

The local invariants at an actual off-path node. Its saved ancestors retain reference coverage, cursor ranks and trace stabilization; none of these fields assumes the node's search result.

• frame : Frame.Valid G f
• codes : CodeEntry G tcLevel f.level f.numcells f.entry
• pairs : PairsEntry G tcLevel f.level f.numcells f.entry
• machine : Comparison G.graph f.codes bs fs f.entry
• scope : Scope G tcLevel f bs f.entry parents
• guides : Guides G.graph tcLevel f.entry parents
• cosets : Cosets f.entry parents
• ranked (t : Nat) (p : Parent n) : parents t = some p → Parent.Ranked G.graph tcLevel p
• traces : Traces G f.entry parents
• orbits : OrbitTrace G f.entry
• counters : 0 < f.entry.gcaFirst ∧ f.entry.gcaFirst ≤ f.entry.gcaCanon ∧ f.entry.gcaCanon < f.level
• capacity : 0 < f.entry.wsCap

structure Hex.GraphIso.Nauty.Sparse.Max.SweepInput {n k : Nat} (G : Sparse.Colored n k) (tcLevel : Nat) (l : Loop n) (bs fs : List Nat) (cursor : Option Nat) (cell : VSet n) (st : State n) (parents : Parents n) : Prop

A native sweep after its first leaf exists. Coverage refers to the complete actual selected cell and its current cursor; all machine fields refer to the executed state after preparation or child recovery.

• frame : Frame.Valid G l.node
• internal : (visit (Graph.ofGraph G.graph) l.node.level l.node.numcells l.node.entry).fst < n
• selected : Cell.Valid G (Loop.cell G.graph tcLevel l)
• codes : CodeReady G tcLevel l.node.level (Loop.cell G.graph tcLevel l).numcells st
• pairs : PairsReady G tcLevel l.node.level (Loop.cell G.graph tcLevel l).numcells st
• machine : Comparison G.graph (Loop.cell G.graph tcLevel l).codes bs fs st
• effect : FrameOut G l.node.level l.node.level (Loop.cell G.graph tcLevel l).entry st
• target : Generic.Target State.frame l.node.level (Loop.cell G.graph tcLevel l).tc cell st
• subset (v : Nat) : cell.mem v = true → (Loop.cell G.graph tcLevel l).vertices.mem v = true
• member (v : Nat) : cursor = some v → cell.mem v = true
• choice : Frame.Choice G.graph tcLevel l.node (Loop.cell G.graph tcLevel l).tc (State.key G.graph bs st)
• small : st.noncheaplevel ≤ l.node.level → NodeShape n l.node.level st.ptn
• scope : Scope G tcLevel l.node bs st parents
• guides : Guides G.graph tcLevel st parents
• cosets : Cosets st parents
• ranked (t : Nat) (p : Parent n) : parents t = some p → Parent.Ranked G.graph tcLevel p
• traces : Traces G st parents
• orbits : OrbitTrace G st
• self : l.first = true → TraceFrame G l.node.level st st
• guided (v : Nat) : Parent.Guided G.graph tcLevel (Loop.parent G.graph tcLevel l st bs cell v)
• counters : 0 < st.gcaFirst ∧ st.gcaFirst ≤ st.gcaCanon ∧ st.gcaCanon ≤ l.node.level
• first : l.first = true → st.gcaFirst = l.node.level
• other : l.first = false → st.gcaFirst < l.node.level
• capacity : 0 < st.wsCap
• recorded : CheapRecorded l.node.level (Loop.cell G.graph tcLevel l).tc st
• route : RouteRecorded G.graph tcLevel l.node.level (Loop.cell G.graph tcLevel l).tc st
• cover : Cell.Cover G.graph tcLevel (Loop.cell G.graph tcLevel l) (Remaining cursor cell) (State.key G.graph bs st)
• phase : st.compCanon ≤ 0 ∨ l.first = false ∧ cursor.isSome = true

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.parent {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {l : Loop n} {bs fs : List Nat} {cursor : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) {tv : Nat} (hv : cell.mem tv = true) : Parent.Valid G tcLevel (Loop.parent G.graph tcLevel l st bs cell tv)

A live cursor suspends a valid parent with the literal selected coordinate. The frozen unhinted target is used only in its choice rule.

theorem Hex.GraphIso.Nauty.Sparse.Max.SweepInput.child {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {l : Loop n} {bs fs : List Nat} {cursor : Option Nat} {cell : VSet n} {st : State n} {parents : Parents n} (h : SweepInput G tcLevel l bs fs cursor cell st parents) {tv : Nat} (htv : cursor = some tv) : have p := Loop.parent G.graph tcLevel l st bs cell tv; NodeInput G tcLevel (Parent.child G.graph tcLevel p) bs fs (parents.push p)

Selecting the current cursor assembles every off-path child invariant from the native sweep state. In particular its suspended rank comes from the actual filtered-cell coverage, and first-ancestor stabilization is transported through the executed individualization.

def Hex.GraphIso.Nauty.Sparse.Max.NodeMax {n k : Nat} (G : Sparse.Colored n k) (tcLevel fuel : Nat) : Prop

The coverage induction concerns the literal native off-path call, with only smaller recursion bounds used as induction hypotheses.

Equations

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