def Hex.GraphIso.Nauty.SearchState.canonical {n : Nat} {κ : Type} (st : SearchState n κ) : Array Nat × Nat × Int × Int × Array Nat × κ × Nat

Canonical fields affected by a leaf verdict. Admission and return bookkeeping preserve this projection.

Equations

• st.canonical = (st.canoncode, st.canonlevel, st.eqlevCanon, st.compCanon, st.canonlab, st.canong, st.samerows)

def Hex.GraphIso.Nauty.resolve {n : Nat} {κ : Type} (level : Nat) (r : Leaf × SearchState n κ) : SearchState n κ

The canonical effect of a classified leaf, independent of its exit.

Equations

• Hex.GraphIso.Nauty.resolve level r = match r.fst with | Hex.GraphIso.Nauty.Generic.Leaf.better sr => Hex.GraphIso.Nauty.install level sr r.snd | x => r.snd

theorem Hex.GraphIso.Nauty.leafExit_canonical {n : Nat} {κ : Type} (leaf : Leaf) (level : Nat) (st : SearchState n κ) : (leafExit leaf level st).snd.canonical = (resolve level (leaf, st)).canonical

Only a better verdict changes canonical fields after classification.

theorem Hex.GraphIso.Nauty.Settled.canonical {n : Nat} {κ : Type} {cs bs : List Nat} {st out : SearchState n κ} (h : Settled cs bs st) (he : out.canonical = st.canonical) : Settled cs bs out

Canonical-field equality preserves the settled comparison machine.

theorem Hex.GraphIso.Nauty.key_canonical {n : Nat} {κ : Type} {ctx : Ctx n} {bs : List Nat} {st out : SearchState n κ} (he : out.canonical = st.canonical) : SearchState.key ctx bs out = SearchState.key ctx bs st

Canonical-field equality preserves every ghost incumbent.

theorem Hex.GraphIso.Nauty.canonVerdict_short {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon = 0) (hshort : cs.length < st.canonlevel) (hlen : cs.length ≤ n) : have out := resolve cs.length (canonVerdict ctx cs.length st); incKey ctx cs out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs cs out

Canonical classification of a code-tied leaf at a shorter depth installs the candidate, since its sentinel precedes a real incumbent code.

theorem Hex.GraphIso.Nauty.canonVerdict_greater {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon = 1) (hlen : cs.length ≤ n) : have out := resolve cs.length (canonVerdict ctx cs.length st); incKey ctx cs out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs cs out

A frozen upward code comparison installs the candidate independently of its adjacency rows.

theorem Hex.GraphIso.Nauty.canonVerdict_less {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon = -1) : have out := resolve cs.length (canonVerdict ctx cs.length st); incKey ctx bs out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs bs out

A frozen downward code comparison retains the incumbent independently of its adjacency rows.

theorem Hex.GraphIso.Nauty.canonVerdict_rows {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hc : st.compCanon = 0) (hlen : cs.length = bs.length) (hcache : CanongInv ctx st.canong st.canonlab st.samerows) : have out := resolve cs.length (canonVerdict ctx cs.length st); ∃ (bs' : List Nat), incKey ctx bs' out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs bs' out

At equal code paths, the adjacency-row comparison chooses the exact maximum and leaves a comparison machine that recovery can restore.

theorem Hex.GraphIso.Nauty.canonVerdict_max {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hlen : cs.length ≤ n) (hcache : CanongInv ctx st.canong st.canonlab st.samerows) : have out := resolve cs.length (canonVerdict ctx cs.length st); ∃ (bs' : List Nat), incKey ctx bs' out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs bs' out

Canonical leaf classification computes the incumbent maximum. The ghost codes survive the overwrite window and are readable after resolution.

theorem Hex.GraphIso.Nauty.Codes.nonpos {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hle : keyLe (pathLeafKey ctx cs st.lab) (incKey ctx bs st.canonlab)) : st.compCanon ≤ 0

A leaf bounded by the incumbent cannot have an upward frozen code verdict. This also applies to a first-reference automorphism return.

theorem Hex.GraphIso.Nauty.classify_max {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hlen : cs.length ≤ n) (hcache : CanongInv ctx st.canong st.canonlab st.samerows) (hfirst : (classify ctx cs.length n st).fst = Generic.Leaf.autoFirst → keyLe (pathLeafKey ctx cs st.lab) (incKey ctx bs st.canonlab)) : have out := resolve cs.length (classify ctx cs.length n st); ∃ (bs' : List Nat), incKey ctx bs' out.canonlab = keyMax (incKey ctx bs st.canonlab) (pathLeafKey ctx cs st.lab) ∧ Settled cs bs' out

All discrete classifications choose the incumbent maximum, provided a first-reference return is covered by its saved reference.

theorem Hex.GraphIso.Nauty.leaf_max {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hlen : cs.length ≤ n) (hcs : cs ≠ []) (hbs : bs ≠ []) (hcache : CanongInv ctx st.canong st.canonlab st.samerows) (hfirst : (classify ctx cs.length n st).fst = Generic.Leaf.autoFirst → keyLe (pathLeafKey ctx cs st.lab) (incKey ctx bs st.canonlab)) : have verdict := classify ctx cs.length n st; have out := (leafExit verdict.fst cs.length verdict.snd).snd; ∃ (bs' : List Nat), Settled cs bs' out ∧ SearchState.key ctx bs' out = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

The actual leaf action installs the optional incumbent maximum and returns its ghost codes with a recoverable comparison machine.

theorem Hex.GraphIso.Nauty.leaf_best {n : Nat} {ctx : Ctx n} {cs bs : List Nat} {st : Search n} (h : Codes cs bs st) (hlen : cs.length ≤ n) (hcs : cs ≠ []) (hbs : bs ≠ []) (hcache : CanongInv ctx st.canong st.canonlab st.samerows) (hfirst : (classify ctx cs.length n st).fst = Generic.Leaf.autoFirst → keyLe (pathLeafKey ctx cs st.lab) (incKey ctx bs st.canonlab)) : have verdict := classify ctx cs.length n st; SearchState.best ctx (leafExit verdict.fst cs.length verdict.snd).snd = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

After a leaf action the executable incumbent is the maximum; the proof uses ghost codes for the incoming overwrite window.