theorem Hex.GraphIso.Nauty.cellEnd_of_closed {ptn : Array Nat} {level i : Nat} (hi : i < ptn.size) (hc : ¬ptn[i]! > level) : cellEnd ptn level i = i

A position with a closed partition entry is its own cell end.

theorem Hex.GraphIso.Nauty.cellEnd_succ_of_open {ptn : Array Nat} {level i : Nat} (hi : i < ptn.size) (ho : ptn[i]! > level) : cellEnd ptn level i = cellEnd ptn level (i + 1)

A position with an open partition entry shares its cell end with its successor.

theorem Hex.GraphIso.Nauty.cellEnd_interior {ptn : Array Nat} {level i j : Nat} (hj : i ≤ j) (hlt : j < cellEnd ptn level i) : ptn[j]! > level

Interior positions of a cell run are open.

theorem Hex.GraphIso.Nauty.mem_cells_iff {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {c e : Nat} : (c, e) ∈ cells ptn level nn ↔ c < nn ∧ (c = 0 ∨ ptn[c - 1]! ≤ level) ∧ e = cellEnd ptn level c

Membership in the cell list: a start below the bound paired with its cell end.

theorem Hex.GraphIso.Nauty.cellEnd_succ_congr {ptn : Array Nat} {level : Nat} (hvals : ∀ (q : Nat), q < ptn.size → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) (i : Nat) : cellEnd ptn (level + 1) i = cellEnd ptn level i

Cell ends agree between adjacent levels when no entry sits at the intermediate value.

theorem Hex.GraphIso.Nauty.mem_cells_succ_congr {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) (hvals : ∀ (q : Nat), q < ptn.size → ptn[q]! ≤ level ∨ level + 1 < ptn[q]!) {c e : Nat} : (c, e) ∈ cells ptn (level + 1) nn ↔ (c, e) ∈ cells ptn level nn

Cell membership agrees between adjacent levels when no entry sits at the intermediate value.

theorem Hex.GraphIso.Nauty.cells_eq_of_shared {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {p q : Nat × Nat} (hp : p ∈ cells ptn level nn) (hq : q ∈ cells ptn level nn) {j : Nat} (hjp1 : p.fst ≤ j) (hjp2 : j ≤ p.snd) (hjq1 : q.fst ≤ j) (hjq2 : j ≤ q.snd) : p = q

Two cells of the partition list sharing a position coincide.