Verification run 2 -- B: the complete graph (exact rational / symbolic)
PASS  Proposition 3.1: 1 - 1/((n-1) pi_max) is an eigenvalue of P (exact determinant), 56 random rational targets, n = 2..8
PASS  Proposition 3.1: the only eigenvalue in (beta, 1] is 1 (exact root count), so the relaxation time is (n-1) pi_max
PASS  Section 3: P - I = (n/(n-1))(P_ind - I), rho = 1 - 1/(n pi_max), and rho is an eigenvalue of P_ind (exact)
PASS  Proposition 1.1: mu_p(e) = (1+(n-2)p)/(n-p), mu_p(x) = (1-p)/(n-p)   (symbolic, n = 2..9)
PASS  Proposition 1.1: (n-1) mu_p(e) = (n-1)/n + ((n-1)^3/n) p/(n-p)
PASS  Proposition 1.1: d tau/dp = (n-1)^3/(n-p)^2, tau(0) = (n-1)/n, tau(1-) = n-1; Remark 6.3(b): d(1/tau)/dp at 0 is -(n-1)
PASS  Remark 7.2(b): char. polynomial of P_p on K_n is (z-1)(z-beta_2)(z+1/(n-1))^(n-2), beta_2 = 1 - 1/tau(p)   (symbolic, n = 2..9)
PASS  Theorem 1.3(a): equality on K_n   (symbolic)
PASS  Proposition 1.1 through the general program: 77 exact cases (n = 2..12, 7 values of p)
PASS  Remark 7.2(b): on K_2, P_p = [[p, 1-p],[1, 0]] with eigenvalues 1 and -(1-p); tau = 1/(2-p), tau_abs = 1/p
PASS  Remark 7.2(b): on K_3, tau(p) < 2 = (n-1)/(n-2), so tau_abs is constant 2
PASS  Remark 7.2(b): for n >= 4, tau(0) < (n-1)/(n-2) < n-1 = tau(1-): tau_abs is non-decreasing and not constant

checks passed: 12   TOTAL failures: 0
