def Hex.GraphIso.Nauty.Sparse.CanonLabel {n k : Nat} (G : Sparse.Colored n k) (st : State n) : Prop

The incumbent label fills each original colour cell with its own vertices. This asserts label validity, independently of maximality.

Equations

• Hex.GraphIso.Nauty.Sparse.CanonLabel G st = (st.canonlab.size = n ∧ Hex.GraphIso.Nauty.CellsReach G.toDense st.canonlab)

theorem Hex.GraphIso.Nauty.Sparse.FrameOut.canonical {n k : Nat} {G : Sparse.Colored n k} {base level : Nat} {st out : State n} (h : FrameOut G base level st out) (hc : CanonLabel G st) : CanonLabel G out

theorem Hex.GraphIso.Nauty.Sparse.CanonLabel.congr {n k : Nat} {G : Sparse.Colored n k} {st out : State n} (h : CanonLabel G st) (he : out.canonlab = st.canonlab) : CanonLabel G out

theorem Hex.GraphIso.Nauty.Sparse.Ready.canonical {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) : CanonLabel G (firstterminal level st)

Installing a reached leaf creates a complete, colour-respecting label.

theorem Hex.GraphIso.Nauty.Sparse.advance_canonical {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (first : Bool) (tcLevel fuel cfuel level numcells tc tv1 tv index : Nat) (cell : VSet n) (st out : State n) (exit : Generic.Exit) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hx : FrameOut G level level st out) (hc : CanonLabel G out) : CanonLabel G (Generic.advance (n + 2) (fun (first : Bool) (level numcells tc tv1 : Nat) (cursor : Option Nat) (cell : VSet n) (index : Nat) (st : State n) => Generic.sweep first (Graph.ofGraph G.graph) (n + 2) tcLevel fuel cfuel level numcells tc tv1 cursor cell index st) first level numcells tc tv1 tv cell index out exit).snd.snd

Recovery and all surviving siblings retain a valid incumbent installed by a child, even when its exit returns past the parent.

theorem Hex.GraphIso.Nauty.Sparse.sweep_first_canonical {n k : Nat} (G : Sparse.Colored n k) (hn : 0 < n) (tcLevel fuel cfuel level numcells tc tv index : Nat) (cell : VSet n) (st : State n) (hl : 1 ≤ level) (h : Ready G level numcells st) (ht : Generic.Target State.frame level tc cell st) (hv : cell.mem tv = true) (horbit : Generic.Policy.orbit st tv = tv) (hc : CanonLabel G (Generic.node true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (level + 1) (numcells + 1) (Generic.Policy.child true level tc tv st)).snd) : CanonLabel G (Generic.sweep true (Graph.ofGraph G.graph) (n + 2) tcLevel fuel (cfuel + 1) level numcells tc tv (some tv) cell index st).snd.snd

Once the first child installs a valid incumbent, the entire first-path sweep returns a valid incumbent. Later children may improve its label.