Domination bookkeeping for the optimality proof

Small lemmas about how far down a returning search call has guaranteed that every leaf key is dominated by the incumbent, and about moving a subtree along an automorphism.

• Beaten.dom — a strictly beaten key is in particular dominated.
• stopDepth — the depth a returning call vouches for: its own depth when it ran to completion, and the backjump target's child depth when it was cut short.
• leafUpdate_dom_new — after recording a leaf, that leaf's key is dominated.
• leafUpdate_abort — a backjump request always points at the branch point with a leaf the state already holds, and only when the certificates tie.
• partEquiv_inv, subR_inv — an automorphism fixing a node carries the leaves below the child γ w onto the leaves below the child w, so the two children are interchangeable.

Domination helpers

theorem IsoGraph.Canon.Beaten.dom {st : St} {k : List (List UInt64)} (h : Beaten st k) : Dom st k

def IsoGraph.Canon.stopDepth (d : ℕ) : Option ℕ → ℕ

The depth to which a returning call guarantees that everything below is dominated: the node itself if it finished, the backjump target's child if it was cut short.

Equations

• IsoGraph.Canon.stopDepth d none = d
• IsoGraph.Canon.stopDepth d (some j) = min (j + 1) d

theorem IsoGraph.Canon.leafUpdate_dom_new (G : Graph) (path : Array ℕ) (invPath : Array UInt64) (lab : Array ℕ) (st : St) : Dom (leafUpdate G path invPath lab st) (leafKey invPath (certOf G lab))

A leaf update dominates the leaf it was given.

theorem IsoGraph.Canon.leafUpdate_abort {G : Graph} {path : Array ℕ} {invPath : Array UInt64} {lab : Array ℕ} {st : St} {j : ℕ} (h : (leafUpdate G path invPath lab st).abortTo = some j) : ∃ (l : Leaf), (st.first = some l ∨ st.best = some l) ∧ lexCmpU64 (certOf G lab) l.cert = Ordering.eq ∧ j = commonPrefix path l.path

A leaf update only ever asks to backjump to the branch point with a leaf it already holds, and only when the certificates tie.

Moving a subtree back along an automorphism

theorem IsoGraph.Canon.partEquiv_inv {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) {p : Part} (he : PartEquiv n (fun (x : ℕ) => g[x]!) p p) : PartEquiv n (fun (x : ℕ) => (invAuto n g)[x]!) p p

theorem IsoGraph.Canon.subR_inv {n : ℕ} {f : ℕ → ℕ → Bool} {g : Array ℕ} (hg : IsAutoArr n f g) {p : Part} (hp : Part.WF n p) (he : PartEquiv n (fun (x : ℕ) => g[x]!) p p) {invPath : Array UInt64} {w : ℕ} (hw : w < n) {k : List (List UInt64)} (h : SubR n f invPath p g[w]! k) : SubR n f invPath p w k

Orbit pruning, the direction the search needs. If γ fixes the node, the leaves below the child γ w are exactly the leaves below the child w.