theorem
Hex.GraphIso.Nauty.firstFloor
{n : Nat}
(ctx : Ctx n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy ctx inf tcLevel bound fun (st : Search n) => bound ≤ st.allsamelevel ∧ bound ≤ st.eqlevFirst
Operations at or below a frame retain its lower bound on the all-same boundary and first-reference agreement.
theorem
Hex.GraphIso.Nauty.firstPath_floor
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells last : Nat}
{st leaf : Search n}
(hp : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf)
:
The first leaf installs both bounds, and every enclosing first sweep preserves them down to its own entry level.
theorem
Hex.GraphIso.Nauty.sweep_same
{n : Nat}
(ctx : Ctx n)
(inf tcLevel fuel cfuel level numcells tc tv1 : Nat)
(cursor : Option Nat)
(cell : VSet n)
(index : Nat)
(st : Search n)
:
Generic.Past true tv1 cursor →
(sweep true ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.allsamelevel = st.allsamelevel
Later first-path siblings leave the all-same boundary unchanged, even if a child returns past the current frame.