theorem Hex.GraphIso.Nauty.Sparse.Ready.small_key {n k : Nat} {G : Sparse.Colored n k} {level numcells tc len fuel v w : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hshape : NodeShape n level st.ptn) (hc : IsCell st.ptn level tc len) (hlen : 1 < len) (hr : tc + len ≤ n) (hv : (windowSet n st.lab tc len).mem v = true) (hw : (windowSet n st.lab tc len).mem w = true) (hf : n < fuel + (numcells + 1)) (tcLevel : Nat) : vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells v = vertexKey G.graph tcLevel fuel level st.lab st.ptn tc numcells w

At a native equitable partition with the cheap shape, every member of a target cell has the same complete unpruned sparse child key.

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.uniform {n k : Nat} {G : Sparse.Colored n k} {c : Cell n} (h : Valid G c) (hshape : NodeShape n c.level c.entry.ptn) {v w : Nat} (hv : c.vertices.mem v = true) (hw : c.vertices.mem w = true) (tcLevel : Nat) : key G.graph tcLevel c v = key G.graph tcLevel c w

Cheap-shape transitivity identifies the frozen keys of arbitrary original target vertices, irrespective of later filtering.

theorem Hex.GraphIso.Nauty.Sparse.Max.Cell.Valid.cover {n k : Nat} {G : Sparse.Colored n k} {tcLevel : Nat} {c : Cell n} {best : Option (Key n)} {v : Nat} (h : Valid G c) (hshape : NodeShape n c.level c.entry.ptn) (hv : c.vertices.mem v = true) (hc : Covers (key G.graph tcLevel c v) best) (live : Nat → Prop) : Cover G.graph tcLevel c live best

Covering any one complete child of a cheap target covers every original child, including those bypassed by a cheap-boundary return.