theorem Hex.GraphIso.Nauty.Sparse.PathInv.empty_trace {n k : Nat} {G : Sparse.Colored n k} {level : Nat} {st : State n} (h : PathInv G level st) (ht : TraceOk G st) (hn : 0 < n) (he : st.fixedpts = VSet.empty) (gamma : Array Nat) : gamma ∈ st.genTrace → CellStab st.ptn level st.lab gamma

With an empty individualized path, native automorphism soundness already gives stabilization of the current refined partition. This seeds the root orbit argument without a generator-stabilization premise.

theorem Hex.GraphIso.Nauty.Sparse.OrbitTrace.carrier {n k : Nat} {G : Sparse.Colored n k} {level numcells tv : Nat} {base st : State n} (h : OrbitTrace G st) (ht : TraceOk G st) (hb : Ready G level numcells base) (hn : 0 < n) (hl : 1 ≤ level) (hv : tv < n) (hs : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → CellStab base.ptn level base.lab gamma) (hne : st.orbits[tv]! ≠ tv) : ∃ (gamma : Array Nat), checkAutom (Graph.context G.graph).g gamma = true ∧ CellStab base.ptn level base.lab gamma ∧ gamma[tv]! = st.orbits[tv]! ∧ st.orbits[tv]! < tv

The actual orbit pointer has a checked word carrier in any frozen partition stabilized by the accumulated trace. A skipped pointer has a strictly smaller endpoint, as required by ranked child coverage.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.orbit_skip {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc len tv : Nat} {cs : List Nat} {base st : State n} {live : Nat → Prop} {best : Option (Key n)} {first : Bool} (h : CellCover G.graph tcLevel fuel level numcells tc len cs base live best) (hb : Ready G level numcells base) (ho : OrbitTrace G st) (ht : TraceOk G st) (hn : 0 < n) (hl : 1 ≤ level) (hc : IsCell base.ptn level tc len) (hlen : 1 < len) (hr : tc + len ≤ n) (hf : n < fuel + (numcells + 1)) (hv : (windowSet n base.lab tc len).mem tv = true) (hle : ∀ (v : Nat), live v → tv ≤ v) (hs : ∀ (gamma : Array Nat), gamma ∈ st.genTrace → CellStab base.ptn level base.lab gamma) (hskip : (!first || st.orbits[tv]! == tv) = false) : CellCover G.graph tcLevel fuel level numcells tc len cs base (fun (v : Nat) => live v ∧ tv < v) best

The literal first-path orbit guard removes only a child represented by a strictly smaller child with the same whole sparse subtree maximum. The frozen-ancestor trace invariant supplies stabilization at this level.

theorem Hex.GraphIso.Nauty.Sparse.CellCover.empty_orbit {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc len tv : Nat} {cs : List Nat} {st : State n} {live : Nat → Prop} {best : Option (Key n)} {first : Bool} (h : CellCover G.graph tcLevel fuel level numcells tc len cs st live best) (hb : Ready G level numcells st) (hp : PathInv G level st) (ho : OrbitTrace G st) (ht : TraceOk G st) (hempty : st.fixedpts = VSet.empty) (hn : 0 < n) (hl : 1 ≤ level) (hc : IsCell st.ptn level tc len) (hlen : 1 < len) (hr : tc + len ≤ n) (hf : n < fuel + (numcells + 1)) (hv : (windowSet n st.lab tc len).mem tv = true) (hle : ∀ (v : Nat), live v → tv ≤ v) (hskip : (!first || st.orbits[tv]! == tv) = false) : CellCover G.graph tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ tv < v) best

The root's empty path discharges the trace-stabilization requirement of the actual orbit skip using only native generator soundness.