def Hex.GraphIso.Nauty.Sparse.RefineSt.toPartition {n : Nat} (s : RefineSt n) : Nauty.RefineSt n

The partition fields observed by the shared certificate algebra. This projection is confined to proofs and invokes no dense refinement routine.

Equations

• s.toPartition = { lab := s.lab, ptn := s.ptn, active := s.active, numcells := s.numcells, hint := 0, maxpos := 0, longcode := s.longcode }

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.stOk {n level : Nat} {s : RefineSt n} (h : Valid level s) : StOk n level s.toPartition

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.starts {n level : Nat} {s : RefineSt n} (h : Valid level s) : StartsOk level s.toPartition

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.injective {n level : Nat} {s : RefineSt n} (h : Valid level s) : LabInj s.lab n

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Valid.queue_mem {n level : Nat} {s : RefineSt n} {pos : Nat} (h : Valid level s) (hp : pos < s.queue.size) : s.active.mem s.queue[pos]! = true

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Step.refInv {n level : Nat} {s t : RefineSt n} (h : Step level s t) (hs : Valid level s) (ht : Valid level t) : RefInv level s.lab s.ptn t.toPartition

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.cert_transport {n level : Nat} {s t : RefineSt n} (G : SparseGraph n) (split : Nat) (hs : Valid level s) (ht : Valid level t) (hstep : Step level s t) (hb : split < n) (hm : s.active.mem split = true) (ha : Activation n level s.ptn t.ptn (s.active.erase split) t.active) (hc : ∀ (a len : Nat), IsCell t.ptn level a len → a + len ≤ n → ConstOn (Graph.context G) (worksetOf n s.lab split (cellEnd s.ptn level split)) (segN t.lab a len)) (hinv : CertInv (Graph.context G) level s.toPartition) : CertInv (Graph.context G) level t.toPartition

Sparse passes preserve the shared equitability certificate once their proved native count and activation properties are supplied.