theorem
Hex.GraphIso.Nauty.Max.first_drop
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells last tv : Nat}
{st leaf : Search n}
(hopen : (Generic.prepareFirst ctx tcLevel level numcells st).fst ≠ n)
(htv : (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.fst.nextElem none = some tv)
(horbit : (cheapCheck true level (Generic.prepareFirst ctx tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv)
(hp :
have r := Generic.prepareFirst ctx tcLevel level numcells st;
Generic.FirstPath ctx tcLevel fuel (level + 1) (r.fst + 1)
(child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf)
(hsame : (node true ctx inf tcLevel (fuel + 1) level numcells st).snd.allsamelevel ≤ level)
:
have r := Generic.prepareFirst ctx tcLevel level numcells st;
have ch :=
node true ctx inf tcLevel fuel (level + 1) (r.fst + 1)
(child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd));
have sr :=
sweep true ctx inf tcLevel fuel (n + 1) level r.fst r.snd.fst.toNat tv (some tv) r.snd.snd.fst 0
(cheapCheck true level r.snd.snd.snd.snd);
sr.fst = Generic.Exit.done ∧ r.snd.snd.snd.fst = sr.snd.fst ∧ ch.snd.allsamelevel = level + 1
Lowering the all-same boundary requires the completed orbit count and a guiding child whose boundary has reached its own entry.
theorem
Hex.GraphIso.Nauty.Max.firstPath_uniform
{n k : Nat}
{G : Colored n k}
{tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hp : Generic.FirstPath { g := rowsOf G } tcLevel fuel level numcells st last leaf)
(hn : ∀ (f : Nat), f < fuel → (contract G tcLevel).nodeValid f (Generic.nodeCall { g := rowsOf G } (n + 2) tcLevel f))
{cs bs fs : List Nat}
{parents : Parents n}
(hi :
NodeInput G { g := rowsOf G } tcLevel fuel true { level := level, numcells := numcells, codes := cs, entry := st } bs
fs parents)
(hsame : (node true { g := rowsOf G } (n + 2) tcLevel fuel level numcells st).snd.allsamelevel ≤ level)
:
The all-same boundary is justified by actual counted carriers. The only search premises are contracts for strictly smaller node calls.