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

The full chosen-cell bound, including vertices subsequently filtered out.

Equations

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

def Hex.GraphIso.Nauty.Max.Remaining {n : Nat} (cursor : Option Nat) (cell : VSet n) (v : Nat) : Prop

A cursor names the next vertex to consider, not the previous vertex.

Equations

• Hex.GraphIso.Nauty.Max.Remaining cursor cell v = (cell.mem v = true ∧ ∃ (tv : Nat), cursor = some tv ∧ tv ≤ v)

structure Hex.GraphIso.Nauty.Max.SweepInput {n k : Nat} (G : Colored n k) (ctx : Ctx n) (tcLevel fuel cfuel : Nat) (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : Search n) (l : Loop n) (bs fs : List Nat) (parents : Parents n) : Prop

A sweep starts before its first leaf or resumes with both comparisons initialized. Both cases retain coverage in the original target window.

• node : Frame.Valid G l.node
• first_eq : first = l.first
• level_eq : level = l.node.level
• numcells_eq : numcells = (Loop.prepare ctx tcLevel l).fst
• tc_eq : tc = (Loop.prepare ctx tcLevel l).snd.fst.toNat
• tv1_eq : tv1 = ((Loop.prepare ctx tcLevel l).snd.snd.fst.nextElem none).getD 0
• origin : ∃ (bs₀ : List Nat), ∃ (fs₀ : List Nat), Entry G ctx tcLevel first l.node bs₀ fs₀
• base : SearchOk G level numcells (Loop.prepare ctx tcLevel l).snd.snd.snd.snd
• partition : SearchOk G level numcells st
• effect : SearchOut G level level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd st
• equitable : Equitable ctx level st.lab st.ptn
• target : Generic.Target (fun (st : Search n) => st) level tc cell st
• window : IsCell (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst
• len : 2 ≤ (Loop.prepare ctx tcLevel l).snd.snd.snd.fst
• range : tc + (Loop.prepare ctx tcLevel l).snd.snd.snd.fst ≤ n
• subset (v : Nat) : cell.mem v = true → (windowSet n (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst).mem v = true
• cursor_mem (tv : Nat) : cursor = some tv → cell.mem tv = true
• fuel : n ≤ level + fuel
• cursor_fuel : Generic.CursorFuel n cfuel cursor
• path : PathInv G ctx level st
• choice : Loop.Choice ctx tcLevel l (SearchState.key ctx bs st)
• small : st.noncheaplevel ≤ level → SubtreeOk ctx level { lab := st.lab, ptn := st.ptn, active := st.active, numcells := numcells, hint := 0, maxpos := 0, longcode := 0 }
• phase : first = true ∧ bs = [] ∧ fs = [] ∧ st = (Loop.prepare ctx tcLevel l).snd.snd.snd.snd ∧ cell = (Loop.prepare ctx tcLevel l).snd.snd.fst ∧ cursor = cell.nextElem none ∧ index = 0 ∨ SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st ∧ Comparison ctx (Loop.codes ctx l) bs fs st ∧ (st.compCanon ≤ 0 ∨ first = false ∧ cursor.isSome = true)
• coverage : CellCover ctx tcLevel (n - level) level numcells tc (Loop.prepare ctx tcLevel l).snd.snd.snd.fst (Loop.codes ctx l) (Loop.prepare ctx tcLevel l).snd.snd.snd.snd (Remaining cursor cell) (SearchState.key ctx bs st)
• canonical : CanonGuide level tc (Loop.prepare ctx tcLevel l).snd.snd.snd.snd (Loop.key ctx tcLevel l) (SearchState.key ctx bs st) st
• first_ref : st.gcaFirst = level → Generic.Covers (Loop.key ctx tcLevel l st.firstlab[tc]!) (SearchState.key ctx bs st) ∧ cellsPerm (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab st.firstlab
• generators : first = true → ∀ (γ : Array Nat), γ ∈ st.genTrace → CellStab (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.ptn level (Loop.prepare ctx tcLevel l).snd.snd.snd.snd.lab γ
• scope : Scope G ctx tcLevel level (Loop.codes ctx l) bs st parents
• parent : 1 < level → ∃ (p : Parent n), parents (level - 1) = some p ∧ Parent.child ctx tcLevel p = l.node
• counters : 0 < st.canonlevel → 0 < st.gcaFirst ∧ st.gcaFirst ≤ st.gcaCanon
• control : 0 < st.canonlevel → (first = true → st.gcaFirst = level) ∧ (first = false → st.gcaFirst < level)

def Hex.GraphIso.Nauty.Max.keyContract {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Generic.Contract (Search n) n

The maximum contract uses ghost incumbent codes at entry and a settled executable incumbent at return. Each nonlocal witness names a frozen ancestor subtree rather than the current child by assumption.

Equations

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

def Hex.GraphIso.Nauty.Max.contract {n k : Nat} (G : Colored n k) (tcLevel : Nat) : Generic.Contract (Search n) n

The single recursive contract combines key bounds with preservation of every accumulated generator at each surviving first ancestor.

Equations

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

theorem Hex.GraphIso.Nauty.Max.node_zero {n k : Nat} (G : Colored n k) (tcLevel : Nat) (first : Bool) (level numcells : Nat) (st : Search n) : (contract G tcLevel).nodePost 0 first level numcells st (Generic.Exit.fuel, st)

A node with no executable fuel cannot satisfy the adequate-fuel input.

theorem Hex.GraphIso.Nauty.Max.sweep_zero {n k : Nat} (G : Colored n k) (tcLevel fuel : Nat) (first : Bool) (level numcells tc tv1 tv : Nat) (cell : VSet n) (index : Nat) (st : Search n) : (contract G tcLevel).sweepPost fuel 0 first level numcells tc tv1 (some tv) cell index st (Generic.Exit.fuel, index, st)

A live cursor with zero sweep fuel cannot satisfy its iteration bound.