def Hex.Perm.Cycle.Follows {n : Nat} (p : Perm n) (c : Array (Fin n)) (next : Fin n) : Prop

The array follows the permutation, with next immediately after its last entry. This is the invariant maintained by the executable visit loop.

Equations

• Hex.Perm.Cycle.Follows p c next = ∀ (i : Nat) (hi : i < c.size), p.get c[i] = if hj : i + 1 < c.size then c[i + 1] else next

theorem Hex.Perm.Cycle.follows_empty {n : Nat} (p : Perm n) (x : Fin n) : Follows p #[] x

theorem Hex.Perm.Cycle.Follows.push {n : Nat} {p : Perm n} {c : Array (Fin n)} {x : Fin n} (h : Follows p c x) : Follows p (c.push x) (p.get x)

theorem Hex.Perm.Cycle.nodup_size {n : Nat} {c : Array (Fin n)} (h : c.toList.Nodup) : c.size ≤ n

theorem Hex.Perm.Cycle.get_injective {n : Nat} {c : Array (Fin n)} (h : c.toList.Nodup) {i j : Nat} (hi : i < c.size) (hj : j < c.size) (he : c[i] = c[j]) : i = j

theorem Hex.Perm.Cycle.Follows.return_first {n : Nat} {p : Perm n} {c : Array (Fin n)} {x : Fin n} (h : Follows p c x) (hd : c.toList.Nodup) (hx : x ∈ c) : ∃ (hc : 0 < c.size), x = c[0]

A path without repeated entries can first return only to its first entry: a return to a later entry would give its predecessor two equal images.

def Hex.Perm.Cycle.Valid {n : Nat} (p : Perm n) (c : Array (Fin n)) : Prop

A nonempty, duplicate-free array records one complete directed cycle, including the singleton cycle of a fixed point.

Equations

• Hex.Perm.Cycle.Valid p c = (c.toList.Nodup ∧ ∃ (hc : 0 < c.size), Hex.Perm.Cycle.Follows p c c[0])

theorem Hex.Perm.Cycle.Follows.valid {n : Nat} {p : Perm n} {c : Array (Fin n)} {x : Fin n} (h : Follows p c x) (hd : c.toList.Nodup) (hx : x ∈ c) : Valid p c

theorem Hex.Perm.Cycle.Valid.nonempty {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) : 0 < c.size

theorem Hex.Perm.Cycle.Valid.get {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (i : Nat) (hi : i < c.size) : p.get c[i] = c[(i + 1) % c.size]

The wrap-around successor equation gives a direct reconstruction rule.

theorem Hex.Perm.Cycle.Valid.closed {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) {x : Fin n} (hx : x ∈ c) : p.get x ∈ c

theorem Hex.Perm.Cycle.Valid.mem_iff {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (x : Fin n) : p.get x ∈ c ↔ x ∈ c

theorem Hex.Perm.Cycle.Valid.pow_get {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (k i : Nat) (hi : i < c.size) : (p.pow k).get c[i] = c[(i + k) % c.size]

theorem Hex.Perm.Cycle.Valid.period {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (x : Fin n) (hx : x ∈ c) : (p.pow c.size).get x = x

theorem Hex.Perm.Cycle.Valid.dvd_period {n : Nat} {p : Perm n} {c : Array (Fin n)} (h : Valid p c) (k : Nat) (hk : (p.pow k).get c[0] = c[0]) : c.size ∣ k

Returning the first point forces the exponent to be divisible by the cycle length. In particular, no smaller positive period is possible.