def Hex.GraphIso.Nauty.Sparse.Grows {n : Nat} (before after : Option (Key n)) : Prop

Native incumbent growth, including the absence of an incumbent before the first leaf. Parsed sparse keys are compared without row expansion.

Equations

• Hex.GraphIso.Nauty.Sparse.Grows before after = ∀ (b : Hex.GraphIso.Nauty.Sparse.Key n), before = some b → ∃ (a : Hex.GraphIso.Nauty.Sparse.Key n), after = some a ∧ b.Le a

theorem Hex.GraphIso.Nauty.Sparse.Grows.refl {n : Nat} (key : Option (Key n)) : Grows key key

theorem Hex.GraphIso.Nauty.Sparse.Grows.trans {n : Nat} {a b c : Option (Key n)} (hab : Grows a b) (hbc : Grows b c) : Grows a c

theorem Hex.GraphIso.Nauty.Sparse.Grows.some {n : Nat} {a b : Key n} (h : a.Le b) : Grows (Option.some a) (Option.some b)

structure Hex.GraphIso.Nauty.Sparse.ReturnCodes {n : Nat} (G : SparseGraph n) (stem bs fs : List Nat) (st : State n) : Prop

A completed native call retains settled comparisons on an extension of its entry path. Recovery truncates that path at the receiving ancestor.

• machine : ∃ (cs : List Nat), stem <+: cs ∧ Settled cs bs st ∧ FirstCodeInv n cs fs st.firstcode st.eqlevFirst
• nonempty : bs ≠ []
• lower : ∃ (f : Label n), ∃ (c : Label n), Label.ofArray? n st.firstlab = some f ∧ Label.ofArray? n st.canonlab = some c ∧ { codes := fs ++ [codeSentinel], graph := G.relabel f.perm }.Le { codes := bs ++ [codeSentinel], graph := G.relabel c.perm }

theorem Hex.GraphIso.Nauty.Sparse.Comparison.returned {n : Nat} {G : SparseGraph n} {cs bs fs : List Nat} {st : State n} (h : Comparison G cs bs fs st) (hn : st.compCanon ≤ 0) : ReturnCodes G cs bs fs st

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.prefix {n : Nat} {G : SparseGraph n} {stem cs bs fs : List Nat} {st : State n} (h : ReturnCodes G cs bs fs st) (hp : stem <+: cs) : ReturnCodes G stem bs fs st

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.read {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) : State.best G st = State.key G bs st

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.nonpos {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) : st.compCanon ≤ 0

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.fields {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st out : State n} (h : ReturnCodes G stem bs fs st) (hc : SearchState.canonical out = SearchState.canonical st) (hr : SearchState.reference out = SearchState.reference st) (he : out.eqlevFirst = st.eqlevFirst) : ReturnCodes G stem bs fs out

Bookkeeping that retains canonical and first-reference fields preserves the semantic comparison result, including both parsed labels.

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.leave {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) (tv : Nat) : ReturnCodes G stem bs fs (Generic.Policy.leaveChild tv st)

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.afterSweep {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) (first : Bool) (level size index : Nat) : ReturnCodes G stem bs fs (Generic.Policy.afterSweep first level size index st)

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.recover {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) (inf : Nat) : Comparison G stem bs fs (Generic.Policy.recover inf stem.length st)

Actual native recovery reconstructs both code machines at the exact entry prefix, even when the last compared leaf lay several levels below it.

theorem Hex.GraphIso.Nauty.Sparse.afterSweep_key {n : Nat} (G : SparseGraph n) (bs : List Nat) (first : Bool) (level size index : Nat) (st : State n) : State.key G bs (Generic.Policy.afterSweep first level size index st) = State.key G bs st

Finishing the actual native sweep changes no semantic incumbent.

theorem Hex.GraphIso.Nauty.Sparse.recover_nonpos {n : Nat} {st : State n} (h : st.compCanon ≤ 0) (inf level : Nat) : (Generic.Policy.recover inf level st).compCanon ≤ 0

Native recovery retains a settled comparison's nonpositive sign.

theorem Hex.GraphIso.Nauty.Sparse.ReturnCodes.resumed {n : Nat} {G : SparseGraph n} {stem bs fs : List Nat} {st : State n} (h : ReturnCodes G stem bs fs st) (inf : Nat) : ReturnCodes G stem bs fs (Generic.Policy.recover inf stem.length st)