OK   Lemma 3 identity on y > a v
OK   Lemma 3 identity on -a u <= y <= a v
OK   Lemma 3 identity on y < -a u
OK   q u = (1-q) v = tau
OK   E chi = 0, E chi^2 = 1
OK   m_k = q u^k + (1-q)(-v)^k
OK   kappa3 = u - v
OK   kappa4 = w - 4
OK   kappa5 = (u-v)(w-10)
OK   kappa6 = w^2 - 26 w + 64
OK   centred unit-variance kappa formulas (3..6)
OK   Lemma 5 moments vs exact enumeration (12 random rational cases, non-unit beta)
OK   (i) P(u) = l1(u)
OK   (i) P'(u) = l1'(u)
OK   (ii) B^2 - 4 c4 G = B0^2 - 4 c4 s
OK   (iii) (y-u)^2 divides P - l1
OK   (iii) S1 leading coeff c4
OK   (iii) disc S1 = B0^2 - 4 c4 (s + B0 (u+v))
OK   (iv) k3 c3 + 2 k4 c4 = k3 B0 - 4 c4
OK   (v) E P(chi) = q(1-q)(bu - av)
OK   (v) 2 tau a + 2 q(1-q)(bu-av) = 2 tau (1-q)(a+b)
OK   (vi) P(-z0-x) - l2(-z0-x) = e0 + e1 x + ... + c4 x^4
OK   (vi) l2(-z0-x) = q b x
OK   Lemma 10: E|a chi1 + b chi2| = 2 tau (1-q)(a+b) (exact, random rationals)
OK   ubar^4 - 2 ubar^2 - 1 > 0 (ubar > u0)
OK   ubar - u0 < 1e-7: (ubar-1e-7)^4 - 2(...)^2 - 1 < 0
OK   a(9/25) = 225/353 < 16/25
OK   a(471/1000) = 942000/1221841 > 77/100
OK   kappa4 < 0 on [1, 19/10]: u^4 - 4u^2 + 1 < 0 at u=1 and u=19/10 (convex in u^2)
OK   near-dictator constant 486/256*(1/10)(19/10)^2/(9/10)^3 = 0.9401042 < 0.9402
OK   (x - t)_+ <= 27/(256 t^3) x^4: max of (x-t)/x^4 at x = 4t/3 equals 27/(256 t^3)
OK   (1-q) u^3 = tau u^4 and q v^3 = tau v^4
OK   u0^4 + u0^-4 = 6
OK   d/da (1+a)^2/a^3 = -(1+a)(a+3)/a^4
OK   (1-q0)/q0 = 1 + sqrt2
ALL SYMBOLIC CHECKS: PASS
exit 0 elapsed 2 s
