← Mathematical handbook

Exact finite-ranking equality at the reciprocal-even contact means

theorem Papers.AnsariRockel2026RhoFootrule.ranking_cauchy_equality_iff (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) : rankingSquare n π = rankingDistance n π ^ 2 / (↑n + 1) ↔ ∀ (i : Fin (n + 1)), |↑↑(π i) - ↑↑i| = rankingDistance n π / (↑n + 1)

Ordinary finite Cauchy--Schwarz is an equality precisely for constant absolute displacement.

theorem Papers.AnsariRockel2026RhoFootrule.ranking_constant_contact_iff (n N : ℕ) (hN : 0 < N) : (∃ (π : Equiv.Perm (Fin (n + 1))), ∀ (i : Fin (n + 1)), |↑↑(π i) - ↑↑i| = (↑n + 1) / (2 * ↑N)) ↔ 2 * N ∣ n + 1

The displayed constant-displacement formulation in Remark 2.2.

theorem Papers.AnsariRockel2026RhoFootrule.ranking_contact_equality_exists_iff (n N : ℕ) (hN : 0 < N) : (∃ (π : Equiv.Perm (Fin (n + 1))), rankingDistance n π / (↑n + 1) ^ 2 = 1 / (2 * ↑N) ∧ rankingSquare n π = rankingDistance n π ^ 2 / (↑n + 1)) ↔ 2 * N ∣ n + 1

Remark 2.2: equality at mean 1/(2N) is possible exactly for divisible ranking sizes.

theorem Papers.AnsariRockel2026RhoFootrule.finite_ranking_strict_correction (n : ℕ) (π : Equiv.Perm (Fin (n + 1))) (h0 : rankingDistance n π / (↑n + 1) ^ 2 ≠ 0) (hN : ∀ (N : ℕ), 0 < N → rankingDistance n π / (↑n + 1) ^ 2 ≠ 1 / (2 * ↑N)) : 0 < minimumVariance (rankingDistance n π / (↑n + 1) ^ 2) ∧ rankingDistance n π ^ 2 / (↑n + 1) < rankingSquare n π

Away from the reciprocal-even contact means, the finite correction is strictly positive.