theorem Hex.GraphIso.Nauty.Sparse.breakout_match {n : Nat} (σ : Renaming n) (level first len o : Nat) (lab out ptn : Array Nat) (hp : lab.size = n) (hq : out.size = n) (hs : ptn.size = n) (hend : ptn[n - 1]! ≤ level) (hvals : ∀ (q : Nat), q < n → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (hc : IsCell ptn level first len) (hb : first + len ≤ n) (hn : 1 < len) (ho : o < len) (hperm : cellsPerm ptn level out (Array.map σ.toFun lab)) : ∃ (j : Nat), j < len ∧ out[first + j]! = σ.toFun lab[first + o]! ∧ cellsPerm (ptn.set! first (level + 1)) (level + 1) (breakout n out ptn (level + 1) first out[first + j]!).fst (Array.map σ.toFun (breakout n lab ptn (level + 1) first lab[first + o]!).fst)

Every enumerated member of a target cell has a corresponding member after renaming. The actual individualization rotations preserve cell equivalence on the new partition, despite different offsets and tie orders.