def Hex.GraphIso.Nauty.vertexKey {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (tc numcells v : Nat) : Key n

The child specification indexed by its individualized vertex.

Equations

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

theorem Hex.GraphIso.Nauty.vertexKey_offset {n : Nat} (ctx : Ctx n) (tcLevel fuel level : Nat) (lab ptn : Array Nat) (tc numcells offset : Nat) : vertexKey ctx tcLevel fuel level lab ptn tc numcells lab[tc + offset]! = childKey ctx tcLevel fuel level lab ptn tc numcells offset

Vertex and offset indexing give the same child specification.

theorem Hex.GraphIso.Nauty.SearchOk.vertex_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {st : Search n} {level numcells tc len v fuel : Nat} {γ : Array Nat} (h : SearchOk G level numcells st) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hgsz : ctx.g.size = n) (ha : checkAutom ctx.g γ = true) (hstab : CellStab st.ptn level st.lab γ) (hc : IsCell st.ptn level tc len) (hr : tc + len ≤ n) (hv : (windowSet n st.lab tc len).mem v = true) (hfuel : level + 1 + fuel ≤ n + 1) (tcLevel : Nat) : vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells v = vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells γ[v]!

A checked cell stabilizer identifies the child keys at the vertices it carries, independently of their offsets in the target cell.

theorem Hex.GraphIso.Nauty.SearchOut.breakoutPerm {n k : Nat} {G : Colored n k} {level numcells tc len o : Nat} {st out : Search n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) : ∃ (oCur : Nat), oCur < len ∧ out.lab[tc + oCur]! = st.lab[tc + o]! ∧ cellsPerm (st.ptn.set! tc (level + 1)) (level + 1) (breakout n st.lab st.ptn (level + 1) tc st.lab[tc + o]!).fst (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).fst

A recovered loop state individualizes the same vertex as its frozen entry frame, possibly at a different offset within the target cell. The two resulting child labellings remain cell-equivalent.

theorem Hex.GraphIso.Nauty.split_end {ptn : Array Nat} {level tc : Nat} (hend : ptn[ptn.size - 1]! ≤ level) (htc : tc < ptn.size) : (ptn.set! tc (level + 1))[(ptn.set! tc (level + 1)).size - 1]! ≤ level + 1

Splitting a nonempty cell start keeps the final partition position closed one level later.

theorem Hex.GraphIso.Nauty.split_starts {n : Nat} {ptn : Array Nat} {level tc len : Nat} (hcell : IsCell ptn level tc len) (hrange : tc + len ≤ n) (v : Nat) : (VSet.empty.insert tc).mem v = true → v = 0 ∨ (ptn.set! tc (level + 1))[v - 1]! ≤ level + 1

The active singleton created by individualization marks a cell start of the split partition.

theorem Hex.GraphIso.Nauty.SearchOut.child_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc len o specFuel tcLevel : Nat} {st out child : Search n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hcell : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hrange : tc + len ≤ n) (ho : o < len) (hclab : child.lab = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).fst) (hcptn : child.ptn = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).snd.fst) (hcactive : child.active = (breakout n out.lab out.ptn (level + 1) tc st.lab[tc + o]!).snd.snd) (hcanon : child.canonlab = out.canonlab) (hfuel : level + 1 + specFuel ≤ n + 1) : childKey ctx tcLevel specFuel level st.lab st.ptn tc numcells o = specNode ctx tcLevel specFuel (level + 1) child.lab child.ptn child.active (numcells + 1)

Individualizing the same vertex after recovering its parent leaves the specification child key unchanged, despite within-cell label movement.

theorem Hex.GraphIso.Nauty.SearchOut.vertex_key {n k : Nat} {G : Colored n k} {ctx : Ctx n} {level numcells tc len v fuel tcLevel : Nat} {st out : Search n} (h : SearchOut G level level st out) (hok : SearchOk G level numcells st) (hout : SearchOk G level numcells out) (hn0 : 0 < n) (hlevel : 1 ≤ level) (hc : IsCell st.ptn level tc len) (hlen : 2 ≤ len) (hr : tc + len ≤ n) (hv : (windowSet n st.lab tc len).mem v = true) (hfuel : level + 1 + fuel ≤ n + 1) : vertexKey ctx tcLevel fuel level st.lab st.ptn tc numcells v = vertexKey ctx tcLevel fuel level out.lab out.ptn tc numcells v

Recovery preserves each target vertex's child specification.

theorem Hex.GraphIso.Nauty.SearchOut.window_eq {n k : Nat} {G : Colored n k} {level tc len : Nat} {st out : Search n} (h : SearchOut G level level st out) (hc : IsCell st.ptn level tc len) : windowSet n st.lab tc len = windowSet n out.lab tc len

The recovered labelling has the same target-cell vertex set.