@[reducible, inline]

abbrev Hex.GraphIso.Nauty.FirstCodes {n : Nat} (cs fs : List Nat) (st : Search n) : Prop

The first-reference comparison at a current code path.

Equations

• Hex.GraphIso.Nauty.FirstCodes cs fs st = Hex.GraphIso.Nauty.FirstCodeInv n cs fs st.firstcode st.eqlevFirst

theorem Hex.GraphIso.Nauty.FirstCodes.congr {n : Nat} {cs fs : List Nat} {st out : Search n} (h : FirstCodes cs fs st) (hc : out.firstcode = st.firstcode) (he : out.eqlevFirst = st.eqlevFirst) : FirstCodes cs fs out

Changes outside the code machine preserve its meaning.

theorem Hex.GraphIso.Nauty.FirstCodes.compare {n : Nat} {cs fs : List Nat} {st : Search n} {code : Nat} (h : FirstCodes cs fs st) (hc : code < codeSentinel) : FirstCodes (cs ++ [code]) fs (compareCodes (cs.length + 1) code st)

Comparing a new refinement code extends the current first-code path.

theorem Hex.GraphIso.Nauty.FirstCodes.target {n : Nat} {ctx : Ctx n} {cs fs : List Nat} {st : Search n} (h : FirstCodes cs fs st) (tcLevel numcells : Nat) : FirstCodes cs fs (chooseTarget false ctx tcLevel cs.length numcells st).snd.snd.snd

Target selection can lower first-path agreement without changing its codes.

theorem Hex.GraphIso.Nauty.FirstCodes.classify {n : Nat} {ctx : Ctx n} {cs fs : List Nat} {st : Search n} (h : FirstCodes cs fs st) (numcells : Nat) : FirstCodes cs fs (Nauty.classify ctx cs.length numcells st).snd

Classification preserves the first-reference code comparison.

theorem Hex.GraphIso.Nauty.FirstCodes.leaf {n : Nat} {cs fs : List Nat} {st : Search n} (h : FirstCodes cs fs st) (leaf : Leaf) : FirstCodes cs fs (leafExit leaf cs.length st).snd

Leaf actions preserve the first-reference code comparison.

theorem Hex.GraphIso.Nauty.FirstCodes.recover {n : Nat} {cs fs : List Nat} {st : Search n} {level : Nat} (h : FirstCodes cs fs st) (hlen : level ≤ cs.length) (inf : Nat) : FirstCodes (List.take level cs) fs (Nauty.recover inf level st)

Recovery truncates the current path at the receiving ancestor.

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

The two comparisons and the saved first leaf's incumbent bound.

• canonical : Codes cs bs st

  Canonical-code comparison, with semantic codes during overwriting.

• first : FirstCodes cs fs st

  Agreement with the first reference's code path.

• nonempty : bs ≠ []

  An incumbent has already been installed.

• lower : keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab)

  The incumbent bounds the first leaf.

theorem Hex.GraphIso.Nauty.Comparison.congr {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st out : Search n} (h : Comparison ctx cs bs fs st) (hcc : out.canoncode = st.canoncode) (hcl : out.canonlevel = st.canonlevel) (hce : out.eqlevCanon = st.eqlevCanon) (hcmp : out.compCanon = st.compCanon) (hfc : out.firstcode = st.firstcode) (hfe : out.eqlevFirst = st.eqlevFirst) (hfl : out.firstlab = st.firstlab) (hcan : out.canonlab = st.canonlab) : Comparison ctx cs bs fs out

Changes outside both comparisons and both saved labels preserve their bounds.

theorem Hex.GraphIso.Nauty.Comparison.visit {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (level numcells : Nat) : Comparison ctx cs bs fs (Nauty.visit ctx level numcells st).snd.snd

Refinement changes neither saved reference nor either comparison machine.

theorem Hex.GraphIso.Nauty.Comparison.compare {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} {code : Nat} (h : Comparison ctx cs bs fs st) (hc : code < codeSentinel) (hlen : cs.length ≤ n) : Comparison ctx (cs ++ [code]) bs fs (compareCodes (cs.length + 1) code st)

The next refinement code advances both comparison machines.

theorem Hex.GraphIso.Nauty.Comparison.target {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (tcLevel numcells : Nat) : Comparison ctx cs bs fs (chooseTarget false ctx tcLevel cs.length numcells st).snd.snd.snd

Choosing the sweep target retains the canonical comparison and its lower bound.

theorem Hex.GraphIso.Nauty.Comparison.child {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (first : Bool) (level tc tv : Nat) : Comparison ctx cs bs fs (Nauty.child first level tc tv st)

Individualization changes no saved code or labelling.

theorem Hex.GraphIso.Nauty.Comparison.cheap {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (h : Comparison ctx cs bs fs st) (first : Bool) (level : Nat) : Comparison ctx cs bs fs (cheapCheck first level st)

The cheap guard preserves both comparisons and both references.

theorem Hex.GraphIso.Nauty.comparison_firstterminal {n : Nat} {ctx : Ctx n} {cs : List Nat} {st : Search n} (hne : cs ≠ []) (hcsize : st.canoncode.size = n + 2) (hfsize : st.firstcode.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) : Comparison ctx cs cs cs (firstterminal cs.length st)

The first leaf initializes both comparisons and bounds itself.

theorem Hex.GraphIso.Nauty.Comparison.leaf {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), Settled cs bs' out ∧ FirstCodes cs fs out ∧ bs' ≠ [] ∧ keyLe (incKey ctx fs out.firstlab) (incKey ctx bs' out.canonlab) ∧ SearchState.key ctx bs' out = some (incMax (SearchState.key ctx bs st) (pathLeafKey ctx cs st.lab))

A resolved leaf keeps both comparisons recoverable, retains the first-key bound, and installs the exact incumbent maximum.

theorem Hex.GraphIso.Nauty.comparison_recover {n : Nat} {ctx : Ctx n} {cs bs fs : List Nat} {st : Search n} (hc : Settled cs bs st) (hf : FirstCodes cs fs st) (hne : bs ≠ []) (hlower : keyLe (incKey ctx fs st.firstlab) (incKey ctx bs st.canonlab)) {level : Nat} (hlen : level ≤ cs.length) (inf : Nat) : Comparison ctx (List.take level cs) bs fs (recover inf level st)

At any receiving ancestor, a settled leaf restores both comparisons and their saved-reference bound.