theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.emit_store
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{st : State n}
{parents : Parents n}
(h : Scope G tcLevel f bs st parents)
(hf : Frame.Valid G f)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
:
Every actual emitter remains inside each suspended selected child. Its labelling therefore retains the chosen vertex at that target position. The ancestor chain supplies both the cell permutation and the literal closed boundaries needed to coarsen the final native refinement.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.emit_cover
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{st : State n}
{parents : Parents n}
(h : Scope G tcLevel f bs st parents)
(hf : Frame.Valid G f)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
{ref gamma : Array Nat}
{best : Option (Key n)}
(ha : Automorphism G gamma)
(href : ref.size = n)
(hfr : cellsPerm p.state.ptn p.node.level p.state.lab ref)
(hmap : ∀ (i : Nat), i < n → gamma[ref[i]!]! = (Frame.emit G.graph tcLevel f).snd.lab[i]!)
(hcover : Covers (Parent.key G.graph tcLevel p ref[p.tc]!) best)
:
Covers (Frame.key G.graph tcLevel (Parent.child G.graph tcLevel p)) best
A scatter at the actual emitter covers the chosen child of a saved ancestor. All current-label containment and selected-position facts are derived from the native scope, rather than assumed by this return rule.
theorem
Hex.GraphIso.Nauty.Sparse.Max.Scope.child_witness
{n k : Nat}
{G : Sparse.Colored n k}
{tcLevel : Nat}
{f : Frame n}
{bs : List Nat}
{st : State n}
{parents : Parents n}
(h : Scope G tcLevel f bs st parents)
{t : Nat}
{p : Parent n}
(hp : parents t = some p)
(ht : t < f.level - 1)
{best : Option (Key n)}
(hc : Covers (Frame.key G.graph tcLevel (Parent.child G.graph tcLevel p)) best)
:
Coverage of a suspended selected child supplies exactly the frozen ancestor named by a nonlocal return, using the retained parent chain.