theorem
Hex.GraphIso.Nauty.Sparse.canonVerdict_max
{n : Nat}
{G : SparseGraph n}
{cs bs : List Nat}
{st : State n}
{l c : Label n}
(h : Codes cs bs st)
(hlen : cs.length ≤ n)
(hl : Label.ofArray? n st.lab = some l)
(hc : Label.ofArray? n st.canonlab = some c)
(hR : st.canong.Prefix (G.relabel c.perm) st.samerows)
:
have out := resolve cs.length (canonVerdict (Graph.ofGraph G) cs.length st);
∃ (bs' : List Nat), ∃ (d : Label n), Label.ofArray? n out.canonlab = some d ∧ { codes := bs' ++ [codeSentinel], graph := G.relabel d.perm } = { codes := bs ++ [codeSentinel], graph := G.relabel c.perm }.max
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm } ∧ Settled cs bs' out
Native canonical classification chooses the exact maximum of the incoming incumbent and candidate. The returned codes describe the actual installed label, including the code overwrite window and row rejection.
theorem
Hex.GraphIso.Nauty.Sparse.codes_nonpos
{n : Nat}
{G : SparseGraph n}
{cs bs : List Nat}
{st : State n}
{l c : Label n}
(h : Codes cs bs st)
(hle :
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm }.Le
{ codes := bs ++ [codeSentinel], graph := G.relabel c.perm })
:
A candidate bounded by the incumbent cannot have an upward frozen code verdict, including when first-reference admission skips row scanning.
theorem
Hex.GraphIso.Nauty.Sparse.classify_max
{n : Nat}
{G : SparseGraph n}
{cs bs : List Nat}
{st : State n}
{l c : Label n}
(h : Codes cs bs st)
(hlen : cs.length ≤ n)
(hl : Label.ofArray? n st.lab = some l)
(hc : Label.ofArray? n st.canonlab = some c)
(hR : st.canong.Prefix (G.relabel c.perm) st.samerows)
(hfirst :
(classify (Graph.ofGraph G) cs.length n st).fst = Generic.Leaf.autoFirst →
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm }.Le
{ codes := bs ++ [codeSentinel], graph := G.relabel c.perm })
:
have out := resolve cs.length (classify (Graph.ofGraph G) cs.length n st);
∃ (bs' : List Nat), ∃ (d : Label n), Label.ofArray? n out.canonlab = some d ∧ { codes := bs' ++ [codeSentinel], graph := G.relabel d.perm } = { codes := bs ++ [codeSentinel], graph := G.relabel c.perm }.max
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm } ∧ Settled cs bs' out
The complete native discrete classifier chooses the maximum once the first-reference branch is bounded by its retained history.
theorem
Hex.GraphIso.Nauty.Sparse.leaf_max
{n : Nat}
{G : SparseGraph n}
{cs bs : List Nat}
{st : State n}
{l c : Label n}
(h : Codes cs bs st)
(hlen : cs.length ≤ n)
(hl : Label.ofArray? n st.lab = some l)
(hc : Label.ofArray? n st.canonlab = some c)
(hR : st.canong.Prefix (G.relabel c.perm) st.samerows)
(hfirst :
(classify (Graph.ofGraph G) cs.length n st).fst = Generic.Leaf.autoFirst →
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm }.Le
{ codes := bs ++ [codeSentinel], graph := G.relabel c.perm })
:
have verdict := classify (Graph.ofGraph G) cs.length n st;
have out := (leafExit verdict.fst cs.length verdict.snd).snd;
∃ (bs' : List Nat), ∃ (d : Label n), Label.ofArray? n out.canonlab = some d ∧ { codes := bs' ++ [codeSentinel], graph := G.relabel d.perm } = { codes := bs ++ [codeSentinel], graph := G.relabel c.perm }.max
{ codes := cs ++ [codeSentinel], graph := G.relabel l.perm } ∧ Settled cs bs' out
Shared exit bookkeeping retains the exact native maximum and settled code state chosen by classification, for every automorphism/return arm.