theorem Hex.GraphIso.Nauty.Sparse.Generation.receipt {n k : Nat} {G : Sparse.Colored n k} {gs : List (Perm n)} {base : List (Fin n)} {guide tv : Fin n} {tcLevel fuel level numcells tc : Nat} {first short : Bool} {st out : State n} {cell : VSet n} {previous : Option Nat} (h : Generation.Cover G.toDense gs base guide cell previous) (hready : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (htarget : Generic.Target State.frame level tc cell st) (hnext : cell.nextElem previous = some ↑tv) (hpast : Generation.CanonPast level tc previous st) (hcall : Generic.node false (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc (↑tv) st) = (Generic.Exit.unwind level short, out)) (hr : RefReturn (Graph.context G.graph) level out) (hsaved : Saved G out) (horbits : OrbitTrace G out) (hsound : TraceOk G out) (htrace : Realizes G gs out.genTrace.toList) (hfix : ∀ (gamma : Array Nat), gamma ∈ out.genTrace → ∀ (b : Fin n), b ∈ base → gamma[↑b]! = ↑b) (hfirst : out.firstlab[tc]! = ↑guide) (hcoset : out.cosetindex = ↑tv) : Generation.Cover G.toDense gs base guide cell (some ↑tv)

All three actual native reference-return alternatives discharge the current stabilizer-orbit obligation in a containing generated group. The shared group relation uses the sparse graph's semantic interpretation; every child call, scatter, label position and orbit pointer is native.