theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.emit_coset {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : (emit G tcLevel f).snd.cosetindex = f.entry.cosetindex

Native preparation, classification and leaf action retain the selected first-path coset index.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.emit_first {n : Nat} (G : SparseGraph n) (tcLevel : Nat) (f : Frame n) : (emit G tcLevel f).snd.gcaFirst = f.entry.gcaFirst

theorem Hex.GraphIso.Nauty.Sparse.Max.canon_exit {n : Nat} (level : Nat) (st : State n) : have out := leafExit Generic.Leaf.autoCanon level st; (∃ (short : Bool), out.fst = Generic.Exit.unwind st.gcaCanon short) ∨ out.fst = Generic.Exit.unwind st.gcaFirst false ∧ out.snd.orbits[out.snd.cosetindex]! < out.snd.cosetindex

The actual canonical-admission branch returns to its canonical ancestor, or returns to the first ancestor after acquiring a smaller representative for the selected coset index.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.coset_return {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hs : Scope G tcLevel f bs f.entry parents) (hcoset : Cosets f.entry parents) (hrank : ∀ (t : Nat) (p : Parent n), parents t = some p → Parent.Ranked G.graph tcLevel p) (hframes : ∀ (t : Nat) (p : Parent n), parents t = some p → p.first = true → TraceFrame G p.node.level p.state f.entry) (ho : OrbitTrace G f.entry) (hpos : 0 < f.entry.gcaFirst) (hlt : f.entry.gcaFirst < f.level) (ha : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) (hexit : (emit G.graph tcLevel f).fst = Generic.Exit.unwind f.entry.gcaFirst false) (hsmall : (emit G.graph tcLevel f).snd.orbits[(emit G.graph tcLevel f).snd.cosetindex]! < (emit G.graph tcLevel f).snd.cosetindex) : MaxResult (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd) (f.level - 1) (Max.Witness G tcLevel parents.frames) (emit G.graph tcLevel f).fst

The coset return satisfies the full maximum contract. Its selected ancestor comes from the saved-index invariant, and native trace words transport its interrupted child to an already covered smaller child.

theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.Valid.canonical {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {f : Frame n} {bs fs : List Nat} {parents : Parents n} (h : Valid G f) (hi : CodeEntry G tcLevel f.level f.numcells f.entry) (hc : Comparison G.graph f.codes bs fs f.entry) (hs : Scope G tcLevel f bs f.entry parents) (hg : Guides G.graph tcLevel f.entry parents) (hcoset : Cosets f.entry parents) (hrank : ∀ (t : Nat) (p : Parent n), parents t = some p → Parent.Ranked G.graph tcLevel p) (hframes : ∀ (t : Nat) (p : Parent n), parents t = some p → p.first = true → TraceFrame G p.node.level p.state f.entry) (ho : OrbitTrace G f.entry) (hcounter : 0 < f.entry.gcaFirst ∧ f.entry.gcaFirst ≤ f.entry.gcaCanon ∧ f.entry.gcaCanon < f.level) (ha : have p := prepareOther (Graph.ofGraph G.graph) tcLevel f.level f.numcells f.entry; (classify (Graph.ofGraph G.graph) f.level p.fst p.snd.snd.snd.snd.snd).fst = Generic.Leaf.autoCanon) : MaxResult (key G.graph tcLevel f) (State.key G.graph bs f.entry) (State.best G.graph (emit G.graph tcLevel f).snd) (f.level - 1) (Max.Witness G tcLevel parents.frames) (emit G.graph tcLevel f).fst

Every native canonical-reference admission satisfies the maximum return rule, including the earlier first-ancestor coset branch. All reference, rank, index and trace premises are local traversal invariants.