structure Hex.GraphIso.Nauty.Generation.VisitCover {n : Nat} (P : Nat → Prop) (lab : Array Nat) (tc len : Nat) (tcell : VSet n) (cursor : Option Nat) : Prop

Every possible occurrence lies in a live child or has been ruled out. The predicate is abstract so both ordinary leaves and references carrying uniformity evidence use the same sweep coverage proof.

• cover : ChildCover P (fun (o : Nat) => lab[tc + o]!) (fun (o : Nat) => o < len) (fun (o : Nat) => ¬P o) (ChildLive lab tc len tcell cursor)
• past (o : Nat) : o < len → tcell.mem lab[tc + o]! = true → ¬After cursor lab[tc + o]! → ¬P o

theorem Hex.GraphIso.Nauty.Generation.VisitCover.start {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} (hlab : ∀ (o : Nat), o < len → lab[tc + o]! < n) : VisitCover P lab tc len (windowSet n lab tc len) none

Initially every occurrence is in the live target window.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.advance {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} (h : VisitCover P lab tc len tcell cursor) {tv : Nat} (hnext : tcell.nextElem cursor = some tv) (hcur : ∀ (o : Nat), o < len → lab[tc + o]! = tv → ¬P o) : VisitCover P lab tc len tcell (some tv)

A child proved to have no matching occurrence advances the sweep.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.filterDesc {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} (h : VisitCover P lab tc len tcell cursor) (hstep : ∀ (o : Nat), ChildLive lab tc len tcell cursor o → tcell'.mem lab[tc + o]! = true ∨ ∃ (j : Nat), j < len ∧ P o = P j ∧ lab[tc + j]! < lab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : VisitCover P lab tc len tcell' cursor

A descending filter preserves absence coverage through arbitrarily many earlier filters. Equality here is equality of occurrence propositions, so it retains the target hints as well as the complete leaf key.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.smaller {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} (h : VisitCover P lab tc len tcell cursor) {tv o : Nat} (hnext : tcell.nextElem cursor = some tv) (ho : o < len) (hlt : lab[tc + o]! < tv) : ¬P o

An earlier original child has no occurrence, including when an older filter removed it from the current target set.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.carrier {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {ctx : Ctx n} {level : Nat} {ptn : Array Nat} (h : VisitCover P lab tc len tcell cursor) {tv oRef : Nat} {ref cur : Array Nat} {store : Array (Array Nat)} (hnext : tcell.nextElem cursor = some tv) (hpos : tc < n) (href : oRef < len) (habsent : ¬P oRef) (hcarrier : CellCarrier ctx ptn level lab ref cur store) (hatRef : ref[tc]! = lab[tc + oRef]!) (hatCur : cur[tc]! = tv) (hcarry : ∀ {γ : Array Nat} {o j : Nat}, checkAutom ctx.g γ = true → CellStab ptn level lab γ → o < len → j < len → γ[lab[tc + o]!]! = lab[tc + j]! → (P o ↔ P j)) : VisitCover P lab tc len tcell (some tv)

A checked carrier transfers absence from a reference child to the current child. The carrier belongs to the frozen cell stabilizer.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.reference {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {ctx : Ctx n} {level : Nat} {ptn : Array Nat} (h : VisitCover P lab tc len tcell cursor) {tv oRef : Nat} {ref cur : Array Nat} {store : Array (Array Nat)} (hnext : tcell.nextElem cursor = some tv) (hpos : tc < n) (href : oRef < len) (hearlier : lab[tc + oRef]! < tv) (hcarrier : CellCarrier ctx ptn level lab ref cur store) (hatRef : ref[tc]! = lab[tc + oRef]!) (hatCur : cur[tc]! = tv) (hcarry : ∀ {γ : Array Nat} {o j : Nat}, checkAutom ctx.g γ = true → CellStab ptn level lab γ → o < len → j < len → γ[lab[tc + o]!]! = lab[tc + j]! → (P o ↔ P j)) : VisitCover P lab tc len tcell (some tv)

A carrier to an earlier reference discharges the current child using the ranked coverage invariant, without claiming exhaustive search.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.filterAutom {n : Nat} {P : Nat → Prop} {tc len : Nat} {tcell tcell' : VSet n} {cursor : Option Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (h : VisitCover P st.lab tc len tcell cursor) {e : Nat} (hok : IterOk ctx level st) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hlen : len = e + 1 - tc) (hcarry : ∀ {γ : Array Nat} {o j : Nat}, checkAutom ctx.g γ = true → CellStab st.ptn level st.lab γ → o < len → j < len → γ[st.lab[tc + o]!]! = st.lab[tc + j]! → (P o ↔ P j)) (hdrop : ∀ (o : Nat), ChildLive st.lab tc len tcell cursor o → tcell'.mem st.lab[tc + o]! = false → ∃ (γ : Array Nat), checkAutom ctx.g γ = true ∧ CellStab st.ptn level st.lab γ ∧ γ[st.lab[tc + o]!]! < st.lab[tc + o]!) (hsub : ∀ (v : Nat), tcell'.mem v = true → tcell.mem v = true) : VisitCover P st.lab tc len tcell' cursor

A checked cell stabilizer transports the entire reference occurrence through a pruning step. It need not belong to the emitted generator list.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.longprune {n : Nat} {P : Nat → Prop} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (h : VisitCover P st.lab tc len tcell cursor) {e : Nat} (hok : IterOk ctx level st) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hlen : len = e + 1 - tc) (hcarry : ∀ {γ : Array Nat} {o j : Nat}, checkAutom ctx.g γ = true → CellStab st.ptn level st.lab γ → o < len → j < len → γ[st.lab[tc + o]!]! = st.lab[tc + j]! → (P o ↔ P j)) {fixedpts : VSet n} {autos : Array (VSet n × VSet n)} (haut : ∀ (p : VSet n × VSet n), p ∈ autos.toList → fixedpts.subset p.fst = true → PairOk ctx.g st.ptn st.lab level p.fst p.snd) : VisitCover P st.lab tc len (Nauty.longprune tcell fixedpts autos) cursor

The off-path long-prune ledger preserves every sought reference.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.shortprune {n : Nat} {P : Nat → Prop} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (h : VisitCover P st.lab tc len tcell cursor) {e : Nat} (hok : IterOk ctx level st) (hcell : (tc, e) ∈ cells st.ptn level n) (hne : tc < e) (hlen : len = e + 1 - tc) (hcarry : ∀ {γ : Array Nat} {o j : Nat}, checkAutom ctx.g γ = true → CellStab st.ptn level st.lab γ → o < len → j < len → γ[st.lab[tc + o]!]! = st.lab[tc + j]! → (P o ↔ P j)) {out : SearchSt n} (hlast : ∀ (fix mcr : VSet n), out.autos.back? = some (fix, mcr) → PairOk ctx.g st.ptn st.lab level fix mcr) : VisitCover P st.lab tc len (Nauty.shortprune tcell out) cursor

The off-path short-prune ledger preserves every sought reference, including when the last pair is implicit.

theorem Hex.GraphIso.Nauty.Generation.VisitCover.finish {n : Nat} {P : Nat → Prop} {lab : Array Nat} {tc len : Nat} {tcell : VSet n} {cursor : Option Nat} (h : VisitCover P lab tc len tcell cursor) (hnext : tcell.nextElem cursor = none) (o : Nat) : o < len → ¬P o

Exhausting a sweep with no matching visited child rules out every matching child of the original target window.