theorem Hex.GraphIso.Nauty.Generation.carries_label {n k : Nat} {G : Colored n k} {base : List (Fin n)} {ctx : Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} {pos : Nat} {u v : Fin n} (h : LabelCarrier ctx ref cur store) (htrace : ∀ (γ : Array Nat), γ ∈ store → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hpos : pos < n) (href : ref[pos]! = ↑u) (hcur : cur[pos]! = ↑v) : Aut.Carries G base u v

A recorded reference-to-current leaf carrier gives the corresponding vertex carrier in the generated pointwise stabilizer.

theorem Hex.GraphIso.Nauty.Generation.Cover.reference {n k : Nat} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G base guide tcell cursor) {tv u : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) (href : Aut.Orbit G base guide u → Aut.Carries G base u guide) {ctx : Ctx n} {ref cur : Array Nat} {store : Array (Array Nat)} {pos : Nat} (hcarrier : LabelCarrier ctx ref cur store) (htrace : ∀ (γ : Array Nat), γ ∈ store → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ store → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hpos : pos < n) (hatRef : ref[pos]! = ↑u) (hatCur : cur[pos]! = ↑tv) : Cover G base guide tcell (some ↑tv)

A direct first-reference or canonical-reference return consumes the child when the reference's orbit obligation is already covered. This uses the emitted carrier even when the orbit partition did not grow.

theorem Hex.GraphIso.Nauty.Generation.Cover.unwind {n k : Nat} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G base guide tcell cursor) {tv : Fin n} (hnext : tcell.nextElem cursor = some ↑tv) {ctx : Ctx n} {tcLevel level pos : Nat} {out : SearchSt n} {best : Option (Key n)} (payload : Unwind ctx tcLevel level out best) (htrace : ∀ (γ : Array Nat), γ ∈ out.genTrace → γ ∈ Aut.trace G) (hfix : ∀ (γ : Array Nat), γ ∈ out.genTrace → ∀ (b : Fin n), b ∈ base → γ[↑b]! = ↑b) (hpos : pos < n) (hatCur : out.lab[pos]! = ↑tv) (hfirstLt : out.firstlab[pos]! < n) (hcanonLt : out.canonlab[pos]! < n) (hfirst : Aut.Orbit G base guide ⟨out.firstlab[pos]!, hfirstLt⟩ → Aut.Carries G base ⟨out.firstlab[pos]!, hfirstLt⟩ guide) (hcanon : Aut.Orbit G base guide ⟨out.canonlab[pos]!, hcanonLt⟩ → Aut.Carries G base ⟨out.canonlab[pos]!, hcanonLt⟩ guide) (hcoset : out.cosetindex = ↑tv) : Cover G base guide tcell (some ↑tv)

The located generator receipt can be consumed without dropping its carrier. The reference premises are conditional: a canonical reference outside the guide's full orbit imposes no generation obligation.

theorem Hex.GraphIso.Nauty.Generation.Cover.shortCarriers {n k : Nat} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G base guide tcell cursor) {st : SearchSt n} (hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → ∀ (v : Fin n), mcr.mem ↑v = false → ∃ (u : Fin n), ↑u < ↑v ∧ Aut.Carries G base v u) : Cover G base guide (Nauty.shortprune tcell st) cursor

Generated descending carriers justify a short-prune filter without requiring its fixed-point bitset to characterize the active base.

theorem Hex.GraphIso.Nauty.Generation.Cover.shortprune {n k : Nat} {G : Colored n k} {base : List (Fin n)} {guide : Fin n} {tcell : VSet n} {cursor : Option Nat} (h : Cover G base guide tcell cursor) {st : SearchSt n} (hlast : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → PairGenerated G fix mcr ∧ ∀ (b : Fin n), b ∈ base → fix.mem ↑b = true) : Cover G base guide (Nauty.shortprune tcell st) cursor

The guiding child's short-prune request preserves generated orbit coverage once its last ledger pair has generated carriers.