Verification run 2 -- A: the target mu_p (exact rational arithmetic unless said otherwise)
PASS  Lemma 2.1(a): the solution of the linear system equals the series (1) up to the tail (graphs with n <= 16, p >= 1/10)
PASS  Lemma 2.1(b): mu_p > 0 and mu_p(e) > mu_p(x) for x != e   (40 graphs x 9 values of p)
PASS  Lemma 2.1(d): 0 <= eps_x(p) <= q/p   (largest eps/(q/p) = 0.4997)
PASS  Lemma 2.1(c): spectral formula against the exact target (40 digits; largest deviation 9.18e-41)
PASS  Lemma 2.1(c): |mu_p(x) - 1/n| < 1e-7 at p = 1e-9 on all graphs (bipartite ones included), exact
PASS  Remark 2.2(a): target of the lazy walk at p equals mu_{p'}, p' = 2p/(1+p)  (exact)
PASS  Remark 2.2(b): target of the walk with a loop at p equals mu_{p''}, p'' = p(d+1)/(d+p)  (exact)
PASS  Remark 2.2(a),(b): tau' = 2 tau(p') and tau'' = ((d+1)/d) tau(p'')   (5 graphs, 3 values of p; largest deviation 6.24e-39)
PASS  Remark 2.2(c): theta/(1+theta) (1/(1+theta))^k = p q^k with p = theta/(1+theta)
PASS  Remark 2.2(d): P_p(e,e) > 0 for p > 0 on all graphs
   Z/16, S = {+-1,+-3}: |5| = 3, |6| = 2, 5 ~ 6: True
   mu_p(5) = 166302456507/2750816164792  = 0.060455678077
   mu_p(6) = 16623080149401/275081616479200  = 0.060429629439
   mu_p(5) - mu_p(6) = 2.604864e-05
PASS  Remark 2.3: |6| = 2, |5| = 3, adjacent, and mu_p(5) > mu_p(6) at p = 1/100 (exact)
   information: on the grid k/1000 the inequality mu_p(5) > mu_p(6) holds at 37 grid points, from p = 0.001 to p = 0.037; contiguous: True
PASS  Remark 2.3: at p = 999/1000 the target decreases along every edge leading away from e (all graphs)
PASS  Corollary 2.5: |tau(1e-12) - tau(0)| < 1e-8 on all graphs (largest 6.65e-11)
PASS  Lemma 6.2(a): g(e) > g(x) for all x != e  (exact, all graphs)
PASS  Lemma 6.2(b): |mu_p - 1/n - p g| <= C_1 p^2 for p <= 1/2  (largest left side / right side = 0.1667)

checks passed: 15   TOTAL failures: 0
