structure Hex.GraphIso.Nauty.Generation.Cover {n k : Nat} (G : Colored n k) (gs : List (Perm n)) (base : List (Fin n)) (guide : Fin n) (tcell : VSet n) (cursor : Option Nat) : Prop

Coverage of the first child's full stabilizer orbit by generated carriers and the remaining target vertices. Vertices in other orbits place no generation obligation on this sweep.

• cover : RelCover (Carries G gs base) Fin.val (Aut.Orbit G base guide) (fun (v : Fin n) => Carries G gs base v guide) fun (v : Fin n) => Aut.Orbit G base guide v ∧ tcell.mem ↑v = true ∧ After cursor ↑v
• past (v : Fin n) : Aut.Orbit G base guide v → tcell.mem ↑v = true → ¬After cursor ↑v → Carries G gs base v guide

theorem Hex.GraphIso.Nauty.Generation.Cover.mono {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} {more : List (Perm n)} (h : Cover G gs base guide tcell cursor) (hsub : ∀ (p : Perm n), p ∈ gs → p ∈ more) : Cover G more base guide tcell cursor

Coverage at a reached cursor survives later generator admissions.

theorem Hex.GraphIso.Nauty.Generation.Cover.start {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} (hwindow : ∀ (v : Fin n), Aut.Orbit G base guide v → tcell.mem ↑v = true) : Cover G gs base guide tcell none

Before the first child, all images of the guide are live.

theorem Hex.GraphIso.Nauty.Generation.Cover.advance {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) {tv : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) (hcur : Aut.Orbit G base guide tv → Carries G gs base tv guide) : Cover G gs base guide tcell (some ↑tv)

Visiting the least live vertex advances the cursor once its orbit obligation has been discharged.

theorem Hex.GraphIso.Nauty.Generation.Cover.before {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) {tv u : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) (horbit : Aut.Orbit G base guide u) (hlt : ↑u < ↑tv) : Carries G gs base u guide

Every orbit vertex earlier than the next live child is already covered, including vertices removed by an older filter.

theorem Hex.GraphIso.Nauty.Generation.Cover.smaller {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) {tv u : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) (horbit : Aut.Orbit G base guide tv) (hcarry : Carries G gs base tv u) (hlt : ↑u < ↑tv) : Carries G gs base tv guide

A smaller generated image discharges the current child, even if an older filter removed that image from the target set.

theorem Hex.GraphIso.Nauty.Generation.Cover.orbitSkip {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) {tv : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) {store : List (Array Nat)} {orbits : Array Nat} (hsound : OrbSound (OrbConn store n) orbits n) (htrace : Realizes G gs store) (hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hne : orbits[↑tv]! ≠ ↑tv) : Cover G gs base guide tcell (some ↑tv)

A sound orbit pointer consumes the current first-path child while retaining its generated stabilizer carrier.

theorem Hex.GraphIso.Nauty.Generation.Cover.filterDesc {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell tcell' : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) (hstep : ∀ (v : Fin n), Aut.Orbit G base guide v → tcell.mem ↑v = true → After cursor ↑v → tcell'.mem ↑v = true ∨ ∃ (u : Fin n), Carries G gs base v u ∧ ↑u < ↑v) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : Cover G gs base guide tcell' cursor

Descending generated carriers preserve coverage under a target-set filter. The destination need not have survived earlier filters.

theorem Hex.GraphIso.Nauty.Generation.Cover.finish {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) (hnext : tcell.nextElem cursor = none) (v : Fin n) : Aut.Orbit G base guide v → Carries G gs base guide v

Emptying the live suffix represents every image of the guide by a word in the final generator list that fixes the current base.

theorem Hex.GraphIso.Nauty.Generation.Cover.stabilizer {n k : Nat} {gs : List (Perm n)} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G gs base guide tcell cursor) (hnext : tcell.nextElem cursor = none) (hdeep : ∀ (p : Perm n), IsIso G G p → Perm.Fixes (guide :: base) p → Perm.Generated gs p) {p : Perm n} (hp : IsIso G G p) (hfix : Perm.Fixes base p) : Perm.Generated gs p

The completed sweep closes one step of the point-stabilizer chain.