theorem
Hex.GraphIso.Nauty.Sparse.labels_map
{n : Nat}
{ref lab : Array Nat}
{f l : Label n}
(hf : Label.ofArray? n ref = some f)
(hl : Label.ofArray? n lab = some l)
:
The forward permutation between two parsed labels maps their literal arrays pointwise, independently of any graph or automorphism claim.
theorem
Hex.GraphIso.Nauty.Sparse.RouteAt.autoFirst_key
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel base : Nat}
{root : RefineSt n}
{cs fs : List Nat}
{st out : State n}
{f l : Label n}
(h : RouteAt G.graph tcLevel st.firsttc base root cs.length n st)
(href : FirstRef G.graph tcLevel base root st)
(hr : RefineSt.Ready G.graph base root)
(hh : CheapHistory G.graph tcLevel cs.length cs.length n st)
(hcodes : FirstCodeInv n cs fs st.firstcode st.eqlevFirst)
(hauto : classify (Graph.ofGraph G.graph) cs.length n st = (Generic.Leaf.autoFirst, out))
(hw : st.workperm.size = n)
(hf : Label.ofArray? n st.firstlab = some f)
(hl : Label.ofArray? n st.lab = some l)
(hrf : CellsReach G.toDense st.firstlab)
(hrl : CellsReach G.toDense st.lab)
:
Every first-reference admission has the complete saved key when its actual guided history is available. Cheap and scanned admissions use the proved native automorphism; the guided path establishes the sentinel.
theorem
Hex.GraphIso.Nauty.Sparse.TraceReady.leaf_max
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel base : Nat}
{root : RefineSt n}
{cs bs fs : List Nat}
{st : State n}
(h : TraceReady G tcLevel cs.length n st)
(hn : 0 < n)
(route : RouteAt G.graph tcLevel st.firsttc base root cs.length n st)
(href : FirstRef G.graph tcLevel base root st)
(hr : RefineSt.Ready G.graph base root)
(hc : Comparison G.graph cs bs fs st)
:
have verdict := classify (Graph.ofGraph G.graph) cs.length n st;
have out := (leafExit verdict.fst cs.length verdict.snd).snd;
∃ (l : Label n), ∃ (c : Label n), ∃ (bs' : List Nat), ∃ (d : Label n), Label.ofArray? n st.lab = some l ∧ Label.ofArray? n st.canonlab = some c ∧ Label.ofArray? n out.canonlab = some d ∧ { codes := bs' ++ [codeSentinel], graph := G.graph.relabel d.perm } = { codes := bs ++ [codeSentinel], graph := G.graph.relabel c.perm }.max
{ codes := cs ++ [codeSentinel], graph := G.graph.relabel l.perm } ∧ Settled cs bs' out
At a valid prepared native leaf with retained guided history, the executed leaf action computes the exact incumbent maximum. The first-key bound is derived from that history, not supplied as a classification oracle.