theorem Hex.GraphIso.Nauty.certInv_of_activeCells {n : Nat} {ctx : Ctx n} {level : Nat} {st : RefineSt n} (hactive : ∀ (p : Nat × Nat), p ∈ cells st.ptn level n → st.active.mem p.fst = true) : CertInv ctx level st

If every cell start is marked active, the refinement certificate invariant holds vacuously.

theorem Hex.GraphIso.Nauty.initial_cells_active {n k : Nat} (G : Colored n k) (hn0 : 0 < n) (p : Nat × Nat) : p ∈ cells (initPtn n (n + 2) (initialPartition G).snd) 1 n → (initActive n (initialPartition G).snd).mem p.fst = true

Every cell in the root ordered partition is initially active.

theorem Hex.GraphIso.Nauty.certInv_initial {n k : Nat} (G : Colored n k) (hn0 : 0 < n) : CertInv { g := rowsOf G } 1 { lab := (initialPartition G).fst, ptn := initPtn n (n + 2) (initialPartition G).snd, active := initActive n (initialPartition G).snd, numcells := (initialPartition G).snd.length, hint := 0, maxpos := 0, longcode := (initialPartition G).snd.length }

The root refinement state has the certificate invariant required by refine_equitable.