theorem Hex.GraphIso.Nauty.Generation.match_prep {n : Nat} {st : Search n} {level code : Nat} (hlevel : st.eqlevFirst = level - 1) (hcode : code = st.firstcode[level]!) : (compareCodes 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 : Search n} {level inf : Nat} (hlevel : level ≤ st.eqlevFirst) : (recover 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.