theorem Hex.GraphIso.Nauty.ChildCover.pruned {n : Nat} {g : Array (VSet n)} {lab ptn : Array Nat} {level tc len : Nat} {key : Nat → Key n} {live : Nat → Prop} {best : Option (Key n)} {filtered : VSet n} (h : ChildCover key id (fun (v : Nat) => (windowSet n lab tc len).mem v = true) (fun (v : Nat) => Generic.Covers (key v) best) live) (hok : LabOk lab n) (hc : IsCell ptn level tc len) (hr : tc + len ≤ lab.size) (hsub : ∀ (v : Nat), live v → (windowSet n lab tc len).mem v = true) (hkey : ∀ (γ : Array Nat), checkAutom g γ = true → CellStab ptn level lab γ → ∀ (v : Nat), (windowSet n lab tc len).mem v = true → key v = key γ[v]!) (hdrop : ∀ (v : Nat), live v → filtered.mem v = false → ∃ (γ : Array Nat), checkAutom g γ = true ∧ CellStab ptn level lab γ ∧ γ[v]! < v) : ChildCover key id (fun (v : Nat) => (windowSet n lab tc len).mem v = true) (fun (v : Nat) => Generic.Covers (key v) best) fun (v : Nat) => live v ∧ filtered.mem v = true

A descending filter composes with coverage of the current live set. Its carrier may land in an already visited child or outside an earlier filter's survivors; ranked coverage resolves both cases.

def Hex.GraphIso.Nauty.CellCover {n : Nat} (ctx : Ctx n) (tcLevel fuel level numcells tc len : Nat) (cs : List Nat) (st : Search n) (live : Nat → Prop) (best : Option (Key n)) : Prop

Coverage of a frozen target cell, indexed by vertex labels. Live vertices can include the cursor condition as well as mutable set membership.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.CellCover.init {n : Nat} (ctx : Ctx n) (tcLevel fuel level numcells tc len : Nat) (cs : List Nat) (st : Search n) (best : Option (Key n)) : CellCover ctx tcLevel fuel level numcells tc len cs st (fun (v : Nat) => (windowSet n st.lab tc len).mem v = true) best

Before visiting children, every target vertex represents itself.

theorem Hex.GraphIso.Nauty.CellCover.grow {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : Search n} {live : Nat → Prop} {before after : Option (Key n)} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live before) (hg : Generic.Grows before after) : CellCover ctx tcLevel fuel level numcells tc len cs st live after

Growing the incumbent preserves all previously covered children.

theorem Hex.GraphIso.Nauty.CellCover.visit {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells tc len tv : Nat} {cs : List Nat} {st : Search n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hle : ∀ (v : Nat), live v → tv ≤ v) (hc : Generic.Covers (prefixKey cs (vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells tv)) best) : CellCover ctx tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ tv < v) best

Visiting the least live vertex advances the cursor and absorbs every original child represented by that vertex.

theorem Hex.GraphIso.Nauty.CellCover.skip {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells tc len tv rep : Nat} {cs : List Nat} {st : Search n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hle : ∀ (v : Nat), live v → tv ≤ v) (hr : (windowSet n st.lab tc len).mem rep = true) (hlt : rep < tv) (hkey : vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells tv = vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells rep) : CellCover ctx tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ tv < v) best

A child repeating a smaller representative is already covered when it reaches the cursor. Ranked coverage rules out a still-live carrier below that cursor, including after earlier filters.

theorem Hex.GraphIso.Nauty.CellCover.finish {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : Search n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hempty : ∀ (v : Nat), ¬live v) (v : Nat) : (windowSet n st.lab tc len).mem v = true → Generic.Covers (prefixKey cs (vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells v)) best

Exhausting the live set covers the full original target cell.

theorem Hex.GraphIso.Nauty.CellCover.finish_cursor {n : Nat} {ctx : Ctx n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st : Search n} {live : Nat → Prop} {best : Option (Key n)} {cell : VSet n} {cursor : Option Nat} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hmem : ∀ (v : Nat), live v → cell.mem v = true) (hle : ∀ (v : Nat), live v → VSet.scanStart cursor ≤ v) (hnone : cell.nextElem cursor = none) (v : Nat) : (windowSet n st.lab tc len).mem v = true → Generic.Covers (prefixKey cs (vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells v)) best

The executable cursor terminator exhausts every live member at or after its scan start, closing coverage of the original target cell.

theorem Hex.GraphIso.Nauty.CellCover.frame {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc len : Nat} {cs : List Nat} {st out : Search n} {live : Nat → Prop} {best : Option (Key n)} (h : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hf : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hc : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hr : tc + len ≤ n) (hfuel : level + 1 + fuel ≤ n + 1) (hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true) : CellCover ctx tcLevel fuel level numcells tc len cs out live best

Restoring a parent can reorder its labels, but preserves every vertex-indexed child key and the accumulated coverage relation.

theorem Hex.GraphIso.Nauty.SweepPre.long_cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 len : Nat} {first : Bool} {cursor : Option Nat} {cell : VSet n} {st : Search n} {cs : List Nat} {live : Nat → Prop} {best : Option (Key n)} (h : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hc : IsCell st.ptn level tc len) (hr : tc + len ≤ n) (hfuel : level + 1 + fuel ≤ n + 1) (hcover : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true) (hmem : ∀ (v : Nat), live v → cell.mem v = true) : CellCover ctx tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ (longprune cell st.fixedpts st.autos).mem v = true) best

The actual long filter preserves coverage of the shrinking live set. It uses the restored sweep's local interpretation of fix-passing pairs.

theorem Hex.GraphIso.Nauty.SweepPre.short_cover {n k : Nat} {G : Colored n k} {ctx : Ctx n} {tcLevel fuel level numcells tc tv1 len : Nat} {first : Bool} {cursor : Option Nat} {cell : VSet n} {st : Search n} {cs : List Nat} {live : Nat → Prop} {best : Option (Key n)} (h : SweepPre G ctx tcLevel first level numcells tc tv1 cursor cell st) (hn0 : 0 < n) (hgsz : ctx.g.size = n) (hc : IsCell st.ptn level tc len) (hr : tc + len ≤ n) (hfuel : level + 1 + fuel ≤ n + 1) (hcover : CellCover ctx tcLevel fuel level numcells tc len cs st live best) (hsub : ∀ (v : Nat), live v → (windowSet n st.lab tc len).mem v = true) (hmem : ∀ (v : Nat), live v → cell.mem v = true) (hfix : ∀ (fix mcr : VSet n), st.autos.back? = some (fix, mcr) → st.fixedpts.subset fix = true) : CellCover ctx tcLevel fuel level numcells tc len cs st (fun (v : Nat) => live v ∧ (shortprune cell st).mem v = true) best

The actual short filter preserves ranked coverage once its newest pair passes the receiving loop's fix test.