theorem
Hex.GraphIso.Nauty.Max.Frame.emit_coset
{n : Nat}
(ctx : Ctx n)
(tcLevel : Nat)
(f : Frame n)
:
Leaf preparation and action retain the suspended first child's index.
A code-two return either names the canonical ancestor or records that the current coset has acquired a smaller orbit representative.
theorem
Hex.GraphIso.Nauty.Max.Parent.orbit_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel : Nat}
{p : Parent n}
{out : Search n}
(h : Valid G ctx tcLevel p)
(hgsz : ctx.g.size = n)
(hi : RunInv G ctx out)
(hgens : ∀ (γ : Array Nat), γ ∈ out.genTrace → CellStab p.state.ptn p.loop.node.level p.state.lab γ)
(hlt : out.orbits[p.chosen]! < p.chosen)
(hg : Generic.Grows (SearchState.key ctx p.bs p.state) (SearchState.best ctx out))
:
Generic.Covers (Frame.key ctx tcLevel (child ctx tcLevel p)) (SearchState.best ctx out)
A smaller orbit representative in a suspended first sweep identifies an already covered child, using all admitted generators in that frame.
theorem
Hex.GraphIso.Nauty.Max.NodeInput.coset_cover
{n k : Nat}
{G : Colored n k}
{ctx : Ctx n}
{tcLevel fuel : Nat}
{f : Frame n}
{bs fs : List Nat}
{parents : Parents n}
(h : NodeInput G ctx tcLevel fuel false f bs fs parents)
(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)
(he : (Frame.emit ctx tcLevel f).fst = Generic.Exit.unwind f.entry.gcaFirst false)
(hlt :
(Frame.emit ctx tcLevel f).snd.orbits[(Frame.emit ctx tcLevel f).snd.cosetindex]! < (Frame.emit ctx tcLevel f).snd.cosetindex)
{p : Parent n}
(hp : parents f.entry.gcaFirst = some p)
(hg : Generic.Grows (SearchState.key ctx bs f.entry) (SearchState.best ctx (Frame.emit ctx tcLevel f).snd))
:
Generic.Covers (Frame.key ctx tcLevel (Parent.child ctx tcLevel p))
(SearchState.best ctx (Frame.emit ctx tcLevel f).snd)
The actual coset-index exit covers the interrupted first-ancestor child using the established saved-index and earlier-child invariants.
Every actual code-two return satisfies the maximum rule, including the early return selected by a smaller coset representative.