theorem Hex.GraphIso.Nauty.Sparse.sweep_same {n : Nat} (ctx : Graph n) (inf tcLevel fuel cfuel level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : State n) : Generic.Past true tv1 cursor → (Generic.sweep true ctx inf tcLevel fuel cfuel level numcells tc tv1 cursor cell index st).snd.snd.allsamelevel = st.allsamelevel

Later first-path siblings leave the all-same boundary unchanged, even if a child returns past the current frame.

theorem Hex.GraphIso.Nauty.Sparse.firstSweep_same {n : Nat} {ctx : Graph n} {inf tcLevel fuel cfuel level numcells tc tv index : Nat} {cell : VSet n} {st : State n} (horbit : st.orbits[tv]! = tv) : (Generic.sweep true ctx inf tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st).snd.snd.allsamelevel = (Generic.node true ctx inf tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child true level tc tv st)).snd.allsamelevel

The guiding child's all-same boundary survives cleanup and the entire sibling sweep, including an early exit.