theorem
Hex.GraphIso.Nauty.Sparse.compareCodes_eqlev
{n : Nat}
(level code : Nat)
(st : State n)
:
(compareCodes level code st).eqlevFirst = if st.eqlevFirst = level - 1 ∧ code = st.firstcode[level]! then level else st.eqlevFirst
The shared comparison advances only from agreement at the preceding level, applied to the actual native search state.
theorem
Hex.GraphIso.Nauty.Sparse.divergencePolicy
{n : Nat}
(g : Graph n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy g inf tcLevel bound fun (st : State n) => st.eqlevFirst < bound
Native descendants cannot restore first-code agreement lost strictly above their receiving ancestor.
theorem
Hex.GraphIso.Nauty.Sparse.node_diverged
{n : Nat}
{g : Graph n}
{inf tcLevel fuel level numcells bound : Nat}
{st : State n}
(hlevel : bound < level)
(h : st.eqlevFirst < bound)
:
theorem
Hex.GraphIso.Nauty.Sparse.sweep_diverged
{n : Nat}
{g : Graph n}
{first : Bool}
{inf tcLevel fuel cfuel level numcells tc tv1 index bound : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : State n}
(hpast : Generic.Past first tv1 cursor)
(hlevel : bound ≤ level)
(h : st.eqlevFirst < bound)
:
(Generic.sweep first g inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.eqlevFirst < bound