theorem
Hex.GraphIso.Nauty.Max.Loop.node_step
{n : Nat}
{ctx : Ctx n}
{tcLevel : Nat}
{l : Loop n}
(next : Generic.SweepFn (Search n) n)
(hfirst : l.first = true → (prepare ctx tcLevel l).fst ≠ n)
(hother :
l.first = false →
have p := prepareOther ctx tcLevel l.node.level l.node.numcells l.node.entry;
(classify ctx l.node.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal)
:
Generic.nodeStep ctx tcLevel next l.first l.node.level l.node.numcells l.node.entry = have p := prepare ctx tcLevel l;
have result :=
next l.first l.node.level p.fst p.snd.fst.toNat ((p.snd.snd.fst.nextElem none).getD 0) (p.snd.snd.fst.nextElem none)
p.snd.snd.fst 0 p.snd.snd.snd.snd;
match result.fst with
| Generic.Exit.done =>
(Generic.Exit.unwind (l.node.level - 1) false, afterSweep l.first l.node.level p.snd.snd.snd.fst result.snd.fst result.snd.snd)
| exit => (exit, result.snd.snd)
An internal node enters exactly the sweep described by its frozen frame.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.internal_result
{n k : Nat}
{G : Colored n k}
{tcLevel fuel : Nat}
{first : Bool}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G { g := rowsOf G } tcLevel (fuel + 1) first f bs fs parents)
(hs : (contract G tcLevel).sweepValid fuel (n + 1) (Generic.sweepCall { g := rowsOf G } (n + 2) tcLevel fuel (n + 1)))
(hfirst : first = true → (Generic.prepareFirst { g := rowsOf G } tcLevel f.level f.numcells f.entry).fst ≠ n)
(hother :
first = false →
have p := prepareOther { g := rowsOf G } tcLevel f.level f.numcells f.entry;
(classify { g := rowsOf G } f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.internal)
:
have ctx := { g := rowsOf G };
have result :=
Generic.nodeStep ctx tcLevel (Generic.sweepCall ctx (n + 2) tcLevel fuel (n + 1)) first f.level f.numcells f.entry;
Generic.Result (Frame.key ctx tcLevel f) (SearchState.key ctx bs f.entry) (SearchState.best ctx result.snd)
(f.level - 1) (Witness ctx tcLevel (Parents.frames ctx tcLevel parents)) result.fst
The initialized actual sweep supplies both bounds and the exact ancestor witness needed by its enclosing node.
The first internal branch satisfies its complete local maximum rule.
The off-path internal branch permits hinted dominated descent and positive comparison overwrites under the same maximum contract.