theorem
Hex.GraphIso.Nauty.Max.Loop.prepare_key
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(l : Loop n)
(bs : List Nat)
:
SearchState.key ctx bs (prepare ctx tcLevel l).snd.snd.snd.snd = SearchState.key ctx bs l.node.entry
Sweep preparation retains the semantic incumbent, including when its code array is being overwritten by a better path.
theorem
Hex.GraphIso.Nauty.Max.Loop.choice
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
(hf : Frame.Valid G l.node)
(h : Entry G ctx tcLevel l.first l.node bs fs)
(hnc : (prepare ctx tcLevel l).fst < n)
:
Choice ctx tcLevel l (SearchState.key ctx bs l.node.entry)
Actual node preparation chooses the specification target or has already proved the whole node dominated by its incoming incumbent.
theorem
Hex.GraphIso.Nauty.Max.Loop.choice_prepared
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
(hf : Frame.Valid G l.node)
(h : Entry G ctx tcLevel l.first l.node bs fs)
(hnc : (prepare ctx tcLevel l).fst < n)
:
The target justification is initialized at the actual prepared sweep, with its current semantic incumbent rather than an assumed parent bound.
theorem
Hex.GraphIso.Nauty.Max.Parent.collapse
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{p : Parent n}
(h : Valid G ctx tcLevel p)
(hcheap : p.state.noncheaplevel ≤ p.loop.node.level)
(hgsz : ctx.g.size = n)
(hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u)
(hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false)
:
A cheap parent's entire specification is already covered or is exactly the subtree of its actual chosen child.