theorem Hex.GraphIso.Nauty.fixed_ne {α : Type} {f : α → α} {z u v : α} (hz : f z = z) (hu : f u = v) (hne : u ≠ v) : z ≠ u

A fixed point is distinct from either member of a nontrivial swap.

theorem Hex.GraphIso.Nauty.flip_iff {α : Type} {R : α → α → Bool} {f : α → α} {P : α → α → Prop} (hsymm : ∀ (u v : α), R u v = R v u) (hswap : ∀ (u v : α), P u v → f u = v ∧ f v = u) (hcover : ∀ (z : α), f z = z ∨ ∃ (u : α), ∃ (v : α), P u v ∧ (z = u ∨ z = v)) : (∀ (z w : α), R (f z) (f w) = R z w) ↔ (∀ (z : α), f z = z → ∀ (u v : α), P u v → R z u = R z v) ∧ ∀ (u v x y : α), P u v → P x y → R u x = R v y ∧ R u y = R v x

A map given by transpositions preserves adjacency exactly when fixed vertices see each pair alike and the adjacency between pairs agrees under simultaneous exchange. The cross conditions include a pair compared with itself, expressing equal loops and symmetry on that pair.

theorem Hex.GraphIso.Nauty.flip_bits {n : Nat} {ctx : Ctx n} {f : Nat → Nat} {P : Nat → Nat → Prop} (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hbound : ∀ (z : Nat), z < n → f z < n) (hswap : ∀ (u v : Nat), P u v → f u = v ∧ f v = u) (hcover : ∀ (z : Nat), z < n → f z = z ∨ ∃ (u : Nat), ∃ (v : Nat), u < n ∧ v < n ∧ P u v ∧ (z = u ∨ z = v)) (hfix : ∀ (z : Nat), z < n → f z = z → ∀ (u v : Nat), P u v → ctx.g[z]!.mem u = ctx.g[z]!.mem v) (hcross : ∀ (u v x y : Nat), P u v → P x y → ctx.g[u]!.mem x = ctx.g[v]!.mem y ∧ ctx.g[u]!.mem y = ctx.g[v]!.mem x) (z w : Nat) : z < n → w < n → ctx.g[f z]!.mem (f w) = ctx.g[z]!.mem w

The transposition criterion on the bounded vertex indices of a graph.

theorem Hex.GraphIso.Nauty.mem_image_invol {n : Nat} {f : Nat → Nat} {s : VSet n} (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) {z : Nat} (hz : z < n) : (VSet.image f s).mem z = s.mem (f z)

Image membership under a bounded involution reads off the preimage.

theorem Hex.GraphIso.Nauty.rows_of_bits {n : Nat} {ctx : Ctx n} {f : Nat → Nat} (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) (hbits : ∀ (z z' : Nat), z < n → z' < n → ctx.g[f z]!.mem (f z') = ctx.g[z]!.mem z') (v : Nat) : v < n → ctx.g[f v]! = VSet.image f ctx.g[v]!

Rows from value-level bit invariance.

def Hex.GraphIso.Nauty.sw1 (u v z : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.sw1 u v z = if z = u then v else if z = v then u else z

theorem Hex.GraphIso.Nauty.sw1_lt {n u v : Nat} (hun : u < n) (hvn : v < n) (z : Nat) : z < n → sw1 u v z < n

theorem Hex.GraphIso.Nauty.sw1_u {u v : Nat} : sw1 u v u = v

theorem Hex.GraphIso.Nauty.sw1_v {u v : Nat} (huv : u ≠ v) : sw1 u v v = u

theorem Hex.GraphIso.Nauty.sw1_fix {u v z : Nat} (hzu : z ≠ u) (hzv : z ≠ v) : sw1 u v z = z

theorem Hex.GraphIso.Nauty.sw1_invol {u v : Nat} (huv : u ≠ v) (z : Nat) : sw1 u v (sw1 u v z) = z

theorem Hex.GraphIso.Nauty.sw1_bits {n : Nat} {ctx : Ctx n} {u v : Nat} (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false) (hun : u < n) (hvn : v < n) (huv : u ≠ v) (hfix : ∀ (z : Nat), z < n → z ≠ u → z ≠ v → ctx.g[z]!.mem u = ctx.g[z]!.mem v) (z z' : Nat) : z < n → z' < n → ctx.g[sw1 u v z]!.mem (sw1 u v z') = ctx.g[z]!.mem z'

Bit invariance of a single swap: every other vertex has equal bits at the two swapped ones.

def Hex.GraphIso.Nauty.sw2 (u v x y z : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.sw2 u v x y z = if z = u then v else if z = v then u else if z = x then y else if z = y then x else z

def Hex.GraphIso.Nauty.Sw2Ok (n u v x y : Nat) : Prop

The distinctness bundle of an active double swap.

Equations

• Hex.GraphIso.Nauty.Sw2Ok n u v x y = (u < n ∧ v < n ∧ x < n ∧ y < n ∧ u ≠ v ∧ u ≠ x ∧ u ≠ y ∧ v ≠ x ∧ v ≠ y ∧ x ≠ y)

theorem Hex.GraphIso.Nauty.sw2_u {u v x y : Nat} : sw2 u v x y u = v

theorem Hex.GraphIso.Nauty.sw2_v {u v x y n : Nat} (h : Sw2Ok n u v x y) : sw2 u v x y v = u

theorem Hex.GraphIso.Nauty.sw2_x {u v x y n : Nat} (h : Sw2Ok n u v x y) : sw2 u v x y x = y

theorem Hex.GraphIso.Nauty.sw2_y {u v x y n : Nat} (h : Sw2Ok n u v x y) : sw2 u v x y y = x

theorem Hex.GraphIso.Nauty.sw2_fix {u v x y z : Nat} (hzu : z ≠ u) (hzv : z ≠ v) (hzx : z ≠ x) (hzy : z ≠ y) : sw2 u v x y z = z

theorem Hex.GraphIso.Nauty.sw2_lt {u v x y n : Nat} (h : Sw2Ok n u v x y) (z : Nat) : z < n → sw2 u v x y z < n

theorem Hex.GraphIso.Nauty.sw2_invol {u v x y n : Nat} (h : Sw2Ok n u v x y) (z : Nat) : sw2 u v x y (sw2 u v x y z) = z

theorem Hex.GraphIso.Nauty.sw2_bits {n : Nat} {ctx : Ctx n} {u v x y : Nat} (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false) (h : Sw2Ok n u v x y) (hfix : ∀ (z : Nat), z < n → z ≠ u → z ≠ v → z ≠ x → z ≠ y → ctx.g[z]!.mem u = ctx.g[z]!.mem v ∧ ctx.g[z]!.mem x = ctx.g[z]!.mem y) (hc1 : ctx.g[u]!.mem x = ctx.g[v]!.mem y) (hc2 : ctx.g[u]!.mem y = ctx.g[v]!.mem x) (z z' : Nat) : z < n → z' < n → ctx.g[sw2 u v x y z]!.mem (sw2 u v x y z') = ctx.g[z]!.mem z'

Bit invariance of a double swap: fixed vertices have equal bits at both swapped pairs, and the cross bits between the pairs match diagonally.

def Hex.GraphIso.Nauty.sw3 (u v x y a b z : Nat) : Nat

Equations

• Hex.GraphIso.Nauty.sw3 u v x y a b z = if z = u then v else if z = v then u else if z = x then y else if z = y then x else if z = a then b else if z = b then a else z

def Hex.GraphIso.Nauty.Sw3Ok (n u v x y a b : Nat) : Prop

The distinctness bundle of an active triple swap.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.sw3_u {u v x y a b : Nat} : sw3 u v x y a b u = v

theorem Hex.GraphIso.Nauty.sw3_v {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) : sw3 u v x y a b v = u

theorem Hex.GraphIso.Nauty.sw3_x {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) : sw3 u v x y a b x = y

theorem Hex.GraphIso.Nauty.sw3_y {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) : sw3 u v x y a b y = x

theorem Hex.GraphIso.Nauty.sw3_a {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) : sw3 u v x y a b a = b

theorem Hex.GraphIso.Nauty.sw3_b {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) : sw3 u v x y a b b = a

theorem Hex.GraphIso.Nauty.sw3_fix {u v x y a b z : Nat} (hzu : z ≠ u) (hzv : z ≠ v) (hzx : z ≠ x) (hzy : z ≠ y) (hza : z ≠ a) (hzb : z ≠ b) : sw3 u v x y a b z = z

theorem Hex.GraphIso.Nauty.sw3_lt {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) (z : Nat) : z < n → sw3 u v x y a b z < n

theorem Hex.GraphIso.Nauty.sw3_invol {u v x y a b n : Nat} (h : Sw3Ok n u v x y a b) (z : Nat) : sw3 u v x y a b (sw3 u v x y a b z) = z

theorem Hex.GraphIso.Nauty.sw3_bits {n : Nat} {ctx : Ctx n} {u v x y a b : Nat} (hsymm : ∀ (z w : Nat), z < n → w < n → ctx.g[z]!.mem w = ctx.g[w]!.mem z) (hloop : ∀ (z : Nat), z < n → ctx.g[z]!.mem z = false) (h : Sw3Ok n u v x y a b) (hfix : ∀ (z : Nat), z < n → z ≠ u → z ≠ v → z ≠ x → z ≠ y → z ≠ a → z ≠ b → ctx.g[z]!.mem u = ctx.g[z]!.mem v ∧ ctx.g[z]!.mem x = ctx.g[z]!.mem y ∧ ctx.g[z]!.mem a = ctx.g[z]!.mem b) (h1 : ctx.g[u]!.mem x = ctx.g[v]!.mem y) (h2 : ctx.g[u]!.mem y = ctx.g[v]!.mem x) (h3 : ctx.g[u]!.mem a = ctx.g[v]!.mem b) (h4 : ctx.g[u]!.mem b = ctx.g[v]!.mem a) (h5 : ctx.g[x]!.mem a = ctx.g[y]!.mem b) (h6 : ctx.g[x]!.mem b = ctx.g[y]!.mem a) (z z' : Nat) : z < n → z' < n → ctx.g[sw3 u v x y a b z]!.mem (sw3 u v x y a b z') = ctx.g[z]!.mem z'

A triple swap preserves every row when each swapped pair looks alike from outside and the three pairs cross each other coherently.

theorem Hex.GraphIso.Nauty.sw2_comp {n u v x y : Nat} (h : Sw2Ok n u v x y) (z : Nat) : sw2 u v x y z = sw1 u v (sw1 x y z)

Disjoint transpositions compose to the double swap.

theorem Hex.GraphIso.Nauty.sw3_comp {n u v x y a b : Nat} (h : Sw3Ok n u v x y a b) (z : Nat) : sw3 u v x y a b z = sw2 u v x y (sw1 a b z)

A disjoint double swap and transposition compose to the triple swap.

theorem Hex.GraphIso.Nauty.cellsPerm_self_setwise {n : Nat} {lab ptn : Array Nat} {level : Nat} {σ : Renaming n} (hps : ptn.size = n) (hlsz : lab.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) (hset : ∀ (p : Nat × Nat), p ∈ cells ptn level n → ∀ (o : Nat), o < p.snd + 1 - p.fst → ∃ (o' : Nat), o' < p.snd + 1 - p.fst ∧ σ.toFun lab[p.fst + o]! = lab[p.fst + o']!) : cellsPerm ptn level lab (Array.map σ.toFun lab)

A renaming permuting every cell's members within the cell is a cell-contents self-equivalence of the labelling.

theorem Hex.GraphIso.Nauty.stPerm_self_setwise {n : Nat} {f : Nat → Nat} {st : RefineSt n} {level : Nat} (hok : StOk n level st) (hinj : LabInj st.lab n) (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) (hset : ∀ (p : Nat × Nat), p ∈ cells st.ptn level n → ∀ (o : Nat), o < p.snd + 1 - p.fst → ∃ (o' : Nat), o' < p.snd + 1 - p.fst ∧ f st.lab[p.fst + o]! = st.lab[p.fst + o']!) : StPerm level st (mapSt (renamingOfFlip f n hfb hinvol) st)

The setwise self-equivalence packaged as StPerm, for a raw involution.

def Hex.GraphIso.Nauty.CellMap {n : Nat} (st : RefineSt n) (level : Nat) (f : Nat → Nat) : Prop

A vertex map sends every cell into itself.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.CellMap.comp {n : Nat} {st : RefineSt n} {level : Nat} {f g : Nat → Nat} (hf : CellMap st level f) (hg : CellMap st level g) : CellMap st level fun (v : Nat) => f (g v)

Composing maps that preserve each cell preserves each cell.

theorem Hex.GraphIso.Nauty.sw1_cells {n : Nat} {st : RefineSt n} {level c e a b : Nat} (hok : StOk n level st) (hinj : LabInj st.lab n) (hc : (c, e) ∈ cells st.ptn level n) (ha : a ≤ e - c) (hb : b ≤ e - c) (hab : a ≠ b) : CellMap st level (sw1 st.lab[c + a]! st.lab[c + b]!)

Swapping two members of one cell preserves all cells.

theorem Hex.GraphIso.Nauty.sw2_cells {n : Nat} {st : RefineSt n} {level u v x y : Nat} (h : Sw2Ok n u v x y) (h1 : CellMap st level (sw1 u v)) (h2 : CellMap st level (sw1 x y)) : CellMap st level (sw2 u v x y)

A disjoint double swap preserves cells when its two swaps do.

theorem Hex.GraphIso.Nauty.sw3_cells {n : Nat} {st : RefineSt n} {level u v x y a b : Nat} (h : Sw3Ok n u v x y a b) (h1 : CellMap st level (sw1 u v)) (h2 : CellMap st level (sw1 x y)) (h3 : CellMap st level (sw1 a b)) : CellMap st level (sw3 u v x y a b)

A disjoint triple swap preserves cells when its three swaps do.

theorem Hex.GraphIso.Nauty.flip_rows {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level : Nat} {S : Nat → Prop} {f : Nat → Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsurj : ∀ (v : Nat), v < n → ∃ (i : Nat), i < n ∧ lab[i]! = v) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (_hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) (hSpair : ∀ (p : Nat × Nat), p ∈ cells ptn level n → S p.fst → p.snd = p.fst + 1) (hSswap : ∀ (p : Nat × Nat), p ∈ cells ptn level n → S p.fst → f lab[p.fst]! = lab[p.fst + 1]! ∧ f lab[p.fst + 1]! = lab[p.fst]!) (hSfix : ∀ (p : Nat × Nat), p ∈ cells ptn level n → ¬S p.fst → ∀ (o : Nat), o < p.snd + 1 - p.fst → f lab[p.fst + o]! = lab[p.fst + o]!) (hSclosed : ∀ (p : Nat × Nat), p ∈ cells ptn level n → ∀ (q : Nat × Nat), q ∈ cells ptn level n → S p.fst → q.snd = q.fst + 1 → PairMatch ctx.g lab[p.fst]! lab[p.fst + 1]! lab[q.fst]! lab[q.fst + 1]! → S q.fst) (hOdd : ∀ (q : Nat × Nat), q ∈ cells ptn level n → q.snd ≠ q.fst + 1 → (q.snd + 1 - q.fst) % 2 = 1) (v : Nat) : v < n → ctx.g[f v]! = VSet.image f ctx.g[v]!

The flip theorem: an involution swapping the vertices of a matching-closed set of pair cells and fixing every other vertex preserves the adjacency rows.

theorem Hex.GraphIso.Nauty.triple_flip_rows {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level d : Nat} {f : Nat → Nat} (hE : Equitable ctx level lab ptn) (hps : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : ∀ (i j : Nat), i < n → j < n → lab[i]! = lab[j]! → i = j) (hlb : ∀ (i : Nat), i < n → lab[i]! < n) (hsurj : ∀ (v : Nat), v < n → ∃ (i : Nat), i < n ∧ lab[i]! = v) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hfb : ∀ (v : Nat), v < n → f v < n) (hinvol : ∀ (v : Nat), v < n → f (f v) = v) (hT : (d, d + 2) ∈ cells ptn level n) (hsmall : ∀ (q : Nat × Nat), q ∈ cells ptn level n → q ≠ (d, d + 2) → q.snd + 1 - q.fst ≤ 2) {a b : Nat} (ha : a < 3) (hb : b < 3) (hswap : f lab[d + a]! = lab[d + b]! ∧ f lab[d + b]! = lab[d + a]!) (hfix : ∀ (v : Nat), v < n → v ≠ lab[d + a]! → v ≠ lab[d + b]! → f v = v) (v : Nat) : v < n → ctx.g[f v]! = VSet.image f ctx.g[v]!

The triple flip theorem: the transposition of two triple members, fixing every other vertex, preserves the adjacency rows.

theorem Hex.GraphIso.Nauty.triple_flip_data {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc : Nat} (hIt : IterOk ctx level st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hE : Equitable ctx level st.lab st.ptn) (hT : (tc, tc + 2) ∈ cells st.ptn level n) (hsmall : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q ≠ (tc, tc + 2) → q.snd + 1 - q.fst ≤ 2) {a b : Nat} (ha : a < 3) (hb : b < 3) (hab : a ≠ b) : ∃ (σ : Renaming n), RowsMap σ ctx.g ctx.g ∧ StPerm level st (mapSt σ st) ∧ st.lab[tc + b]! = σ.toFun st.lab[tc + a]!

The flip data at a triple target: a row-preserving self-symmetry of the node carrying one child's individualized vertex to the other's.

inductive Hex.GraphIso.Nauty.PairReach {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level t : Nat) : Nat → Prop

The PairMatch-reachability closure of a pair-cell start.

• base {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} : PairReach ctx lab ptn level t t
• step {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t c e : Nat} : PairReach ctx lab ptn level t c → (c, c + 1) ∈ cells ptn level n → (e, e + 1) ∈ cells ptn level n → PairMatch ctx.g lab[c]! lab[c + 1]! lab[e]! lab[e + 1]! → PairReach ctx lab ptn level t e

theorem Hex.GraphIso.Nauty.cells_eq_of_start {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {c e e' : Nat} (h1 : (c, e) ∈ cells ptn level nn) (h2 : (c, e') ∈ cells ptn level nn) : e = e'

A cell is determined by its start.

theorem Hex.GraphIso.Nauty.pair_start_ne_second {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {c c' : Nat} (h1 : (c, c + 1) ∈ cells ptn level nn) (h2 : (c', c' + 1) ∈ cells ptn level nn) : c ≠ c' + 1

A pair start is never another pair's second position.

theorem Hex.GraphIso.Nauty.pairReach_pair {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t c : Nat} (hroot : (t, t + 1) ∈ cells ptn level n) (h : PairReach ctx lab ptn level t c) : (c, c + 1) ∈ cells ptn level n

Every member of the closure of a pair start is itself a pair-cell start.

theorem Hex.GraphIso.Nauty.pair_cells_disj {ptn : Array Nat} {level nn : Nat} (hnn : nn ≤ ptn.size) (hend : ptn[ptn.size - 1]! ≤ level) {c c' : Nat} (h1 : (c, c + 1) ∈ cells ptn level nn) (h2 : (c', c' + 1) ∈ cells ptn level nn) (hne : c ≠ c') : c + 2 ≤ c' ∨ c' + 2 ≤ c

Distinct closure pairs occupy disjoint positions.

noncomputable def Hex.GraphIso.Nauty.pairFlip {n : Nat} (ctx : Ctx n) (lab ptn : Array Nat) (level t : Nat) : Nat → Nat

The involution swapping every pair in the PairReach closure of t: a vertex that is a member of a closure pair maps to its partner, and every other vertex is fixed.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.GraphIso.Nauty.pairFlip_first {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) {c : Nat} (hr : PairReach ctx lab ptn level t c) (hcell : (c, c + 1) ∈ cells ptn level n) : pairFlip ctx lab ptn level t lab[c]! = lab[c + 1]!

The flip carries a closure pair's first member to its second.

theorem Hex.GraphIso.Nauty.pairFlip_second {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) {c : Nat} (hr : PairReach ctx lab ptn level t c) (hcell : (c, c + 1) ∈ cells ptn level n) : pairFlip ctx lab ptn level t lab[c + 1]! = lab[c]!

The flip carries a closure pair's second member to its first.

theorem Hex.GraphIso.Nauty.pairFlip_fix {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t v : Nat} (hnone : ∀ (c : Nat), PairReach ctx lab ptn level t c → (c, c + 1) ∈ cells ptn level n → v ≠ lab[c]! ∧ v ≠ lab[c + 1]!) : pairFlip ctx lab ptn level t v = v

The flip fixes every vertex that is not a closure-pair member.

theorem Hex.GraphIso.Nauty.pairFlip_lt {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} (hpsz : ptn.size = n) (hlsz : lab.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hlb : LabOk lab n) {v : Nat} (hv : v < n) : pairFlip ctx lab ptn level t v < n

The flip is bounded on the vertex range.

theorem Hex.GraphIso.Nauty.pairFlip_invol {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) {v : Nat} : pairFlip ctx lab ptn level t (pairFlip ctx lab ptn level t v) = v

The flip is an involution on the vertex range.

theorem Hex.GraphIso.Nauty.pairFlip_fix_cell {n : Nat} {ctx : Ctx n} {lab ptn : Array Nat} {level t : Nat} (hpsz : ptn.size = n) (hend : ptn[ptn.size - 1]! ≤ level) (hinj : LabInj lab n) {q : Nat × Nat} (hq : q ∈ cells ptn level n) (hnotS : ¬PairReach ctx lab ptn level t q.fst) {o : Nat} (ho : o < q.snd + 1 - q.fst) : pairFlip ctx lab ptn level t lab[q.fst + o]! = lab[q.fst + o]!

A member of a cell outside the closure is fixed by the flip: its position would otherwise sit inside a closure pair's window.

theorem Hex.GraphIso.Nauty.pair_flip_data {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level tc : Nat} (hIt : IterOk ctx level st) (hgsz : ctx.g.size = n) (hsymm : ∀ (u w : Nat), u < n → w < n → ctx.g[u]!.mem w = ctx.g[w]!.mem u) (hloop : ∀ (v : Nat), v < n → ctx.g[v]!.mem v = false) (hE : Equitable ctx level st.lab st.ptn) (hP : (tc, tc + 1) ∈ cells st.ptn level n) (hOdd : ∀ (q : Nat × Nat), q ∈ cells st.ptn level n → q.snd ≠ q.fst + 1 → (q.snd + 1 - q.fst) % 2 = 1) {a b : Nat} (ha : a < 2) (hb : b < 2) (hab : a ≠ b) : ∃ (σ : Renaming n), RowsMap σ ctx.g ctx.g ∧ StPerm level st (mapSt σ st) ∧ st.lab[tc + b]! = σ.toFun st.lab[tc + a]!

The flip data at a pair target: a row-preserving self-symmetry of the node carrying one child's individualized vertex to the other's.

theorem Hex.GraphIso.Nauty.flip_data_of_bits {n : Nat} {ctx : Ctx n} {st : RefineSt n} {level : Nat} {f : Nat → Nat} (hIt : IterOk ctx level st) (hgsz : ctx.g.size = n) (hfb : ∀ (w : Nat), w < n → f w < n) (hinvol : ∀ (w : Nat), w < n → f (f w) = w) (hbits : ∀ (z z' : Nat), z < n → z' < n → ctx.g[f z]!.mem (f z') = ctx.g[z]!.mem z') (hset : ∀ (p : Nat × Nat), p ∈ cells st.ptn level n → ∀ (o : Nat), o < p.snd + 1 - p.fst → ∃ (o' : Nat), o' < p.snd + 1 - p.fst ∧ f st.lab[p.fst + o]! = st.lab[p.fst + o']!) : ∃ (σ : Renaming n), RowsMap σ ctx.g ctx.g ∧ StPerm level st (mapSt σ st) ∧ ∀ (i : Nat), i < n → σ.toFun st.lab[i]! = f st.lab[i]!