Verification run 2 -- E: Corollary 1.5 (bounded degree, two-sided spectral gap)
PASS  Corollary 1.5: all numerical inequalities used in the proof (ball size, 1/8 + 1/8, (3/4)(10/11)^11 >= 1/4, 7 kappa/32 >= kappa/5, t <= (r+6)/kappa, r/(2t) >= kappa/4, kappa r^2/80, r >= log_d n - 6 >= 0)
   PGL_2(F_31) with S = {s, a, a^-1}: n = 29760, d = 3, 32 d^6 = 23328
PASS  the graph is the Cayley graph of all of PGL_2(F_31) (n = 29760), d = 3, and n >= 32 d^6
   diameter 22; sizes of the balls of radius 0..8: [1, 4, 10, 22, 46, 89, 160, 276, 466]
   largest eigenvalues of K found (distinct values): [1.0, 0.96832675, 0.96705915, 0.96256025]
   smallest eigenvalues of K found (distinct values): [-0.97476948, -0.96752842, -0.96010057]
PASS  rho from the Lanczos method agrees with rho from a power iteration on the functions of mean zero (0.97476948)
   bipartite: False;  lambda_2 = 0.96832675;  rho = 0.97476948;  kappa = 0.023261;  tau(0) = 31.57238 <= 1/(1-rho) = 39.63453
PASS  0 < rho < 1; trace identity n/d = sum lambda_j^2 <= 2 + (n-2) rho^2; tau(0) <= 1/(1-rho)
   r = floor(log_d(n/32)) = 6;  t = 1 + ceil((r+4)/kappa) = 431;  p = 1/t = 0.002320
PASS  r >= 6, 32 d^r <= n, r + 5 <= t <= (r+6)/kappa
PASS  Step 1: max_x K^j(e,x) <= 2/n + rho^(j-1) for 1 <= j <= 17240   (largest left/right = 0.5000)
PASS  Step 2: P(|X(j)| <= r) <= 2 d^r (2/n + rho^(j-1)) for 1 <= j <= 17240
PASS  Step 3: P(|X(j)| <= r) <= 1/4 for t <= j <= 17240   (value at j = t: 0.00538; largest: 0.00538)
PASS  Step 1, intermediate: K^{2a}(e,e) <= 2/n + rho^{2a}
   P(A) = 0.009248  (bounds: 1 - exp(-kappa/4) = 0.005798, 7 kappa/32 = 0.005088, kappa/5 = 0.004652)
   P(B) >= 0.365477  (bound (3/4)(1-1/t)^t = 0.275589, 1/4)
PASS  Step 4: P(A) >= 1 - exp(-r/(2t)) >= 1 - exp(-kappa/4) >= 7 kappa/32 >= kappa/5
PASS  Step 4: P(B) >= (3/4)(1-1/t)^t >= (3/4)(10/11)^11 >= 1/4
   E Y = 14.13666, Var Y = 14.61734  (truncation error below 2.0e-15);  P(A) P(B) (r/2+1)^2 = 0.05408;  kappa r^2/80 = 0.01047
PASS  Step 4: Var(Y) >= P(A) P(B) (r/2+1)^2 >= kappa r^2/80
   tau(1/t) = 100.8251;  2 Var_p|x| = 29.2347 (from mu_p directly; from the walk: 29.2347);  kappa r^2/40 = 0.02093
PASS  Theorem 1.3(b) at p = 1/t: tau(1/t) >= 2 Var(Y) >= kappa r^2/40
   log_d n = 9.3763;  (kappa/40)(log_d n - 6)^2 = 0.00663
   tau(0.002) = 96.3724
   tau(0.005) = 122.8076
   tau(0.01) = 135.8538
   tau(0.02) = 134.1622
   tau(0.03) = 124.2257
   tau(0.05) = 103.5387
   tau(0.08) = 80.2674
   tau(0.12) = 60.4464
   tau(0.2) = 39.1746
   largest value found: tau(0.0100) = 135.8538;  ratio to tau(0) = 4.303;  ratio to d = 45.285
PASS  Corollary 1.5: sup_p tau(p) >= (kappa/40)(log_d n - 6)^2 on this graph

checks passed: 14   TOTAL failures: 0
