theorem
Hex.GraphIso.Nauty.compareCodes_eqlev
{n : Nat}
(level code : Nat)
(st : Search n)
:
(compareCodes level code st).eqlevFirst = if st.eqlevFirst = level - 1 ∧ code = st.firstcode[level]! then level else st.eqlevFirst
First-code comparison advances only from agreement at the preceding level.
theorem
Hex.GraphIso.Nauty.divergencePolicy
{n : Nat}
(ctx : Ctx n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy ctx inf tcLevel bound fun (st : Search n) => st.eqlevFirst < bound
Once first-code agreement has diverged above a frame, descendants cannot restore it.
theorem
Hex.GraphIso.Nauty.node_diverged
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells bound : Nat}
{st : Search n}
(hlevel : bound < level)
(h : st.eqlevFirst < bound)
:
An off-path call retains divergence above its entry frame.
theorem
Hex.GraphIso.Nauty.sweep_diverged
{n : Nat}
{ctx : Ctx n}
{first : Bool}
{inf tcLevel fuel cfuel level numcells tc tv1 index bound : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
(hpast : Generic.Past first tv1 cursor)
(hlevel : bound ≤ level)
(h : st.eqlevFirst < bound)
:
(sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.eqlevFirst < bound
Later siblings retain divergence above their parent frame.
theorem
Hex.GraphIso.Nauty.leafExit_noncheap
{n : Nat}
{κ : Type}
(leaf : Leaf)
(level : Nat)
(st : SearchState n κ)
:
Classifying or acting on a leaf does not move the cheap boundary.
theorem
Hex.GraphIso.Nauty.recover_noncheap
{n : Nat}
{κ : Type}
(inf level : Nat)
(st : SearchState n κ)
:
(recover inf level st).noncheaplevel = if level < st.noncheaplevel then level + 1 else st.noncheaplevel
Recovery leaves a failed guard strictly below the recovered parent.
theorem
Hex.GraphIso.Nauty.noncheapPolicy
{n : Nat}
(ctx : Ctx n)
(inf tcLevel bound : Nat)
:
Generic.BoundedPolicy ctx inf tcLevel bound fun (st : Search n) => bound < st.noncheaplevel
Searching below a noncheap ancestor cannot turn that ancestor cheap.
theorem
Hex.GraphIso.Nauty.node_noncheap
{n : Nat}
{ctx : Ctx n}
{inf tcLevel fuel level numcells bound : Nat}
{st : Search n}
(hlevel : bound < level)
(h : bound < st.noncheaplevel)
:
A noncheap ancestor stays noncheap throughout an off-path descendant call.
theorem
Hex.GraphIso.Nauty.sweep_noncheap
{n : Nat}
{ctx : Ctx n}
{first : Bool}
{inf tcLevel fuel cfuel level numcells tc tv1 index bound : Nat}
{cursor : Option Nat}
{cell : VSet n}
{st : Search n}
(hpast : Generic.Past first tv1 cursor)
(hlevel : bound ≤ level)
(h : bound < st.noncheaplevel)
:
bound < (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.noncheaplevel
A later-sibling sweep preserves the failed guard at an ancestor.