MAIN-3 verifier (RQ-AUD), data RQ-AUD/audit/rqa/k3_data; 97 data files
M  md5 of the 98 manifest files vs RQ-A k3_MD5SUMS.txt: 0 mismatches []
data: 2704 cells; boxes s=+1: 69871, s=-1: 12104; kinds {(-1, 'lp'): 11613, (-1, 'ncB'): 232, (-1, 'small'): 259, (1, 'lp'): 45720, (1, 'ms'): 21232, (1, 'ncA'): 1097, (1, 'ncB'): 1205, (1, 'small'): 617}
A  U_LO < u3 = sqrt(2+sqrt6), U_HI = 12/5 < u4 = sqrt(3+2sqrt3), q(12/5) = 25/169: True; sqrt2-1 <= T8 < 1: True; S3 (U_LO^2/(1+U_LO^2))^2 > 1.15 > 2/5: True
A  w = u^2 + u^-2 < 10 on the range (needed by the kappa_5 enclosure): True
A  Lemma 4 value 2 tau max(c, d, [s=+1](1-q)(c+d)) at 8000 random rational points: 0 mismatches
A  Lemma 4, k = 3 bound E|X|^2 < T^2 (c^2+d^2) at random rational u > u3: 0 violations
A  Lemma 3: E|chi_1+...+chi_k| = 2k(1-q)^(k-1) tau for k = 1..4 at 70 rational u in [2.11, 2.6): 0 mismatches
A  T = sqrt3 * 2u^5/(1+u^2)^3 and d/du u^5/(1+u^2)^3 = u^4(5-u^2)/(1+u^2)^4: True; T^2 - T2^2 ~ 4*(q - 1)**2*(3*q**2 - 6*q + 1) (zero at q3); (4(1-q)^3)^2 - (2 sqrt3 (1-q)^2)^2 ~ 4*(q - 1)**4*(4*q**2 - 8*q + 1) (zero at q4)
B  2704 one-coordinate cells tile ['2109381/1000000', '12/5', '0', '2/5']: OK; inside True; area True
B  s=+1: 69871 boxes inside True; volume sum == region volume True; overlapping pairs 0 => TILING OK
B  s=-1: 12104 boxes inside True; volume sum == region volume True; overlapping pairs 0 => TILING OK
F  small boxes: 876, violating r2 c(t1) <= 2/5: 0
H  three-bit lemma k = 3: 256 functions, P_f >= 0 on [25/169, q3] fails for 0; P_f == 0 exactly for 2 f (= +-OR_3: True); P_f(q3) = 0 for 6 f (= +-OR_2: True)
RESULT: ALL CHECKS PASSED (parts MABFH, 108s)

real	1m48.266s
user	1m45.563s
sys	0m3.438s
