theorem Hex.GraphIso.Nauty.prefix_take {cs ds : List Nat} (h : cs <+: ds) {level : Nat} (hle : level ≤ cs.length) : List.take level ds = List.take level cs

Extending a descent cannot change a code prefix above the extension.

theorem Hex.GraphIso.Nauty.prefix_witness {n : Nat} {cs ds : List Nat} {target : Nat} {best : Option (Key n)} (hp : cs <+: ds) (ht : target < cs.length) (h : ∀ (tail : Key n), Generic.Covers (prefixKey (List.take (target + 1) ds) tail) best) (tail : Key n) : Generic.Covers (prefixKey (List.take (target + 1) cs) tail) best

A code-supported witness names the same ancestor after the current path is truncated, provided the ancestor's child code is retained.

structure Hex.GraphIso.Nauty.ReturnCodes {n : Nat} (ctx : Ctx n) (stem bs fs : List Nat) (st : Search n) : Prop

A completed call retains a settled comparison on an extension of its incoming code path. The receiving ancestor truncates that extension.

• machine : ∃ (cs : List Nat), stem <+: cs ∧ Settled cs bs st ∧ FirstCodes cs fs st

  The last compared path retains every incoming refinement code.

• nonempty : bs ≠ []
• lower : keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab)

theorem Hex.GraphIso.Nauty.Comparison.returned {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (hn : st.compCanon ≤ 0) : ReturnCodes ctx cs bs fs st

A stable comparison already supplies a return at its own code path.

theorem Hex.GraphIso.Nauty.Comparison.leaf_returned {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel : Nat} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (hh : History ctx tcLevel cs.length cs.length n st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hlevel : 1 ≤ cs.length) (hok : SearchOk G cs.length n st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) : have verdict := classify ctx cs.length n st; have out := (leafExit verdict.fst cs.length verdict.snd).snd; ∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs out ∧ SearchState.key ctx bs' out = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

The actual discrete leaf action supplies a settled return and its exact local maximum.

theorem Hex.GraphIso.Nauty.Comparison.prune_returned {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; ReturnCodes ctx cs bs fs out ∧ SearchState.key ctx bs out = SearchState.key ctx bs st

The actual nonterminal code rejection supplies a settled return and retains its incumbent.

theorem Hex.GraphIso.Nauty.Comparison.exit_returned {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel numcells : Nat} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (hh : History ctx tcLevel cs.length cs.length numcells st) (hinv : RunInv G ctx st) (hn0 : 0 < n) (hlevel : 1 ≤ cs.length) (hok : SearchOk G cs.length numcells st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u v : Nat), u < n → v < n → ctx.g[u]!.mem v = ctx.g[v]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hexit : (classify ctx cs.length numcells st).fst ≠ Generic.Leaf.internal) : have c := classify ctx cs.length numcells st; have out := (leafExit c.fst cs.length c.snd).snd; ∃ (bs' : List Nat), ReturnCodes ctx cs bs' fs out ∧ Generic.Grows (SearchState.key ctx bs st) (SearchState.key ctx bs' out)

Every terminal classification returns settled machines and preserves or increases the incumbent, including rejection before a discrete leaf.

theorem Hex.GraphIso.Nauty.ReturnCodes.prefix {n : Nat} {ctx : Ctx n} {stem cs bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx cs bs fs st) (hp : stem <+: cs) : ReturnCodes ctx stem bs fs st

A deeper call's code receipt also retains every prefix of its entry path.

theorem Hex.GraphIso.Nauty.ReturnCodes.read {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) : SearchState.best ctx st = SearchState.key ctx bs st

Every completed comparison exposes its ghost incumbent in executable storage.

theorem Hex.GraphIso.Nauty.ReturnCodes.nonpos {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) : st.compCanon ≤ 0

Completed comparisons are nonpositive, including a rejection by rows after a code tie.

theorem Hex.GraphIso.Nauty.ReturnCodes.fields {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st out : Search n} (h : ReturnCodes ctx stem bs fs st) (hc : SearchState.canonical out = SearchState.canonical st) (hr : SearchState.reference out = SearchState.reference st) (he : out.eqlevFirst = st.eqlevFirst) : ReturnCodes ctx stem bs fs out

Return bookkeeping preserves the complete comparison receipt.

theorem Hex.GraphIso.Nauty.ReturnCodes.leave {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) (tv : Nat) : ReturnCodes ctx stem bs fs { lab := st.lab, ptn := st.ptn, active := st.active, orbits := st.orbits, fixedpts := st.fixedpts.erase tv, autos := st.autos, wsCap := st.wsCap, firstcode := st.firstcode, canoncode := st.canoncode, firsttc := st.firsttc, firstlab := st.firstlab, canonlab := st.canonlab, canong := st.canong, samerows := st.samerows, compCanon := st.compCanon, eqlevFirst := st.eqlevFirst, eqlevCanon := st.eqlevCanon, gcaFirst := st.gcaFirst, gcaCanon := st.gcaCanon, canonlevel := st.canonlevel, noncheaplevel := st.noncheaplevel, allsamelevel := st.allsamelevel, cosetindex := st.cosetindex, stabvertex := st.stabvertex, numnodes := st.numnodes, tctotal := st.tctotal, canupdates := st.canupdates, numorbits := st.numorbits, numgenerators := st.numgenerators, numbadleaves := st.numbadleaves, maxlevel := st.maxlevel, order := st.order, genTrace := st.genTrace, workperm := st.workperm }

Removing a temporary fixed point changes no comparison or saved key.

theorem Hex.GraphIso.Nauty.ReturnCodes.afterSweep {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) (first : Bool) (level size index : Nat) : ReturnCodes ctx stem bs fs (Nauty.afterSweep first level size index st)

Completing a node's symmetry counter preserves its returned comparison.

theorem Hex.GraphIso.Nauty.recover_key {n : Nat} (ctx : Ctx n) (bs : List Nat) (inf level : Nat) (st : Search n) : SearchState.key ctx bs (recover inf level st) = SearchState.key ctx bs st

Recovery changes no semantic incumbent labelling.

theorem Hex.GraphIso.Nauty.afterSweep_key {n : Nat} (ctx : Ctx n) (bs : List Nat) (first : Bool) (level size index : Nat) (st : Search n) : SearchState.key ctx bs (afterSweep first level size index st) = SearchState.key ctx bs st

Finishing a sweep changes no semantic incumbent.

theorem Hex.GraphIso.Nauty.recover_nonpos {n : Nat} {st : Search n} (h : st.compCanon ≤ 0) (inf level : Nat) : (recover inf level st).compCanon ≤ 0

Parent recovery keeps a completed comparison nonpositive.

theorem Hex.GraphIso.Nauty.ReturnCodes.recover {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) (inf : Nat) : Comparison ctx stem bs fs (Nauty.recover inf stem.length st)

Recovery reconstructs both comparison machines at the receiving ancestor's exact code path, however deep the return originated.

theorem Hex.GraphIso.Nauty.ReturnCodes.resumed {n : Nat} {ctx : Ctx n} {stem bs fs : List Nat} {st : Search n} (h : ReturnCodes ctx stem bs fs st) (inf : Nat) : ReturnCodes ctx stem bs fs (Nauty.recover inf stem.length st)

Recovery supplies a settled receipt at the shortened path for the next sibling.