def Hex.GraphIso.Nauty.Sparse.CanonGuide {n : Nat} (level tc : Nat) (base : State n) (key : Nat → Key n) (best : Option (Key n)) (st : State n) : Prop

A canonical reference pointing to this sweep identifies a child whose native specification key is already covered by its incumbent. The base is the frozen parent frame, before sibling permutations and target filtering.

Equations

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

theorem Hex.GraphIso.Nauty.Sparse.CanonGuide.vacuous {n level tc : Nat} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : st.gcaCanon < level) : CanonGuide level tc base key best st

theorem Hex.GraphIso.Nauty.Sparse.CanonGuide.rebase {n k : Nat} {G : Sparse.Colored n k} {level tc : Nat} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : CanonGuide level tc base key best st) (hf : FrameOut G level level base st) : CanonGuide level tc st key best st

Completed sibling permutations preserve the reference's membership in the current cells, while its covered key still refers to the frozen base.

theorem Hex.GraphIso.Nauty.Sparse.CanonGuide.mem {n level tc len : Nat} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : CanonGuide level tc base key best st) (hok : LabOk base.lab n) (hc : IsCell base.ptn level tc len) (hr : tc + len ≤ base.lab.size) (he : st.gcaCanon = level) : ∃ (v : Nat), Covers (key v) best ∧ st.canonlab[tc]! = v ∧ (windowSet n base.lab tc len).mem v = true

The reference remains in the original target window even when an earlier filter has removed it from the mutable target set.

theorem Hex.GraphIso.Nauty.Sparse.CanonGuide.recover {n k : Nat} {G : Sparse.Colored n k} {level tc tv : Nat} {base st out : State n} {key : Nat → Key n} {before after : Option (Key n)} (h : CanonGuide level tc base key before st) (hbound : st.gcaCanon ≤ level) (hgrows : Grows before after) (hdone : Covers (key tv) after) (hframe : FrameOut G level level base st) (hreturn : out.gcaCanon ≤ st.gcaCanon ∧ out.canonlab = st.canonlab ∨ out.canonlab.size = st.lab.size ∧ cellsPerm st.ptn level st.lab out.canonlab ∧ out.canonlab[tc]! = tv) (inf : Nat) : CanonGuide level tc base key after (Generic.Policy.recover inf level out)

Actual recovery either retains the old covered child or selects the just-completed child, then clamps the canonical ancestor to this parent.

theorem Hex.GraphIso.Nauty.Sparse.child_canon_locate {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc tv : Nat} {cell : VSet n} {base st : State n} {key : Nat → Key n} {best : Option (Key n)} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (first childFirst : Bool) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hguide : CanonGuide level tc base key best st) : have out := (Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; out.gcaCanon = level → ∃ (v : Nat), Covers (key v) best ∧ out.canonlab[tc]! = v ∧ cellsPerm base.ptn level base.lab out.canonlab

A return pointing to its receiving parent retains that parent's previously covered reference, before any partition recovery occurs.

theorem Hex.GraphIso.Nauty.Sparse.child_canon_guide {n k : Nat} {G : Sparse.Colored n k} {tcLevel fuel level numcells tc tv1 tv : Nat} {first : Bool} {cell : VSet n} {base st : State n} {key : Nat → Key n} {before after : Option (Key n)} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (hbound : st.gcaCanon ≤ level) (hguide : CanonGuide level tc base key before st) (hframe : FrameOut G level level base st) (hgrows : Grows before after) (hdone : Covers (key tv) after) : have childFirst := first && tv == tv1; have raw := (Generic.node childFirst (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child first level tc tv st)).snd; have left := if childFirst = true then afterChildFirst level tv1 raw else raw; have out := Generic.Policy.leaveChild tv left; CanonGuide level tc base key after (Generic.Policy.recover (n + 2) level out)

The actual child return preserves the guide through first-child bookkeeping, fixed-point cleanup and parent recovery. Child coverage is the local induction premise; the reference provenance comes from the native call.