theorem
Hex.GraphIso.Nauty.Max.Loop.bound_eq
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
(h : Frame.Valid G l.node)
(hcell :
IsCell (prepare ctx tcLevel l).snd.snd.snd.snd.ptn l.node.level (prepare ctx tcLevel l).snd.fst.toNat
(prepare ctx tcLevel l).snd.snd.snd.fst)
(hlen : 2 ≤ (prepare ctx tcLevel l).snd.snd.snd.fst)
(hrange : (prepare ctx tcLevel l).snd.fst.toNat + (prepare ctx tcLevel l).snd.snd.snd.fst ≤ n)
(hselected :
specTargetcell ctx (SearchState.refined ctx l.node.level l.node.numcells l.node.entry).lab
(SearchState.refined ctx l.node.level l.node.numcells l.node.entry).ptn l.node.level tcLevel = (prepare ctx tcLevel l).snd.fst.toNat)
:
At the specification target, the complete sweep bound is exactly its node's key, including the common refinement-code prefix.
theorem
Hex.GraphIso.Nauty.Max.Loop.bound_dominated
{n : Nat}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
(h : Comparison ctx (codes ctx l) bs fs (prepare ctx tcLevel l).snd.snd.snd.snd)
(hc : (prepare ctx tcLevel l).snd.snd.snd.snd.compCanon < 0)
:
Generic.Covers (bound ctx tcLevel l) (SearchState.key ctx bs (prepare ctx tcLevel l).snd.snd.snd.snd)
A downward code comparison bounds the actual sweep even when its hinted target differs from the specification's target.
theorem
Hex.GraphIso.Nauty.Max.Loop.comparison
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
(h : Frame.Valid G l.node)
(hf : l.first = false)
(he : Entry G ctx tcLevel l.first l.node bs fs)
:
Actual off-path preparation supplies the comparison of the sweep's full code prefix, also during upward code-storage overwrites.
theorem
Hex.GraphIso.Nauty.Max.Loop.node_bound
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
{bs fs : List Nat}
{after : Option (Key n)}
(h : Frame.Valid G l.node)
(he : Entry G ctx tcLevel l.first l.node bs fs)
(hcell :
IsCell (prepare ctx tcLevel l).snd.snd.snd.snd.ptn l.node.level (prepare ctx tcLevel l).snd.fst.toNat
(prepare ctx tcLevel l).snd.snd.snd.fst)
(hlen : 2 ≤ (prepare ctx tcLevel l).snd.snd.snd.fst)
(hrange : (prepare ctx tcLevel l).snd.fst.toNat + (prepare ctx tcLevel l).snd.snd.snd.fst ≤ n)
(hnc : (prepare ctx tcLevel l).fst < n)
(hb : Generic.Bounded (bound ctx tcLevel l) (SearchState.key ctx bs (prepare ctx tcLevel l).snd.snd.snd.snd) after)
:
Generic.Bounded (Frame.key ctx tcLevel l.node) (SearchState.key ctx bs l.node.entry) after
A sweep's upper bound implies the node's upper bound, using the actual code comparison in the dominated hinted arm.