A. Bose weight: Farey step identity and lattice-sum identity
  [ok]   w(a)w(b) = w(c)(1+w(a)+w(b)) at 2000 random rational points (exact)
  [ok]   w1+w2+w0w1+w1w2+w2w3 = (1+w1+w3)(1+w0+w2)-(1+w0)(1+w3) at 500 points (exact)
  [ok]   sum_coprime w(1/(m/a+n/b)) = w(a)w(b) for (a,b)=(1,1)  diff 6.0e-60
  [ok]   sum_coprime w(1/(m/a+n/b)) = w(a)w(b) for (a,b)=(0.7,1.9)  diff 1.5e-58
  [ok]   sum_coprime w(1/(m/a+n/b)) = w(a)w(b) for (a,b)=(2.5,0.4)  diff 9.2e-59
  [ok]   sum_{q>=2} phi(q)/(e^q-1) = 1/(e-1)^2  value 0.33869688733846589456
B. Greedy packing of the Propp-Kenyon gap = Farey/Stern-Brocot disks (exact)
  [ok]   greedy disks with 1/s <= 40 are exactly the coprime (m,n), m+n <= 40, each once  489 disks
  [ok]   number of such disks = sum_{q=2}^{Q} phi(q)
  [ok]   base point of disk (m,n) is 2n/(m+n) - 1 and radius is 1/(m+n)^2
  [ok]   these disks and A, B are pairwise disjoint: |x-x'| >= 2ss' (exact)
  [ok]   row of four disks of radius 1/9 at -1/3,-1/9,1/9,1/3 is a packing of the gap
  [ok]   the greedy packing has exactly 3 disks of radius >= 1/9
C. Greedy value for the area: sum_{q>=2} phi(q)/q^4 = zeta(3)/zeta(4) - 1
  [ok]   partial sum (q <= 1e5) + [0, tail bound] contains zeta(3)/zeta(4) - 1  zeta(3)/zeta(4)-1 = 0.1106265353261481, area = 0.3475435106727186
        triangle area 2 - pi/2 = 0.429203673205, ratio = 0.809740
D. Key lemma: derivatives of w, the polynomial identity for Omega (exact)
  [ok]   w'(s) = q^2 E/(E-1)^2
  [ok]   w''(s) = q^3 E (q(E+1) - 2(E-1))/(E-1)^3
  [ok]   Omega: bracket form = x(X-1)U1 + (X-1)U2 + xU3 + U4 (polynomial identity)
  [ok]   Omega: two-line form in the paper equals the U-form
  [ok]   Psi = q^2 E Omega/((E-1)^4 x (X-1)) at 1000 random rational points (exact)
E. Key lemma: Taylor coefficients of Omega (exact)
  [ok]   closed forms of m![q^m]U1..U4 agree with the exact series, m <= 160
  [ok]   m![q^m](U2+U3) = (m+1)((m-4)2^(m-2)+2) for m>=2, 0 for m<=1
  [ok]   m![q^m](2U1+U2) = 2^(m-2)(m^2-m-8)+2(m+1) for m>=2
  [ok]   no negative coefficient of q^m x^n in Omega for m, n <= 160
  [ok]   [q^5 x^0] Omega = 1/6 and all coefficients with m+n <= 4 vanish
        smallest cases: m![q^m](2U1+U2), m=2..6: [0, 4, 26, 108, 366]
F. Numerical sanity checks (not part of any proof)
  [ok]   (log f_rho)'' by finite differences = (s+rho)Psi/f^2 > 0 (300 points, 80 digits)  max rel. dev. 1.6e-30
  [ok]   h is convex in theta on 400 random two-disk moves (double precision)
  [ok]   Phi(chain) <= w(a)w(b): 625 chains (k=2..6), after hill climbing  max (Phi - w(a)w(b))/(w(a)w(b)) = -1.64e-06
  [ok]   int_0^inf t^3 w(1/t)^2 dt = 6(zeta(3)-zeta(4)) (Simpson)  0.718402016691 vs 0.718402016691

TOTAL: ALL CHECKS PASSED  (15.4 s)
