@[reducible, inline]

abbrev Hex.GraphIso.Nauty.Codes {n : Nat} {κ : Type} (cs bs : List Nat) (st : SearchState n κ) : Prop

The canonical comparison machine, including its ghost incumbent codes during an upward overwrite.

Equations

• Hex.GraphIso.Nauty.Codes cs bs st = Hex.GraphIso.Nauty.CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon st.compCanon

def Hex.GraphIso.Nauty.SearchState.best {n : Nat} {κ : Type} (ctx : Ctx n) (st : SearchState n κ) : Option (Key n)

The executable incumbent, read only when code storage is stable.

Equations

• One or more equations did not get rendered due to their size.

def Hex.GraphIso.Nauty.SearchState.key {n : Nat} {κ : Type} (ctx : Ctx n) (bs : List Nat) (st : SearchState n κ) : Option (Key n)

The semantic incumbent represented by a ghost code sequence.

Equations

• Hex.GraphIso.Nauty.SearchState.key ctx bs st = if bs = [] then none else some (Hex.GraphIso.Nauty.incKey ctx bs st.canonlab)

theorem Hex.GraphIso.Nauty.code_read {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} {comparison : Int} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon comparison) (hne : comparison ≠ 1) : List.map (fun (i : Nat) => st.canoncode[i]!) (List.range' 1 st.canonlevel) = bs

Stable code storage contains the ghost incumbent's entire code list.

theorem Hex.GraphIso.Nauty.best_eq_key {n : Nat} {κ : Type} {ctx : Ctx n} {cs bs : List Nat} {st : SearchState n κ} {comparison : Int} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon comparison) (hne : comparison ≠ 1) : SearchState.best ctx st = SearchState.key ctx bs st

The stable executable reading agrees with the semantic incumbent.

theorem Hex.GraphIso.Nauty.Codes.compare {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} {code : Nat} (h : Codes cs bs st) (hc : code < codeSentinel) (hlen : cs.length ≤ n) : Codes (cs ++ [code]) bs (compareCodes (cs.length + 1) code st)

Comparing the next refinement code extends the current path.

theorem Hex.GraphIso.Nauty.Codes.install {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} {comparison : Int} (h : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon comparison) (hne : comparison ≠ -1) (hlen : cs.length ≤ n) (sr : Nat) : Codes cs cs (Nauty.install cs.length sr st)

Installing a leaf makes its path the canonical code sequence. The premise describes code comparison before the row verdict repurposes it.

theorem Hex.GraphIso.Nauty.firstterminal_codes {n : Nat} {κ : Type} {cs : List Nat} {st : SearchState n κ} (hsize : st.canoncode.size = n + 2) (hlen : cs.length ≤ n) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) : Codes cs cs (firstterminal cs.length st)

The first leaf seeds the canonical comparison machine.

theorem Hex.GraphIso.Nauty.firstterminal_best {n : Nat} {κ : Type} {ctx : Ctx n} {cs : List Nat} {st : SearchState n κ} (hne : cs ≠ []) (hsize : st.canoncode.size = n + 2) (hlen : cs.length ≤ n) (hcodes : ∀ (i : Nat), 1 ≤ i → i ≤ cs.length → st.firstcode[i]! = cs[i - 1]!) (hlt : ∀ (c : Nat), c ∈ cs → c < codeSentinel) : SearchState.best ctx (firstterminal cs.length st) = some (pathLeafKey ctx cs st.lab)

The first installed incumbent is the reached leaf, with no placeholder key before it.

inductive Hex.GraphIso.Nauty.Settled {n : Nat} {κ : Type} (cs bs : List Nat) (st : SearchState n κ) : Prop

A completed leaf has either retained its code verdict or used a negative row verdict after full code agreement. Both forms recover to a canonical code machine at every earlier level.

• codes {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} (machine : Codes cs bs st) (nonpos : st.compCanon ≤ 0) : Settled cs bs st

  The code comparison itself remains valid.

• rows {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} (machine : CodeCmpInv n cs bs st.canoncode st.canonlevel st.eqlevCanon 0) (negative : st.compCanon < 0) : Settled cs bs st

  Row rejection changed the comparison value, with all codes tied.

theorem Hex.GraphIso.Nauty.Settled.read {n : Nat} {κ : Type} {ctx : Ctx n} {cs bs : List Nat} {st : SearchState n κ} (h : Settled cs bs st) : SearchState.best ctx st = SearchState.key ctx bs st

Either settled form exposes the same semantic incumbent.

theorem Hex.GraphIso.Nauty.Settled.congr {n : Nat} {κ : Type} {cs bs : List Nat} {st out : SearchState n κ} (h : Settled cs bs st) (hc : out.canoncode = st.canoncode) (hl : out.canonlevel = st.canonlevel) (he : out.eqlevCanon = st.eqlevCanon) (hp : out.compCanon = st.compCanon) : Settled cs bs out

A settled comparison can be reindexed across changes to other fields.

theorem Hex.GraphIso.Nauty.Settled.recover {n : Nat} {κ : Type} {cs bs : List Nat} {st : SearchState n κ} {level : Nat} (h : Settled cs bs st) (hlen : level ≤ cs.length) (inf : Nat) : Codes (List.take level cs) bs (Nauty.recover inf level st)

Recovering either settled leaf verdict truncates the current path and restores the ordinary canonical comparison invariant.