def Hex.GraphIso.Nauty.ChildCover {α : Type u} (key : Nat → α) (rank : Nat → Nat) (all done live : Nat → Prop) : Prop

Every member of all is either covered already or has the same value as a no-larger member of live. The decreasing rank lets successive automorphism filters compose even when a new carrier lands outside the set the previous filter left.

Equations

• Hex.GraphIso.Nauty.ChildCover key rank all done live = Hex.GraphIso.Nauty.RelCover (fun (x y : Nat) => key x = key y) rank all done live

theorem Hex.GraphIso.Nauty.ChildCover.init {α : Type u} (key : Nat → α) (rank : Nat → Nat) (all : Nat → Prop) : ChildCover key rank all (fun (x : Nat) => False) all

Initially every child can witness itself in the live set.

theorem Hex.GraphIso.Nauty.ChildCover.step {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live done' live' : Nat → Prop} (h : ChildCover key rank all done live) (hs : ∀ (x : Nat), live x → (∀ (z : Nat), key z = key x → done' z) ∨ ∃ (y : Nat), live' y ∧ key x = key y ∧ rank y ≤ rank x) (hd : ∀ (x : Nat), done x → done' x) : ChildCover key rank all done' live'

One filtering step composes coverage transitively.

theorem Hex.GraphIso.Nauty.ChildCover.monoDone {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live done' : Nat → Prop} (h : ChildCover key rank all done live) (hd : ∀ (x : Nat), done x → done' x) : ChildCover key rank all done' live

Enlarging the covered set preserves coverage.

theorem Hex.GraphIso.Nauty.ChildCover.filter {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live live' : Nat → Prop} (h : ChildCover key rank all done live) (hs : ∀ (x : Nat), live x → ∃ (y : Nat), live' y ∧ key x = key y ∧ rank y ≤ rank x) : ChildCover key rank all done live'

Filtering the live set preserves coverage when every removed survivor repeats a no-larger survivor of the new set.

theorem Hex.GraphIso.Nauty.ChildCover.resolve {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live live' : Nat → Prop} (h : ChildCover key rank all done live) (hdone : ∀ (x y : Nat), key x = key y → done y → done x) (hstep : ∀ (x : Nat), live x → live' x ∨ ∃ (y : Nat), all y ∧ key x = key y ∧ rank y < rank x) (x : Nat) : live x → done x ∨ ∃ (y : Nat), live' y ∧ key x = key y ∧ rank y ≤ rank x

Resolving one filtered survivor may appeal to the coverage relation of the previous live set. Strict rank descent at every newly removed live vertex makes that recursion well founded.

theorem Hex.GraphIso.Nauty.ChildCover.filterDesc {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live live' : Nat → Prop} (h : ChildCover key rank all done live) (hdone : ∀ (x y : Nat), key x = key y → done y → done x) (hstep : ∀ (x : Nat), live x → live' x ∨ ∃ (y : Nat), all y ∧ key x = key y ∧ rank y < rank x) : ChildCover key rank all done live'

A descending filter preserves ranked coverage even when a carrier lands outside the live set it started from.

theorem Hex.GraphIso.Nauty.ChildCover.finish {α : Type u} {key : Nat → α} {rank : Nat → Nat} {all done live : Nat → Prop} (h : ChildCover key rank all done live) (hempty : ∀ (x : Nat), ¬live x) (x : Nat) : all x → done x

When no live survivor remains, every original child is covered.

theorem Hex.GraphIso.Nauty.ChildCover.bound {n : Nat} {key : Nat → Key n} {rank : Nat → Nat} {all done live : Nat → Prop} {b : Key n} (h : ChildCover key rank all done live) (hempty : ∀ (x : Nat), ¬live x) (hle : ∀ (x : Nat), done x → keyLe (key x) b) (x : Nat) : all x → keyLe (key x) b

Coverage transfers a common upper bound from covered children to all original children.

theorem Hex.GraphIso.Nauty.ChildCover.boundLive {n : Nat} {key : Nat → Key n} {rank : Nat → Nat} {all done live : Nat → Prop} {b : Key n} (h : ChildCover key rank all done live) (hdone : ∀ (x : Nat), done x → keyLe (key x) b) (hlive : ∀ (x : Nat), live x → keyLe (key x) b) (x : Nat) : all x → keyLe (key x) b

Coverage transfers a common upper bound when both the absorbed children and the surviving live representatives lie below it. This is the form a frozen comparison unwind uses: the ledger already covers the visited prefix, and the frozen code verdict covers the siblings the unwind skips.