verify_rqa.py: RQ-C independent verification of RQ-A MAIN_RESULT; data from RQ-A
Part I (symbolic identities, sympy from scratch)
  I Lemma3 at u=7/5,a=1/3,y>av: OK
  I Lemma3 at u=7/5,a=1/3,y<-au: OK
  I Lemma3 at u=7/5,a=1/3,y=0: OK
  I m1=0: OK
  I m2=1: OK
  I kappa3: OK
  I kappa4: OK
  I kappa5: OK
  I kappa6: OK
  I Lemma 9 expansion of E P(M): OK
  I L11(i) P(u)=l1(u): OK
  I L11(i) P'(u)=l1'(u): OK
  I L11(ii): OK
  I L11(iii) remainder of (P-l1)/(y-u)^2: OK
  I L11(iii) leading coeff of S1: OK
  I L11(iii) disc S1: OK
  I L11(iv): OK
  I L11(v) E P(chi): OK
  I L11(v) value: OK
  I L11(vi) e0: OK
  I L11(vi) e1: OK
  I L11(vi) e2: OK
  I L11(vi) e3: OK
  I L11(vi) e4: OK
  I L11(vi) l2(-z0-x)=qbx: OK
  I L12 step 4 factorisation: OK
  I Lemma 5 exact enumeration, 12 random rational (u, beta): OK
Part S (six-moment cells, exact Bernstein subdivision)
  S six-moment cells: 379/379 certified by exact Bernstein subdivision (1.4s)
    V1: max intervals 125, max depth 35, total intervals 15209
    V2: max intervals 127, max depth 38, total intervals 23379
    V3: max intervals 97, max depth 36, total intervals 20719
    V4: max intervals 1, max depth 0, total intervals 379
    tightest V4 (min h / target, float): 5.325e-06 cell ['6088209/4000000', '2460661/1600000', '321/400', '131/160']
    tightest V4 (min h / target, float): 2.584e-04 cell ['4797/3200', '1937/1280', '59/80', '603/800']
    tightest V4 (min h / target, float): 5.180e-04 cell ['5938209/4000000', '776887/500000', '0', '1/200']
    tightest V4 (min h / target, float): 5.733e-04 cell ['5938209/4000000', '776887/500000', '1/200', '1/100']
    tightest V4 (min h / target, float): 6.505e-04 cell ['5938209/4000000', '776887/500000', '1/100', '3/200']
Part Q (quartic boxes, exact rational interval arithmetic)
  Q quartic boxes: 641/641 certified in exact rational interval arithmetic, 3161 sub-boxes, max depth 6 (0.4s)
    min certified lower bound of kappa3*B0-4c4: 1.7708e-03
Part B (coverage, constants)
  B r1a: region matches Table 1: True; tiling True (5 u-strips x 32 a-breaks, bad strips 0); cells 94
  B r1b: region matches Table 1: True; tiling True (5 u-strips x 21 a-breaks, bad strips 0); cells 59
  B r1c: region matches Table 1: True; tiling True (4 u-strips x 8 a-breaks, bad strips 0); cells 32
  B r1d: region matches Table 1: True; tiling True (10 u-strips x 10 a-breaks, bad strips 0); cells 71
  B r2a: region matches Table 1: True; tiling True (4 u-strips x 4 a-breaks, bad strips 0); cells 16
  B r2b: region matches Table 1: True; tiling True (9 u-strips x 15 a-breaks, bad strips 0); cells 47
  B r3a: region matches Table 1: True; tiling True (4 u-strips x 4 a-breaks, bad strips 0); cells 16
  B r3b: region matches Table 1: True; tiling True (7 u-strips x 14 a-breaks, bad strips 0); cells 44
  B quartic boxes tile [611/400, ubar0] x [9/25, 471/1000] in (u,t): True (32 u-strips x 42 a-breaks, bad strips 0)
  B a(9/25) = 225/353 < 16/25: True;  a(471/1000) = 0.770968 > 77/100: True
  B pieces tile [1, ubar0] x [0, 1]: True (3 u-strips x 7 a-breaks, bad strips 0)
  B ubar0^4 - 2 ubar0^2 - 1 > 0: True;  ubar0 < 19/10: True
  B Lemma 14 constant (486/256)(1/10)(19/10)^2/(9/10)^3 = 0.9401042 < 0.9402: True
  B kappa4 < 0 on [1, ubar0] and ubar0^2 < 2+sqrt3: True
RESULT: ALL PARTS PASSED: ISQB  (4.7s)
