theorem Hex.GraphIso.Nauty.Codes.negative {n : Nat} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon < 0) : st.compCanon = -1

A negative comparison in a code machine has nauty's frozen value.

theorem Hex.GraphIso.Nauty.Codes.prefix_le {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon < 0) (key : Key n) : keyLe (prefixKey cs key) (incKey ctx bs st.canonlab)

Every extension of a downward-frozen current path is bounded by the incumbent.

theorem Hex.GraphIso.Nauty.Codes.ancestor_le {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon < 0) {level : Nat} (hlevel : st.eqlevCanon.toNat < level) (hlen : level ≤ cs.length) (key : Key n) : keyLe (prefixKey (List.take level cs) key) (incKey ctx bs st.canonlab)

A frozen comparison also bounds every ancestor child below the first unequal code, independently of any later target choices.

theorem Hex.GraphIso.Nauty.Codes.subtree_le {n : Nat} {ctx : Ctx n} {stem bs : List Nat} {st : Search n} {lab ptn : Array Nat} {active : VSet n} {numcells level : Nat} (h : Codes (stem ++ [(refine ctx level lab ptn active numcells).longcode]) bs st) (hc : st.compCanon < 0) (tcLevel fuel : Nat) : keyLe (prefixKey stem (specNode ctx tcLevel (fuel + 1) level lab ptn active numcells)) (incKey ctx bs st.canonlab)

Once refinement freezes the comparison downward, its entire specification subtree is bounded, including the newly compared code.

theorem Hex.GraphIso.Nauty.classify_pruned {n : Nat} {ctx : Ctx n} {level numcells : Nat} {st : Search n} (hnc : numcells ≠ n) (hbad : (classify ctx level numcells st).fst = Generic.Leaf.bad) : st.compCanon < 0 ∧ classify ctx level numcells st = (Generic.Leaf.bad, st)

A non-discrete rejected node was rejected by codes before any row comparison.

theorem Hex.GraphIso.Nauty.Comparison.prune {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} {numcells : Nat} (h : Comparison ctx cs bs fs st) (hnc : numcells ≠ n) (hbad : (classify ctx cs.length numcells st).fst = Generic.Leaf.bad) : have verdict := classify ctx cs.length numcells st; have out := (leafExit verdict.fst cs.length verdict.snd).snd; Settled cs bs out ∧ FirstCodes cs fs out ∧ SearchState.key ctx bs out = SearchState.key ctx bs st ∧ keyLe (incKey ctx fs out.firstlab) (incKey ctx bs out.canonlab)

Code pruning retains the incumbent and returns a settled machine; it does not install a key from the unvisited subtree.

theorem Hex.GraphIso.Nauty.pruneReturn_target {n : Nat} {κ : Type} (level : Nat) (st : SearchState n κ) : ∃ (target : Nat), ∃ (short : Bool), (pruneReturn level st).fst = Generic.Exit.unwind target short ∧ (st.eqlevCanon.toNat ≤ target ∨ target = st.noncheaplevel - 1)

The shared prune tail returns below the frozen comparison's receiving level only when the cheap boundary supplies its target.

theorem Hex.GraphIso.Nauty.Comparison.prune_witness {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} {numcells target : Nat} (h : Comparison ctx cs bs fs st) (hnc : numcells ≠ n) (hbad : (classify ctx cs.length numcells st).fst = Generic.Leaf.bad) (htarget : st.eqlevCanon.toNat ≤ target) : have out := (leafExit Generic.Leaf.bad cs.length st).snd; ∀ (t : Nat), target ≤ t → t < cs.length → ∀ (key : Key n), keyLe (prefixKey (List.take (t + 1) cs) key) (incKey ctx bs out.canonlab)

A downward code prune bounds each ancestor child at and above its receiving level. The prefix includes that child's code, one level below the receiving sweep, so it retains the first unequal comparison.

theorem Hex.GraphIso.Nauty.Comparison.prune_result {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} {numcells target : Nat} {short : Bool} (h : Comparison ctx cs bs fs st) (hnc : numcells ≠ n) (hbad : (classify ctx cs.length numcells st).fst = Generic.Leaf.bad) (hexit : (leafExit Generic.Leaf.bad cs.length st).fst = Generic.Exit.unwind target short) (hlevel : 0 < cs.length) (ht : target ≤ cs.length - 1) (htarget : st.eqlevCanon.toNat ≤ target) (key : Key n) : have out := leafExit Generic.Leaf.bad cs.length st; Generic.Result (prefixKey cs key) (SearchState.key ctx bs st) (SearchState.key ctx bs out.snd) (cs.length - 1) (fun (t : Nat) (best : Option (Key n)) => ∀ (tail : Key n), Generic.Covers (prefixKey (List.take (t + 1) cs) tail) best) out.fst

A code-supported prune has the generic fragment bound and transports semantic ancestor coverage through its actual nonlocal exit. The cheap return below the unequal code is a separate local obligation.