← Mathematical handbook

Exact constant-displacement permutations at reciprocal-even means

def Verification.halfBlockSwap (k : ℕ) : Equiv.Perm (Fin (k + k))

Swap the two consecutive blocks of length k.

Equations

• Verification.halfBlockSwap k = finSumFinEquiv.symm.trans ((Equiv.sumComm (Fin k) (Fin k)).trans finSumFinEquiv)

theorem Verification.halfBlockSwap_distance (k : ℕ) (i : Fin (k + k)) : |↑↑((halfBlockSwap k) i) - ↑↑i| = ↑k

def Verification.repeatedHalfBlockSwap (N k : ℕ) : Equiv.Perm (Fin (N * (k + k)))

Repeat the block swap in N consecutive groups.

Equations

• Verification.repeatedHalfBlockSwap N k = finProdFinEquiv.symm.trans (((Equiv.refl (Fin N)).prodCongr (Verification.halfBlockSwap k)).trans finProdFinEquiv)

theorem Verification.repeatedHalfBlockSwap_distance (N k : ℕ) (i : Fin (N * (k + k))) : |↑↑((repeatedHalfBlockSwap N k) i) - ↑↑i| = ↑k

theorem Verification.exists_constant_displacement_permutation_iff (n N : ℕ) (hn : 0 < n) (hN : 0 < N) : (∃ (π : Equiv.Perm (Fin n)), ∀ (i : Fin n), |↑↑(π i) - ↑↑i| = ↑n / (2 * ↑N)) ↔ 2 * N ∣ n

The integrality condition in Remark 2.2, for arbitrary positive ranking size.