[OK] b^2 + a^2 = 1
[OK] u + v = 1/tau
[OK] s = tau^3 (b u^2 - a)
[OK] B0 = tau^4 (2a - b(u^2-1))
[OK] P(u) = l1(u)
[OK] P'(u) = l1'(u)
[OK] P - l1 = (y-u)^2 Q1
[OK] disc(Q1) = B0^2 - 4 c4 (s + B0/tau)
[OK] c3 = B0 - 2 c4 k3
[OK] leading coefficient = c4
[OK] k3^2 - k4 = 2
[OK] k3 c3 + 2 k4 c4 = k3 B0 - 4 c4
[OK] E P(chi) via atoms = moment formula with p3 = p4 = 1
[OK] E P(M) - E P(chi) = c3 k3 (p3-1) + c4 k4 (p4-1)
[OK] P(-v) = 0 and P'(-v) = 0
[OK] 2 tau a + 2 q P(u) = 2 tau (1-q)(a+b)
[OK] E chi = 0, E chi^2 = 1
[OK] E chi^3 = k3
[OK] E chi^4 = 3 + k4
[OK] min_x>0 of 27x^4/(256t^3) - (x-t) is 0 (critical point x = 4t/3)
[OK] Lemma D constant at a = 9/10: 361/384 = 0.940104 < 0.9402
[OK] Lemma D constant decreasing on [9/10,1): d/da = 243*(aa - 3)*(aa + 1)/(128*aa**4)
[OK] u0^4 + u0^-4 = 6
[OK] u^4 + v^4 increasing on u >= 1 (derivative 4u^3 - 4u^-5 >= 0)
[OK] u0^2 + u0^-2 = 2 sqrt2
[OK] k4 = u^2 + v^2 - 4 <= 2 sqrt2 - 4 < 0 on [1, u0] (u^2+u^-2 increasing for u >= 1)
[OK] U = 776887/500000 >= u0 (U^2 - 1 = 1.4142136431, (U^2-1)^2 = 2.0000002283 >= 2)
[OK] t in [9/25, 471/1000] covers a in [16/25, 77/100] (a(t) increasing on [0,1])
[OK] a-strips: [0,16/25]: r1 (all u), [16/25,77/100]: r3 (u <= 611/400) + Q (u >= 611/400), [77/100,9/10]: r2 (all u), [9/10,1]: Lemma D
ALL IDENTITIES OK
