theorem Hex.GraphIso.Nauty.Sparse.inverse_eq {n : Nat} {lab : Array Nat} (hsize : lab.size = n) : inverse n lab = invPerm lab

The sparse array loop computes the shared inverse permutation.

@[simp]

theorem Hex.GraphIso.Nauty.Sparse.inverse_size {n : Nat} {lab : Array Nat} (hsize : lab.size = n) : (inverse n lab).size = n

theorem Hex.GraphIso.Nauty.Sparse.inverse_get {n : Nat} {lab : Array Nat} (hsize : lab.size = n) (hinj : ∀ (a b : Nat), a < n → b < n → lab[a]! = lab[b]! → a = b) {i : Nat} (hi : i < n) (hv : lab[i]! < n) : (inverse n lab)[lab[i]!]! = i

Inverse scatter recovers a position from its vertex.

theorem Hex.GraphIso.Nauty.Sparse.inverse_lt {n : Nat} {lab : Array Nat} (hsize : lab.size = n) (hn : 0 < n) (v : Nat) : (inverse n lab)[v]! < n

Every entry of a nonempty inverse array is an in-range position.

theorem Hex.GraphIso.Nauty.Sparse.inverse_label {n : Nat} {lab : Array Nat} {l : Label n} (h : Label.ofArray? n lab = some l) (i : Fin n) : (inverse n lab)[↑(l.get i)]! = ↑i

A checked label supplies the permutation hypotheses of inverse scatter.

theorem Hex.GraphIso.Nauty.Sparse.inverse_toPerm {n : Nat} {lab : Array Nat} {l : Label n} (h : Label.ofArray? n lab = some l) (v : Fin n) : (inverse n lab)[↑v]! = ↑(l.toPerm.get v)

On a checked label, inverse scatter is its old-to-new transporter.