Orbit closure

dfsChildren skips a child that is marked in orb.mark, the set of children in the orbit of the already-processed ones under the automorphisms fixing the node's path. This file proves the one fact that makes the skip legitimate: everything the closure marks is reachable from a seed by the generators, in the form

• orbitClosure_P / closureLoop_P — if a predicate P holds on the seeds and is closed under the generators, then it holds on everything marked.

Instantiated with P w := "the subtree below the child w is dominated" and combined with Autos.reach_child_auto, this says that skipping a marked child loses no leaf key.

Orbit closure

def IsoGraph.Canon.MarkP (P : ℕ → Prop) (mark : Array Bool) : Prop

mark only ever flags points satisfying P.

Equations

• IsoGraph.Canon.MarkP P mark = ∀ (w : ℕ), mark[w]! = true → P w

def IsoGraph.Canon.StackP (P : ℕ → Prop) (stack : Array ℕ) : Prop

Every entry of the frontier satisfies P.

Equations

• IsoGraph.Canon.StackP P stack = ∀ i < stack.size, P stack[i]!

theorem IsoGraph.Canon.markP_set {P : ℕ → Prop} {mark : Array Bool} {w : ℕ} (hm : MarkP P mark) (hw : P w) : MarkP P (mark.set! w true)

theorem IsoGraph.Canon.stackP_push {P : ℕ → Prop} {stack : Array ℕ} {w : ℕ} (hs : StackP P stack) (hw : P w) : StackP P (stack.push w)

theorem IsoGraph.Canon.stackP_pop {P : ℕ → Prop} {stack : Array ℕ} (hs : StackP P stack) : StackP P stack.pop

theorem IsoGraph.Canon.closure_foldl_P {P : ℕ → Prop} {v : ℕ} (hv : P v) (l : List (Array ℕ)) (ms : Array Bool × Array ℕ) : (∀ g ∈ l, P g[v]!) → MarkP P ms.1 → StackP P ms.2 → MarkP P (List.foldl (fun (ms : Array Bool × Array ℕ) (g : Array ℕ) => have w := g[v]!; if (!ms.1[w]!) = true then (ms.1.set! w true, ms.2.push w) else ms) ms l).1 ∧ StackP P (List.foldl (fun (ms : Array Bool × Array ℕ) (g : Array ℕ) => have w := g[v]!; if (!ms.1[w]!) = true then (ms.1.set! w true, ms.2.push w) else ms) ms l).2

theorem IsoGraph.Canon.closureStep_P {P : ℕ → Prop} {gens : Array (Array ℕ)} {mark : Array Bool} {stack : Array ℕ} {v : ℕ} (hgen : ∀ g ∈ gens, ∀ (w : ℕ), P w → P g[w]!) (hm : MarkP P mark) (hs : StackP P stack) (hv : P v) : MarkP P (closureStep gens mark stack v).1 ∧ StackP P (closureStep gens mark stack v).2

One closure step keeps the invariant. If P is closed under the generators, marking the images of a point satisfying P only ever marks points satisfying P.

theorem IsoGraph.Canon.closureLoop_P {P : ℕ → Prop} {gens : Array (Array ℕ)} (hgen : ∀ g ∈ gens, ∀ (w : ℕ), P w → P g[w]!) (fuel : ℕ) (mark : Array Bool) (stack : Array ℕ) : MarkP P mark → StackP P stack → MarkP P (closureLoop gens fuel mark stack)

The closure loop keeps the invariant.

theorem IsoGraph.Canon.markP_replicate {P : ℕ → Prop} {n : ℕ} : MarkP P (Array.replicate n false)

theorem IsoGraph.Canon.markP_seed_foldl {P : ℕ → Prop} (l : List ℕ) (mark : Array Bool) : (∀ v ∈ l, P v) → MarkP P mark → MarkP P (List.foldl (fun (mark : Array Bool) (v : ℕ) => mark.set! v true) mark l)

theorem IsoGraph.Canon.orbitClosure_P {P : ℕ → Prop} {n : ℕ} {gens : Array (Array ℕ)} {seed : Array ℕ} (hgen : ∀ g ∈ gens, ∀ (w : ℕ), P w → P g[w]!) (hseed : ∀ v ∈ seed, P v) : MarkP P (orbitClosure n gens seed)

Orbit closure is sound. Everything orbitClosure marks satisfies any predicate that holds on the seeds and is closed under the generators. Instantiated with "the subtree below this child is dominated", this is exactly what makes orbit pruning legitimate.