theorem Hex.GraphIso.Nauty.Generation.Cover.shortSource {n k : Nat} {G : Colored n k} {ctx : Ctx n} {base : List (Fin n)} {guide : Fin n} {cell : VSet n} {cursor : Option Nat} {tcLevel specFuel level numcells tc len offset : Nat} {codes bs fs : List Nat} {rsLab rsPtn : Array Nat} {receiverCell : VSet n} {receiverCursor : Option Nat} {entry st out : SearchSt n} {best outBest : Option (Key n)} {trail eventTrail : FrameTrail} (h : Cover G base guide cell cursor) (hg : ctx.g = rowsOf G) (hpathCodes : level = codes.length) (hinv : LoopInv G ctx tcLevel specFuel level codes bs fs numcells rsLab rsPtn tc len receiverCell receiverCursor entry st best trail) (hpath : PathOk ctx (initPtn n (n + 2) (initialPartition G).snd) (initialPartition G).fst level st) (hevent : EventOut G ctx tcLevel codes fs out outBest eventTrail (Int.ofNat level)) (hpreserved : TrailExt (level + 1) (trail.push level { frame := sweepFrame specFuel codes rsLab rsPtn tc numcells, offset := offset }) eventTrail) (hsource : ShortSource G ctx out eventTrail (Int.ofNat level)) (hat : rsLab[tc + offset]! = ↑guide) (hbase : ∀ (b : Fin n), b ∈ base → st.fixedpts.mem ↑b = true) (htrace : ∀ (γ : Array Nat), γ ∈ out.genTrace → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ out.genTrace → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hdeep : ∀ (p : Perm n), IsIso G G p → Perm.Fixes (guide :: base) p → Perm.Generated (Aut.gens G) p) : Cover G base guide (Nauty.shortprune cell out) cursor

The guiding child's short-prune filter uses recorded generators for explicit pairs and the deeper stabilizer for implicit pairs. The saved cheap boundary fixes the guiding vertex in addition to the parent base.