The search misses nothing

dfsNode_dom: every leaf of the whole tree that the search skipped was skipped for a reason, so the leaf it finally holds is the best one.

The obstacle is that pruneNode may clear the incumbent (st.best := none) when the node's invariant path already beats it. So "dominated by the incumbent" is not preserved into a recursive call, and cannot be the invariant. The fix is to carry an extra predicate D — "already accounted for by whoever called us" — and prove everything relative to

• DomD D st k — k is dominated by st's incumbent, or D k.

D is quantified inside the induction motive, so each recursive call may be made at a shifted predicate DomD D st; Guar's BestMono st0 st component is exactly what lets the shift be collapsed again on the way out (DomD.shift).

The other pieces:

• Dchild — every leaf below a given child of the current node is accounted for. dchild_gen says this set is closed under automorphisms fixing the path, which is what makes orbit pruning sound.
• Guar — what a returning call promises: it never asks to jump above the node it was called at, every leaf below the depth it vouches for is accounted for, and it kept the incumbent it was given. guar_stop / guar_go are the two ways a child can come back.
• stopDepth measures how far down the returning state actually vouches for: the whole subtree if it returned normally, only the part above the backjump target if it asked to jump.

def IsoGraph.Canon.DomD (D : List (List UInt64) → Prop) (st : St) (k : List (List UInt64)) : Prop

Dominated by the incumbent, or already accounted for by whoever called us.

Equations

• IsoGraph.Canon.DomD D st k = (IsoGraph.Canon.Dom st k ∨ D k)

theorem IsoGraph.Canon.DomD.up {D : List (List UInt64) → Prop} {st st' : St} {k : List (List UInt64)} (h : DomD D st k) (hm : BestMono st st') : DomD D st' k

theorem IsoGraph.Canon.DomD.shift {D : List (List UInt64) → Prop} {st st' : St} {k : List (List UInt64)} (h : DomD (DomD D st) st' k) (hm : BestMono st st') : DomD D st' k

theorem IsoGraph.Canon.DomD.of {D : List (List UInt64) → Prop} {st st' : St} {k : List (List UInt64)} (h : DomD D st k) : DomD (DomD D st) st' k

def IsoGraph.Canon.Dchild (n : ℕ) (f : ℕ → ℕ → Bool) (D : List (List UInt64) → Prop) (invPath : Array UInt64) (p : Part) (st : St) (w : ℕ) : Prop

Every leaf below the child w is accounted for.

Equations

• IsoGraph.Canon.Dchild n f D invPath p st w = (w < n ∧ ∀ (k : List (List UInt64)), IsoGraph.Canon.SubR n f invPath p w k → IsoGraph.Canon.DomD D st k)

theorem IsoGraph.Canon.Dchild.up {n : ℕ} {f : ℕ → ℕ → Bool} {D : List (List UInt64) → Prop} {invPath : Array UInt64} {p : Part} {st st' : St} {w : ℕ} (h : Dchild n f D invPath p st w) (hm : BestMono st st') : Dchild n f D invPath p st' w

theorem IsoGraph.Canon.dchild_gen {n : ℕ} {f : ℕ → ℕ → Bool} {D : List (List UInt64) → Prop} {path : Array ℕ} {invPath : Array UInt64} {p : Part} {st : St} (hnode : Node n f path invPath p) {g : Array ℕ} (hg : IsAutoArr n f g) (hfix : ∀ i < path.size, g[path[i]!]! = path[i]!) (w : ℕ) (h : Dchild n f D invPath p st w) : Dchild n f D invPath p st g[w]!

Orbit pruning is sound. A generator fixing the path maps accounted-for children to accounted-for children, because it carries the subtree below g w onto the subtree below w.

Small facts about unwind

theorem IsoGraph.Canon.unwind_abort {path : Array ℕ} {st : St} (h : (unwind path st).abortTo.isSome = true) : unwind path st = st ∧ ∃ (j : ℕ), st.abortTo = some j ∧ j < path.size

theorem IsoGraph.Canon.unwind_none {path : Array ℕ} {st : St} (h : (unwind path st).abortTo.isSome = false) : (unwind path st).abortTo = none

theorem IsoGraph.Canon.unwind_stop {path : Array ℕ} {st : St} (h : (unwind path st).abortTo.isSome = false) (hb : ∀ (j : ℕ), st.abortTo = some j → j < path.size + 1) : stopDepth (path.size + 1) st.abortTo = path.size + 1

Small facts about the state

theorem IsoGraph.Canon.pruneNode_rec {invPath : Array UInt64} {st st' : St} {l : Leaf} (h : pruneNode invPath st = some st') (hl : Rec st' l) : Rec st l

theorem IsoGraph.Canon.unwind_rec {path : Array ℕ} {st : St} {l : Leaf} (hl : Rec (unwind path st) l) : Rec st l

theorem IsoGraph.Canon.rec_iff_stq {st : St} {P : Array ℕ → Prop} : StQ P st ↔ ∀ (l : Leaf), Rec st l → P l.path

theorem IsoGraph.Canon.reach_leaf_key {n : ℕ} {f : ℕ → ℕ → Bool} {invPath : Array UInt64} {p : Part} (htc : p.targetCell n = none) {k : List (List UInt64)} (h : Reach n f invPath p k) : k = leafKey invPath (certOf (Graph.ofOracle n f) p.lab)

The orbit cache

theorem IsoGraph.Canon.orbRefresh_markP {n : ℕ} {f : ℕ → ℕ → Bool} {P : ℕ → Prop} {path processed : Array ℕ} {orb : Orbits} {st : St} (hgen : ∀ g ∈ usableAutos st.autos path, ∀ (w : ℕ), P w → P g[w]!) (hseed : ∀ w ∈ processed, P w) (hm : MarkP P orb.mark) : MarkP P (orbRefresh (Graph.ofOracle n f) path processed orb st).mark

theorem IsoGraph.Canon.orbRefresh_gens {n : ℕ} {f : ℕ → ℕ → Bool} {path processed : Array ℕ} {orb : Orbits} {st : St} (horb : ∀ g ∈ orb.gens, IsAutoArr n f g ∧ ∀ i < path.size, g[path[i]!]! = path[i]!) (hst : StGood n f st) (g : Array ℕ) : g ∈ (orbRefresh (Graph.ofOracle n f) path processed orb st).gens → IsAutoArr n f g ∧ ∀ i < path.size, g[path[i]!]! = path[i]!

theorem IsoGraph.Canon.Dchild.self_of {n : ℕ} {f : ℕ → ℕ → Bool} {D : List (List UInt64) → Prop} {invPath : Array UInt64} {p : Part} {st : St} {w : ℕ} (h : Dchild n f D invPath p st w) : Dchild n f (DomD D st) invPath p st w

def IsoGraph.Canon.Guar (n : ℕ) (f : ℕ → ℕ → Bool) (D : List (List UInt64) → Prop) (path : Array ℕ) (st0 st : St) : Prop

What a returning call guarantees: it never asks to jump above the node it was called at, and every leaf below the depth it vouches for is accounted for. st0 is the state it started from, whose incumbent it never loses.

Equations

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

theorem IsoGraph.Canon.guar_stop {n : ℕ} {f : ℕ → ℕ → Bool} {D : List (List UInt64) → Prop} {path : Array ℕ} {v : ℕ} {st0 st : St} (hg : Guar n f D (path.push v) st0 st) (h : (unwind path st).abortTo.isSome = true) : Guar n f D path st0 (unwind path st)

A child that came back asking to jump above us: the request passes through unchanged.

theorem IsoGraph.Canon.guar_go {n : ℕ} {f : ℕ → ℕ → Bool} {D : List (List UInt64) → Prop} {path : Array ℕ} {invPath : Array UInt64} {p : Part} {v : ℕ} {st0 st : St} (hnode : Node n f path invPath p) (hv : v < n) (hg : Guar n f D (path.push v) st0 st) (h : (unwind path st).abortTo.isSome = false) : Dchild n f D invPath p (unwind path st) v ∧ (unwind path st).abortTo = none ∧ BestMono st0 (unwind path st)

A child that came back normally: everything below it is accounted for.

theorem IsoGraph.Canon.dfsNode_dom (n : ℕ) (f : ℕ → ℕ → Bool) (fuel : ℕ) (path : Array ℕ) (invPath : Array UInt64) (p : Part) (st : St) (D : List (List UInt64) → Prop) : Node n f path invPath p → n + 1 ≤ numCells n p + fuel → st.abortTo = none → StGood n f st → Pth st path → Jmp n f (DomD D st) path st → Guar n f D path st (dfsNode (Graph.ofOracle n f) fuel path invPath p st)

The search misses nothing.