theorem Hex.GraphIso.Nauty.Generation.match_prep {n : Nat} {st : SearchSt n} {level code : Nat} (hlevel : st.eqlevFirst = level - 1) (hcode : code = st.firstcode[level]!) : (otherNodePrep level code st).eqlevFirst = level

A matching next refinement code advances the first-reference comparison, regardless of the canonical-incumbent comparison.

theorem Hex.GraphIso.Nauty.Generation.match_recover {n : Nat} {st : SearchSt n} {level inf : Nat} (hlevel : level ≤ st.eqlevFirst) : (recover n inf level st).eqlevFirst = level

Recovering a matching ancestor keeps the first-reference comparison live at precisely that ancestor.

theorem Hex.GraphIso.Nauty.Generation.match_target {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level tcLevel : Nat} (heq : Equitable ctx level lab ptn) (hlab : LabOk lab n) (hlsz : lab.size = n) (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) {hint : Int} (hhint : hint = Int.ofNat (specTargetcell ctx lab ptn level tcLevel)) : Int.ofNat (maketargetcell ctx lab ptn level tcLevel hint).fst = hint

A first-reference target hint equal to the specification's choice cannot demote the first-reference comparison.

theorem Hex.GraphIso.Nauty.Generation.isautom_of_checked {n : Nat} {ctx : Ctx n} {γ : Array Nat} (hsize : ctx.g.size = n) (h : checkAutom ctx.g γ = true) : isautom ctx γ = true

The row checker implies the executable automorphism scan.

theorem Hex.GraphIso.Nauty.Generation.scatter_renaming {n : Nat} {ref : Array Nat} (σ : Renaming n) (hsize : ref.size = n) (hperm : ref.toList.Perm (List.range n)) : firstScatter n ref (Array.map σ.toFun ref) = renamingArray σ

Scattering a permutation labelling onto its renamed copy reconstructs the renaming's complete array.

theorem Hex.GraphIso.Nauty.Generation.match_emits {n k : Nat} {G : Colored n k} {st : SearchSt n} {level : Nat} {p : Perm n} (hp : IsIso G G p) (hsize : st.firstlab.size = n) (hperm : st.firstlab.toList.Perm (List.range n)) (hlab : st.lab = Array.map (renamingOf p).toFun st.firstlab) (hlevel : st.eqlevFirst = level) (hsent : st.firstcode[level + 1]! = codeSentinel) : (processnode { g := rowsOf G } level n st).snd.genTrace = st.genTrace.push (renamingArray (renamingOf p))

Reaching the renamed first-reference leaf emits that exact permutation, even if the canonical incumbent is strictly greater.