def Hex.GraphIso.Nauty.Depth {n : Nat} {κ : Type} (last : Nat) (st : SearchState n κ) : Prop

First-code agreement remains above the sentinel after the first leaf.

Equations

• Hex.GraphIso.Nauty.Depth last st = (st.eqlevFirst ≤ last ∧ st.firstcode[last + 1]! = Hex.GraphIso.Nauty.codeSentinel)

theorem Hex.GraphIso.Nauty.Depth.mono {n : Nat} {κ : Type} {last : Nat} {st out : SearchState n κ} (h : Depth last st) (hle : out.eqlevFirst ≤ st.eqlevFirst) (href : out.reference = st.reference) : Depth last out

Lowering agreement while preserving the reference preserves its depth bound.

theorem Hex.GraphIso.Nauty.compareCodes_depth {n : Nat} {κ : Type} {last level code : Nat} {st : SearchState n κ} (h : Depth last st) (hcode : code < codeSentinel) : Depth last (compareCodes level code st)

A real refinement code cannot advance agreement through the saved sentinel.

theorem Hex.GraphIso.Nauty.chooseTarget_le {n : Nat} (ctx : Ctx n) (tcLevel level numcells : Nat) (st : Search n) : (chooseTarget false ctx tcLevel level numcells st).snd.snd.snd.eqlevFirst ≤ st.eqlevFirst

Target selection can only lower first-code agreement.

theorem Hex.GraphIso.Nauty.classify_eqlev {n : Nat} (ctx : Ctx n) (level numcells : Nat) (st : Search n) : (classify ctx level numcells st).snd.eqlevFirst = st.eqlevFirst

Classification preserves the first-code agreement counter.

theorem Hex.GraphIso.Nauty.leafExit_eqlev {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.eqlevFirst = st.eqlevFirst

Leaf actions preserve the first-code agreement counter.

theorem Hex.GraphIso.Nauty.recover_le {n : Nat} {κ : Type} (inf level : Nat) (st : SearchState n κ) : (recover inf level st).eqlevFirst ≤ st.eqlevFirst

Recovery can only lower first-code agreement.

theorem Hex.GraphIso.Nauty.depthPolicy {n : Nat} (ctx : Ctx n) (inf tcLevel last : Nat) : Generic.StablePolicy ctx inf tcLevel (Depth last) fun (code : Nat) => code < codeSentinel

The search preserves the sentinel depth bound on off-path calls and later siblings.

theorem Hex.GraphIso.Nauty.node_depth {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st : Search n} (h : Depth last st) : Depth last (node false ctx inf tcLevel fuel level numcells st).snd

An off-path node cannot extend agreement below the actual first leaf.

theorem Hex.GraphIso.Nauty.sweep_depth {n : Nat} {ctx : Ctx n} {first : Bool} {inf tcLevel fuel cfuel level numcells tc tv1 index last : Nat} {cursor : Option Nat} {cell : VSet n} {st : Search n} (h : Depth last st) (hpast : Generic.Past first tv1 cursor) : Depth last (sweep first ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd

Later siblings preserve the same bound, including during a first-path sweep.

theorem Hex.GraphIso.Nauty.firstPath_depth {n : Nat} {ctx : Ctx n} {inf tcLevel fuel level numcells last : Nat} {st leaf : Search n} (hpath : Generic.FirstPath ctx tcLevel fuel level numcells st last leaf) (hsize : st.firstcode.size = n + 2) (hlast : last ≤ n) : Depth last (node true ctx inf tcLevel fuel level numcells st).snd

A full first-path call retains the bound installed at its actual first leaf.