theorem Hex.GraphIso.Nauty.Sparse.Max.Frame.first_contains {n : Nat} {G : SparseGraph n} {tcLevel fuel tv : Nat} {f : Frame n} {gamma : Array Nat} (hopen : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).fst ≠ n) (htv : (Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry).snd.snd.fst.nextElem none = some tv) : have r := Generic.prepareFirst (Graph.ofGraph G) tcLevel f.level f.numcells f.entry; gamma ∈ (Generic.sweep true (Graph.ofGraph G) (n + 2) tcLevel fuel (n + 1) f.level r.fst r.snd.fst.toNat tv (some tv) r.snd.snd.fst 0 (cheapCheck true f.level r.snd.snd.snd.snd)).snd.snd.genTrace → gamma ∈ (Generic.node true (Graph.ofGraph G) (n + 2) tcLevel (fuel + 1) f.level f.numcells f.entry).snd.genTrace

Closing an actual first sweep retains every generator it emitted, including the branch that updates the stabilizer index product.