structure Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv {n : Nat} (σ : Renaming n) (level : Nat) (s t : RefineSt n) : Prop

Observable refinement equivalence allows independent scratch layouts, generations and orders within corresponding cells.

• ptn : t.ptn = s.ptn
• cells : cellsPerm s.ptn level t.lab (Array.map σ.toFun s.lab)
• control : CountTrace.control s = CountTrace.control t
• count : s.numcells = t.numcells

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.active {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) : s.active = t.active

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.queue {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) : s.queue = t.queue

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.code {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) : s.longcode = t.longcode

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.hash {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) (v : Nat) : Equiv σ level (s.hash v) (t.hash v)

The literal hash transition respects the observation relation.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.remove {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) (pos : Nat) : Equiv σ level { lab := s.lab, ptn := s.ptn, active := s.active.erase s.queue[pos]!, queue := (s.queue.set! pos s.queue[s.queue.size - 1]!).pop, cellstart := s.cellstart, cellend := s.cellend, indexed := s.indexed, hits := s.hits, marks := s.marks, vmarks := s.vmarks, stamp := s.stamp, numcells := s.numcells, longcode := s.longcode } { lab := t.lab, ptn := t.ptn, active := t.active.erase t.queue[pos]!, queue := (t.queue.set! pos t.queue[t.queue.size - 1]!).pop, cellstart := t.cellstart, cellend := t.cellend, indexed := t.indexed, hits := t.hits, marks := t.marks, vmarks := t.vmarks, stamp := t.stamp, numcells := t.numcells, longcode := t.longcode }

The production swap/pop removal respects the ordered-queue relation.

theorem Hex.GraphIso.Nauty.Sparse.RefineSt.Equiv.counts {n : Nat} {σ : Renaming n} {level : Nat} {s t : RefineSt n} (h : Equiv σ level s t) (first : Nat) (distance : Bool) (hs : Valid level s) (ht : Valid level t) (hc : IsCell s.ptn level first (s.cellend[first]! + 1 - first)) (hb : s.cellend[first]! < n) (hk : ∀ (q : Nat), first ≤ q → q ≤ s.cellend[first]! → s.hits[s.lab[q]!]! < n + 2) (hk' : ∀ (q : Nat), first ≤ q → q ≤ t.cellend[first]! → t.hits[t.lab[q]!]! < n + 2) (hv : ∀ (v : Nat), v ∈ segN s.lab first (s.cellend[first]! + 1 - first) → t.hits[σ.toFun v]! = s.hits[v]!) : Equiv σ level (splitCounts level first distance s) (splitCounts level first distance t)

Every actual count split transports under local key agreement.