noncomputable def Hex.GraphIso.Nauty.Sparse.State.toPartition {n : Nat} (numcells : Nat) (st : State n) : Nauty.RefineSt n

The shared partition interpretation of a native search state. This proof projection is never passed to executable dense refinement or search.

Equations

• Hex.GraphIso.Nauty.Sparse.State.toPartition numcells st = { lab := st.lab, ptn := st.ptn, active := st.active, numcells := numcells, hint := 0, maxpos := 0, longcode := 0 }

theorem Hex.GraphIso.Nauty.Sparse.Ready.iterOk {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) : IterOk (Graph.context G.graph) level (State.toPartition numcells st)

theorem Hex.GraphIso.Nauty.Sparse.Ready.small {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hc : cheapautom st.ptn level n = true) : SubtreeOk (Graph.context G.graph) level (State.toPartition numcells st)

A passing cheap guard supplies exactly the shared small-cell shape for the actual native equitable partition.

theorem Hex.GraphIso.Nauty.Sparse.Ready.transitive {n k : Nat} {G : Sparse.Colored n k} {level numcells : Nat} {st : State n} (h : Ready G level numcells st) (hn : 0 < n) (hl : 1 ≤ level) (hshape : NodeShape n level st.ptn) {tc te a b : Nat} (hc : (tc, te) ∈ cells st.ptn level n) (hne : tc < te) (ha : a ≤ te - tc) (hb : b ≤ te - tc) (hab : a ≠ b) : ∃ (σ : Renaming n), RowsMap σ (Graph.context G.graph).g (Graph.context G.graph).g ∧ cellsPerm st.ptn level st.lab (Array.map σ.toFun st.lab) ∧ st.lab[tc + b]! = σ.toFun st.lab[tc + a]!

At a native equitable node with the cheap shape, its cell stabilizer can carry either selected member of a cell to the other. The shared finite-graph argument consumes only the proved partition interpretation.