MAIN-2 verifier (RQ-AUD), data: RQ-AUD/audit/rqa/k2_data
A  U_LO < u0 < U_LO + 1e-6: True; q(2) = 1/5: True; sqrt2-1 <= T8 < 1: True
A  Lemma 2C value 2 tau max(c, d, [s=+1](1-q)(c+d)) at 8000 random rational points: 0 mismatches
A  27x^4 - 256t^3(x-t) = (3x-4t)^2(3x^2+8tx+16t^2), q u = (1-q) v = tau, q tau, (1-q) tau: True
A  derivatives (monotonicity used): d/du (1-q)tau = -u**2*(u**2 - 3)/(u**2 + 1)**3; d/du q tau = -(3*u**2 - 1)/(u**2 + 1)**3; d/dt (c+d) = -2*(tt**2 + 2*tt - 1)/(tt**2 + 1)**2; d/dt (c-d) = 2*(tt**2 - 2*tt - 1)/(tt**2 + 1)**2
data: 450 one-coordinate cells; boxes s=+1: 17620, s=-1: 12704; kinds {'ncA': 1403, 'lp': 25959, 'small': 437, 'ncB': 2525}
B  one-coordinate cells tile ['1553773/1000000', '2', '0', '9/20']: OK; inside True; area equal True
B  s=+1: 17620 boxes inside region True; volume sum == region volume True; pairs with overlapping interiors 0  => TILING OK
B  s=-1: 12704 boxes inside region True; volume sum == region volume True; pairs with overlapping interiors 0  => TILING OK
F  'small' boxes: 437; with r2 c(t1) > 9/20: 0
C  one-coordinate cells, r2=MINE: failures 0/450, sub-cells 450, max depth 0, 11s
C  one-coordinate cells, r2=RQA-S2: failures 0/450, sub-cells 450, max depth 0, 11s
D  LP boxes, r2=MINE: failures 0/25959; certified at depth {0: 25959}; sub-boxes 25959, 21s
D  LP boxes, r2=RQA-S2: failures 0/25959; certified at depth {0: 25959}; sub-boxes 25959, 31s
E  near-circle boxes: failures 0/3928; passed by test {'1': 1406, '2': 2522}; sub-boxes 3928; boxes touching the sliver [U_LO, u0) (argument applies only at u >= u0): 173; 31s
RESULT: ALL CHECKS PASSED (parts ABCDEFR, 31s)
