check_note.py -- OWR-12339-003; Python 3.13.5
== A. exact lattice arithmetic
PASS  A1 M = A_3^T A_3 = [[1,2/5],[2/5,1]], det M = (det A_3)^2 = 21/25
PASS  A2 (|Q| c^2)^2 = 100/21, i.e. |Q| c^2 = 10/sqrt(21); for the window exp(-pi a|s|^2): 10a/sqrt(21)
PASS  A3 M^{-1} = (1/21)[[25,-10],[-10,25]]
PASS  A4 5M integral and Gamma = M^{-1}Z^2 meets Z^2 exactly in 5Z^2
PASS  A5 [Gamma : 5Z^2] = 25 det M = 21, [Z^2 : 5Z^2] = 25
PASS  A6 r_j = M^{-1}(0,j), j = 0..20, lie in Gamma and are incongruent mod 5Z^2
PASS  A7 certificate a=1: kappa and r_b are complete residue systems, centred; gauge in (1/1024)Z
PASS  A7 certificate a=1/2: kappa and r_b are complete residue systems, centred; gauge in (1/1024)Z
PASS  A8 Z^2 + Gamma = Z w1 + Z w2 with w1 = (3,3)/21, w2 = (-2,5)/21 (covolume 1/21)
PASS  A9 on D, |t|_inf <= 11/42 (t1 in [-1/21, 1/7], t2 in [0, 11/42])
PASS  A10 every (t, theta) is mapped into D by the symmetries (20000 exact random points)
== B. tail bounds (Lemma 4.3)
PASS  B1 5/2 + 11/42 = 58/21 and the eigenvalues of M are 7/5 and 3/5 (trace 2, det 21/25)
PASS  B2 a = 1.0: entrywise tail <= 2.092e-42 < 2.1e-42, ||T||_2 <= sqrt(525) tau = 4.794e-41 < 4.8e-41
PASS  B2 a = 0.5: entrywise tail <= 5.815e-21 < 6.0e-21, ||T||_2 <= sqrt(525) tau = 1.332e-19 < 1.4e-19
== C. lattice facts used in Section 6
PASS  C1 min of m^* M m over Z[i]^2 \ 0 is 1 (values <= 1 need |m1|^2 + |m2|^2 <= 5/3, all searched)
PASS  C2 CVEE Cor. 4.3 would need q^2 = 25/4, q = 5/2 not in N
PASS  C3 CVEE Thm 4.1 / Cor. 4.2 would need alpha = 1 and |q|^2 = 25/4, not an integer
PASS  C4 discriminant of [5,-4,5] is -84 and 84/4 = 21 is not a square
== D. the symbol in pure Python
PASS  D1 Lambda_3: sigma_min(P) at t = (1/14,1/14), theta = (1/2,1/2) is 0.2370731445  [0.2370731445]
PASS  D2 P^* P equals the Gram symbol of the Ron-Shen fibre operator (k-sums) at a random point  [7.8e-16]
PASS  D3 Lambda_1 (not a frame, CVEE Thm 4.1): P is 25 x 24 and lambda_min(P^*P) at t = (5/6,1/3), theta = (1/2,1/2) is 4.2e-17 (an exact zero up to rounding)
PASS  D4 symmetries (i)-(iii) and translations by w1, w2 at a random point  [2.8e-16]
== F. constants of Theorems 1.2 and 1.3
PASS  F1 (10/sqrt 21) 0.23^2 = 0.115437 > 0.1154
PASS  F2 (5/sqrt 21) 0.18^2 = 0.035351 > 0.0353 (window exp(-pi|s|^2/2), normalised)
PASS  F3 numerical value (10/sqrt 21) 0.2370731445^2 = 0.12265 (not part of the theorem)
PASS  F4 exact: ((10 * 529/10000)^2)/21 > (1154/10000)^2
== E. the certificates
PASS  E1 a = 1: the 65597 boxes partition D  [65597 boxes, finest grid 128x64x32x64 = 16777216 cells, uncovered 0]
PASS  E2 a = 1: window parameter and target stored as 1.0, 0.23; every stored bound >= target
PASS  E3 a = 1, box 49203 (stored bound 0.230000149): recomputed smin 0.240811453, E1 0.009956, R2 0.000855, bound 0.230000149 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 45448 (stored bound 0.230000301): recomputed smin 0.242978297, E1 0.011823, R2 0.001154, bound 0.230000301 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 19827 (stored bound 0.230000333): recomputed smin 0.253438139, E1 0.019925, R2 0.003512, bound 0.230000333 >= 0.23  [max dev from stored 6.9e-18]
PASS  E3 a = 1, box 50547 (stored bound 0.230000593): recomputed smin 0.241438781, E1 0.010585, R2 0.000852, bound 0.230000593 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 46960 (stored bound 0.230000629): recomputed smin 0.240785563, E1 0.009932, R2 0.000852, bound 0.230000629 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 33169 (stored bound 0.230000697): recomputed smin 0.246124836, E1 0.014336, R2 0.001787, bound 0.230000697 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 44357 (stored bound 0.230000748): recomputed smin 0.242941221, E1 0.011793, R2 0.001146, bound 0.230000748 >= 0.23  [max dev from stored 3.5e-18]
PASS  E3 a = 1, box 57642 (stored bound 0.230000774): recomputed smin 0.239197283, E1 0.008594, R2 0.000602, bound 0.230000774 >= 0.23  [max dev from stored 3.5e-18]
PASS  E3 a = 1, box 9209 (stored bound 0.230000776): recomputed smin 0.266023586, E1 0.028551, R2 0.007470, bound 0.230000776 >= 0.23  [max dev from stored 6.9e-18]
PASS  E3 a = 1, box 22283 (stored bound 0.230000892): recomputed smin 0.253491812, E1 0.019981, R2 0.003509, bound 0.230000892 >= 0.23  [max dev from stored 0.0e+00]
PASS  E3 a = 1, box 159 (stored bound 0.230001134): recomputed smin 0.299043141, E1 0.048885, R2 0.020156, bound 0.230001134 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 27791 (stored bound 0.230001149): recomputed smin 0.249644158, E1 0.017176, R2 0.002466, bound 0.230001149 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 51384 (stored bound 0.230001151): recomputed smin 0.241481160, E1 0.010623, R2 0.000856, bound 0.230001151 >= 0.23  [max dev from stored 2.2e-16]
PASS  E3 a = 1, box 59005 (stored bound 0.230001183): recomputed smin 0.239191090, E1 0.008587, R2 0.000602, bound 0.230001183 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 21049 (stored bound 0.230001226): recomputed smin 0.254751172, E1 0.021254, R2 0.003495, bound 0.230001226 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 9035 (stored bound 0.230001331): recomputed smin 0.265955845, E1 0.028506, R2 0.007447, bound 0.230001331 >= 0.23  [max dev from stored 1.4e-16]
PASS  E3 a = 1, box 54863 (stored bound 0.230001348): recomputed smin 0.239187461, E1 0.008585, R2 0.000600, bound 0.230001348 >= 0.23  [max dev from stored 1.4e-16]
PASS  E3 a = 1, box 24096 (stored bound 0.230001374): recomputed smin 0.253475687, E1 0.019958, R2 0.003515, bound 0.230001374 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 25611 (stored bound 0.230001382): recomputed smin 0.249654448, E1 0.017185, R2 0.002467, bound 0.230001382 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 50190 (stored bound 0.230001395): recomputed smin 0.241426144, E1 0.010572, R2 0.000852, bound 0.230001395 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 21469 (stored bound 0.230001547): recomputed smin 0.253437949, E1 0.019931, R2 0.003504, bound 0.230001547 >= 0.23  [max dev from stored 3.5e-18]
PASS  E3 a = 1, box 54716 (stored bound 0.230001653): recomputed smin 0.239204267, E1 0.008601, R2 0.000601, bound 0.230001653 >= 0.23  [max dev from stored 1.4e-16]
PASS  E3 a = 1, box 15099 (stored bound 0.230001778): recomputed smin 0.258400161, E1 0.023692, R2 0.004705, bound 0.230001778 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 4688 (stored bound 0.230001807): recomputed smin 0.273902713, E1 0.033448, R2 0.010452, bound 0.230001807 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 46560 (stored bound 0.230001828): recomputed smin 0.240804288, E1 0.009947, R2 0.000854, bound 0.230001828 >= 0.23  [max dev from stored 1.7e-18]
PASS  E3 a = 1, box 2610 (stored bound 0.230001828): recomputed smin 0.274963366, E1 0.034503, R2 0.010458, bound 0.230001828 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 29351 (stored bound 0.230001881): recomputed smin 0.249471786, E1 0.017002, R2 0.002467, bound 0.230001881 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 1152 (stored bound 0.230002022): recomputed smin 0.287495092, E1 0.042619, R2 0.014873, bound 0.230002022 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 59053 (stored bound 0.230002036): recomputed smin 0.239213115, E1 0.008608, R2 0.000602, bound 0.230002036 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 24878 (stored bound 0.230002178): recomputed smin 0.249635437, E1 0.017165, R2 0.002467, bound 0.230002178 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 48598 (stored bound 0.230002212): recomputed smin 0.240805594, E1 0.009948, R2 0.000854, bound 0.230002212 >= 0.23  [max dev from stored 1.7e-18]
PASS  E3 a = 1, box 62792 (stored bound 0.230002312): recomputed smin 0.237615424, E1 0.007173, R2 0.000439, bound 0.230002312 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 40744 (stored bound 0.230002335): recomputed smin 0.242982900, E1 0.011833, R2 0.001146, bound 0.230002335 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 18606 (stored bound 0.230002372): recomputed smin 0.258171322, E1 0.023434, R2 0.004734, bound 0.230002372 >= 0.23  [max dev from stored 2.2e-16]
PASS  E3 a = 1, box 29908 (stored bound 0.230002445): recomputed smin 0.249566995, E1 0.017094, R2 0.002470, bound 0.230002445 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 9105 (stored bound 0.230002596): recomputed smin 0.265714069, E1 0.028262, R2 0.007449, bound 0.230002596 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 25692 (stored bound 0.230002677): recomputed smin 0.249641739, E1 0.017173, R2 0.002465, bound 0.230002677 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 54629 (stored bound 0.230002721): recomputed smin 0.239213451, E1 0.008608, R2 0.000602, bound 0.230002721 >= 0.23  [max dev from stored 0.0e+00]
PASS  E3 a = 1, box 33174 (stored bound 0.230002810): recomputed smin 0.246099251, E1 0.014309, R2 0.001787, bound 0.230002810 >= 0.23  [max dev from stored 2.2e-16]
PASS  E3 a = 1, box 53984 (stored bound 0.230002910): recomputed smin 0.239186650, E1 0.008583, R2 0.000600, bound 0.230002910 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 42445 (stored bound 0.232081901): recomputed smin 0.245006594, E1 0.011780, R2 0.001143, bound 0.232081901 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 19772 (stored bound 0.231984935): recomputed smin 0.256816505, E1 0.021324, R2 0.003507, bound 0.231984935 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 51750 (stored bound 0.230366398): recomputed smin 0.241798994, E1 0.010578, R2 0.000853, bound 0.230366398 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 6328 (stored bound 0.233115427): recomputed smin 0.280141268, E1 0.036115, R2 0.010910, bound 0.233115427 >= 0.23  [max dev from stored 2.8e-16]
PASS  E3 a = 1, box 9494 (stored bound 0.233644813): recomputed smin 0.269749181, E1 0.028557, R2 0.007547, bound 0.233644813 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 12337 (stored bound 0.234742738): recomputed smin 0.263770236, E1 0.024259, R2 0.004767, bound 0.234742738 >= 0.23  [max dev from stored 2.5e-16]
PASS  E3 a = 1, box 47931 (stored bound 0.232502856): recomputed smin 0.243297851, E1 0.009942, R2 0.000852, bound 0.232502856 >= 0.23  [max dev from stored 8.3e-17]
PASS  E3 a = 1, box 7602 (stored bound 0.237817724): recomputed smin 0.274255800, E1 0.028936, R2 0.007501, bound 0.237817724 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 28140 (stored bound 0.231183173): recomputed smin 0.250773523, E1 0.017126, R2 0.002464, bound 0.231183173 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 4914 (stored bound 0.232661005): recomputed smin 0.277117953, E1 0.034014, R2 0.010442, bound 0.232661005 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 11265 (stored bound 0.234572076): recomputed smin 0.270445156, E1 0.028318, R2 0.007555, bound 0.234572076 >= 0.23  [max dev from stored 2.6e-18]
PASS  E3 a = 1, box 56838 (stored bound 0.231102406): recomputed smin 0.240269378, E1 0.008567, R2 0.000599, bound 0.231102406 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 54810 (stored bound 0.231043032): recomputed smin 0.240223842, E1 0.008580, R2 0.000600, bound 0.231043032 >= 0.23  [max dev from stored 2.8e-17]
PASS  E3 a = 1, box 9156 (stored bound 0.237049286): recomputed smin 0.273034184, E1 0.028532, R2 0.007452, bound 0.237049286 >= 0.23  [max dev from stored 3.3e-16]
PASS  E3 a = 1, box 31544 (stored bound 0.233815419): recomputed smin 0.249983739, E1 0.014376, R2 0.001791, bound 0.233815419 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 11889 (stored bound 0.237148692): recomputed smin 0.265922814, E1 0.024021, R2 0.004752, bound 0.237148692 >= 0.23  [max dev from stored 5.6e-17]
PASS  E3 a = 1, box 55642 (stored bound 0.231128900): recomputed smin 0.240298073, E1 0.008568, R2 0.000600, bound 0.231128900 >= 0.23  [max dev from stored 1.4e-16]
PASS  E3 a = 1, box 7747 (stored bound 0.234981627): recomputed smin 0.271261719, E1 0.028764, R2 0.007515, bound 0.234981627 >= 0.23  [max dev from stored 1.7e-16]
PASS  E3 a = 1, box 16226 (stored bound 0.233343255): recomputed smin 0.261609638, E1 0.023563, R2 0.004702, bound 0.233343255 >= 0.23  [max dev from stored 1.1e-16]
PASS  E3 a = 1, box 29260 (stored bound 0.232979204): recomputed smin 0.252422318, E1 0.016968, R2 0.002474, bound 0.232979204 >= 0.23  [max dev from stored 2.2e-16]
      a = 1: 60 boxes recomputed (the 40 with the smallest stored bound and 20 random ones); max deviation from the stored values 3.3e-16
PASS  E1 a = 1/2: the 78318 boxes partition D  [78318 boxes, finest grid 64x32x64x128 = 16777216 cells, uncovered 0]
PASS  E2 a = 1/2: window parameter and target stored as 0.5, 0.18; every stored bound >= target
PASS  E3 a = 1/2, box 53410 (stored bound 0.180000063): recomputed smin 0.194901823, E1 0.013677, R2 0.001224, bound 0.180000063 >= 0.18  [max dev from stored 2.8e-17]
PASS  E3 a = 1/2, box 36378 (stored bound 0.180000187): recomputed smin 0.197999736, E1 0.016290, R2 0.001709, bound 0.180000187 >= 0.18  [max dev from stored 5.6e-16]
PASS  E3 a = 1/2, box 38860 (stored bound 0.180000313): recomputed smin 0.197580286, E1 0.015872, R2 0.001707, bound 0.180000313 >= 0.18  [max dev from stored 5.6e-16]
PASS  E3 a = 1/2, box 39071 (stored bound 0.180000348): recomputed smin 0.197750647, E1 0.016042, R2 0.001708, bound 0.180000348 >= 0.18  [max dev from stored 3.1e-16]
PASS  E3 a = 1/2, box 38054 (stored bound 0.180000399): recomputed smin 0.197910320, E1 0.016201, R2 0.001708, bound 0.180000399 >= 0.18  [max dev from stored 2.8e-16]
PASS  E3 a = 1/2, box 33864 (stored bound 0.180000451): recomputed smin 0.198266113, E1 0.016552, R2 0.001712, bound 0.180000451 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 11225 (stored bound 0.180000491): recomputed smin 0.213791133, E1 0.028753, R2 0.005037, bound 0.180000491 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 21598 (stored bound 0.180000509): recomputed smin 0.203261107, E1 0.020899, R2 0.002360, bound 0.180000509 >= 0.18  [max dev from stored 2.2e-16]
PASS  E3 a = 1/2, box 34439 (stored bound 0.180000553): recomputed smin 0.197665887, E1 0.015956, R2 0.001709, bound 0.180000553 >= 0.18  [max dev from stored 2.8e-16]
PASS  E3 a = 1/2, box 40850 (stored bound 0.180000589): recomputed smin 0.197751368, E1 0.016043, R2 0.001707, bound 0.180000589 >= 0.18  [max dev from stored 5.6e-16]
PASS  E3 a = 1/2, box 45471 (stored bound 0.180000645): recomputed smin 0.197756958, E1 0.016045, R2 0.001710, bound 0.180000645 >= 0.18  [max dev from stored 1.4e-16]
PASS  E3 a = 1/2, box 44555 (stored bound 0.180000651): recomputed smin 0.197846371, E1 0.016134, R2 0.001711, bound 0.180000651 >= 0.18  [max dev from stored 2.8e-17]
PASS  E3 a = 1/2, box 25882 (stored bound 0.180000696): recomputed smin 0.202900944, E1 0.020545, R2 0.002355, bound 0.180000696 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 49750 (stored bound 0.180000825): recomputed smin 0.198708270, E1 0.016990, R2 0.001717, bound 0.180000825 >= 0.18  [max dev from stored 2.5e-16]
PASS  E3 a = 1/2, box 22859 (stored bound 0.180000886): recomputed smin 0.203409173, E1 0.021047, R2 0.002360, bound 0.180000886 >= 0.18  [max dev from stored 3.6e-16]
PASS  E3 a = 1/2, box 65562 (stored bound 0.180000939): recomputed smin 0.194995355, E1 0.013768, R2 0.001225, bound 0.180000939 >= 0.18  [max dev from stored 4.2e-16]
PASS  E3 a = 1/2, box 46955 (stored bound 0.180000940): recomputed smin 0.198573737, E1 0.016851, R2 0.001721, bound 0.180000940 >= 0.18  [max dev from stored 2.2e-16]
PASS  E3 a = 1/2, box 38806 (stored bound 0.180001017): recomputed smin 0.197755626, E1 0.016046, R2 0.001707, bound 0.180001017 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 15358 (stored bound 0.180001022): recomputed smin 0.207002602, E1 0.023921, R2 0.003080, bound 0.180001022 >= 0.18  [max dev from stored 2.8e-17]
PASS  E3 a = 1/2, box 35466 (stored bound 0.180001036): recomputed smin 0.197871057, E1 0.016160, R2 0.001709, bound 0.180001036 >= 0.18  [max dev from stored 1.9e-16]
PASS  E3 a = 1/2, box 38058 (stored bound 0.180001218): recomputed smin 0.197822559, E1 0.016113, R2 0.001708, bound 0.180001218 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 38476 (stored bound 0.180001401): recomputed smin 0.198301117, E1 0.016588, R2 0.001711, bound 0.180001401 >= 0.18  [max dev from stored 3.9e-16]
PASS  E3 a = 1/2, box 14288 (stored bound 0.180001411): recomputed smin 0.210180188, E1 0.026063, R2 0.004115, bound 0.180001411 >= 0.18  [max dev from stored 2.8e-16]
PASS  E3 a = 1/2, box 9657 (stored bound 0.180001443): recomputed smin 0.221634004, E1 0.034484, R2 0.007148, bound 0.180001443 >= 0.18  [max dev from stored 2.5e-16]
PASS  E3 a = 1/2, box 54604 (stored bound 0.180001535): recomputed smin 0.194703857, E1 0.013480, R2 0.001222, bound 0.180001535 >= 0.18  [max dev from stored 1.4e-16]
PASS  E3 a = 1/2, box 4513 (stored bound 0.180001592): recomputed smin 0.228339673, E1 0.038577, R2 0.009760, bound 0.180001592 >= 0.18  [max dev from stored 6.9e-18]
PASS  E3 a = 1/2, box 23694 (stored bound 0.180001623): recomputed smin 0.203016809, E1 0.020660, R2 0.002354, bound 0.180001623 >= 0.18  [max dev from stored 3.3e-16]
PASS  E3 a = 1/2, box 32409 (stored bound 0.180001641): recomputed smin 0.197653256, E1 0.015942, R2 0.001709, bound 0.180001641 >= 0.18  [max dev from stored 1.1e-16]
PASS  E3 a = 1/2, box 15787 (stored bound 0.180001688): recomputed smin 0.206729194, E1 0.023655, R2 0.003072, bound 0.180001688 >= 0.18  [max dev from stored 3.3e-16]
PASS  E3 a = 1/2, box 24422 (stored bound 0.180001699): recomputed smin 0.203187135, E1 0.020828, R2 0.002357, bound 0.180001699 >= 0.18  [max dev from stored 2.5e-16]
PASS  E3 a = 1/2, box 42283 (stored bound 0.180001912): recomputed smin 0.197912969, E1 0.016201, R2 0.001709, bound 0.180001912 >= 0.18  [max dev from stored 1.7e-16]
PASS  E3 a = 1/2, box 58506 (stored bound 0.180001963): recomputed smin 0.194821072, E1 0.013596, R2 0.001222, bound 0.180001963 >= 0.18  [max dev from stored 2.8e-17]
PASS  E3 a = 1/2, box 40147 (stored bound 0.180002189): recomputed smin 0.197924824, E1 0.016213, R2 0.001708, bound 0.180002189 >= 0.18  [max dev from stored 1.1e-16]
PASS  E3 a = 1/2, box 56706 (stored bound 0.180002228): recomputed smin 0.194846852, E1 0.013620, R2 0.001223, bound 0.180002228 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 58517 (stored bound 0.180002319): recomputed smin 0.194821698, E1 0.013597, R2 0.001222, bound 0.180002319 >= 0.18  [max dev from stored 2.5e-16]
PASS  E3 a = 1/2, box 38388 (stored bound 0.180002422): recomputed smin 0.198096180, E1 0.016384, R2 0.001709, bound 0.180002422 >= 0.18  [max dev from stored 3.9e-16]
PASS  E3 a = 1/2, box 4534 (stored bound 0.180002503): recomputed smin 0.227422557, E1 0.037639, R2 0.009780, bound 0.180002503 >= 0.18  [max dev from stored 1.4e-16]
PASS  E3 a = 1/2, box 24810 (stored bound 0.180002657): recomputed smin 0.202597485, E1 0.020240, R2 0.002354, bound 0.180002657 >= 0.18  [max dev from stored 8.3e-17]
PASS  E3 a = 1/2, box 61046 (stored bound 0.180002772): recomputed smin 0.194719046, E1 0.013494, R2 0.001221, bound 0.180002772 >= 0.18  [max dev from stored 2.2e-16]
PASS  E3 a = 1/2, box 31545 (stored bound 0.180002990): recomputed smin 0.201327972, E1 0.018951, R2 0.002373, bound 0.180002990 >= 0.18  [max dev from stored 4.7e-16]
PASS  E3 a = 1/2, box 42445 (stored bound 0.181319127): recomputed smin 0.199125061, E1 0.016096, R2 0.001709, bound 0.181319127 >= 0.18  [max dev from stored 5.3e-16]
PASS  E3 a = 1/2, box 19772 (stored bound 0.183102986): recomputed smin 0.211298491, E1 0.024069, R2 0.004125, bound 0.183102986 >= 0.18  [max dev from stored 3.9e-16]
PASS  E3 a = 1/2, box 51750 (stored bound 0.180805356): recomputed smin 0.195513773, E1 0.013484, R2 0.001224, bound 0.180805356 >= 0.18  [max dev from stored 1.4e-16]
PASS  E3 a = 1/2, box 6328 (stored bound 0.193417278): recomputed smin 0.232584056, E1 0.032076, R2 0.007090, bound 0.193417278 >= 0.18  [max dev from stored 1.1e-16]
PASS  E3 a = 1/2, box 9494 (stored bound 0.185509347): recomputed smin 0.227145063, E1 0.034515, R2 0.007120, bound 0.185509347 >= 0.18  [max dev from stored 1.4e-16]
PASS  E3 a = 1/2, box 70239 (stored bound 0.182943692): recomputed smin 0.197761293, E1 0.013592, R2 0.001225, bound 0.182943692 >= 0.18  [max dev from stored 1.7e-16]
PASS  E3 a = 1/2, box 12337 (stored bound 0.181782580): recomputed smin 0.214700325, E1 0.027885, R2 0.005031, bound 0.181782580 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 47931 (stored bound 0.185440346): recomputed smin 0.203794843, E1 0.016639, R2 0.001715, bound 0.185440346 >= 0.18  [max dev from stored 3.6e-16]
PASS  E3 a = 1/2, box 76387 (stored bound 0.182239516): recomputed smin 0.194928464, E1 0.011929, R2 0.000758, bound 0.182239516 >= 0.18  [max dev from stored 2.8e-17]
PASS  E3 a = 1/2, box 7602 (stored bound 0.181153443): recomputed smin 0.219859947, E1 0.031628, R2 0.007078, bound 0.181153443 >= 0.18  [max dev from stored 6.1e-16]
PASS  E3 a = 1/2, box 66510 (stored bound 0.181239809): recomputed smin 0.196098353, E1 0.013634, R2 0.001224, bound 0.181239809 >= 0.18  [max dev from stored 1.7e-18]
PASS  E3 a = 1/2, box 28140 (stored bound 0.183807070): recomputed smin 0.205029866, E1 0.018863, R2 0.002359, bound 0.183807070 >= 0.18  [max dev from stored 3.3e-16]
PASS  E3 a = 1/2, box 4914 (stored bound 0.181512128): recomputed smin 0.233686996, E1 0.042418, R2 0.009756, bound 0.181512128 >= 0.18  [max dev from stored 1.9e-16]
PASS  E3 a = 1/2, box 11265 (stored bound 0.181388608): recomputed smin 0.214061924, E1 0.027648, R2 0.005025, bound 0.181388608 >= 0.18  [max dev from stored 3.6e-16]
PASS  E3 a = 1/2, box 56838 (stored bound 0.180192475): recomputed smin 0.194926330, E1 0.013512, R2 0.001221, bound 0.180192475 >= 0.18  [max dev from stored 8.3e-17]
PASS  E3 a = 1/2, box 54810 (stored bound 0.180824085): recomputed smin 0.195552138, E1 0.013505, R2 0.001222, bound 0.180824085 >= 0.18  [max dev from stored 1.9e-16]
PASS  E3 a = 1/2, box 9156 (stored bound 0.190181313): recomputed smin 0.230451440, E1 0.033161, R2 0.007108, bound 0.190181313 >= 0.18  [max dev from stored 2.2e-16]
PASS  E3 a = 1/2, box 31544 (stored bound 0.180118439): recomputed smin 0.201400862, E1 0.018910, R2 0.002372, bound 0.180118439 >= 0.18  [max dev from stored 5.6e-17]
PASS  E3 a = 1/2, box 11889 (stored bound 0.183915469): recomputed smin 0.216351374, E1 0.027411, R2 0.005024, bound 0.183915469 >= 0.18  [max dev from stored 8.3e-17]
PASS  E3 a = 1/2, box 72226 (stored bound 0.182549563): recomputed smin 0.197350413, E1 0.013572, R2 0.001228, bound 0.182549563 >= 0.18  [max dev from stored 2.8e-17]
      a = 1/2: 60 boxes recomputed (the 40 with the smallest stored bound and 20 random ones); max deviation from the stored values 6.1e-16
TOTAL failures: 0   (12 s)
