theorem
Hex.GraphIso.Nauty.Sparse.Max.first_drop
{n : Nat}
{G : SparseGraph n}
{inf tcLevel fuel level numcells last tv : Nat}
{st leaf : State n}
(hopen : (Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).fst ≠ n)
(htv : (Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true level
(Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv)
(hp :
have r := Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st;
Generic.FirstPath (Graph.ofGraph G) tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd)) last leaf)
(hsame : (Generic.node true (Graph.ofGraph G) inf tcLevel (fuel + 1) level numcells st).snd.allsamelevel ≤ level)
:
have r := Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st;
have ch :=
Generic.node true (Graph.ofGraph G) inf tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd));
have sr :=
Generic.sweep true (Graph.ofGraph G) 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 native all-same boundary requires the actual completed sweep to count its whole target and the guiding child's boundary to reach its entry. The order accumulator update has no effect on this implication.
theorem
Hex.GraphIso.Nauty.Sparse.Max.first_boundary
{n : Nat}
{G : SparseGraph n}
{inf tcLevel fuel level numcells tv : Nat}
{st : State n}
(hopen : (Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).fst ≠ n)
(htv : (Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).snd.snd.fst.nextElem none = some tv)
(horbit :
(cheapCheck true level
(Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st).snd.snd.snd.snd).orbits[tv]! = tv)
:
have r := Generic.prepareFirst (Graph.ofGraph G) tcLevel level numcells st;
have ch :=
Generic.node true (Graph.ofGraph G) inf tcLevel fuel (level + 1) (r.fst + 1)
(Generic.Policy.child true level r.snd.fst.toNat tv (cheapCheck true level r.snd.snd.snd.snd));
have out := Generic.node true (Graph.ofGraph G) inf tcLevel (fuel + 1) level numcells st;
out.snd.allsamelevel = level ∨ out.snd.allsamelevel = ch.snd.allsamelevel
A native first call either lowers the all-same boundary to its own level or retains precisely the guiding child's boundary.