file k4_data/s12_2560_2580.json
== T: corrupted tilings
  phase-1 cell deleted: verifier result rejected
  phase-1 cell duplicated: verifier result rejected
  cell relabelled as skipped: verifier result rejected
  phase-2 cell relabelled as empty: verifier result rejected
  phase-2 box deleted: verifier result rejected
  split box with s2 = -1: verifier result rejected
  T: PASS
== N: corrupted near-sphere boxes
  63 boxes; rejected: {'a3- = 0': 63, 'a1- - 1/20': 38}; reasons ['K b+^2', 'atom']
  (a3- = 0 must be rejected for all): True
  N: PASS
== K: corrupted comparison boxes
  30 sampled boxes; rejected: {'t0*0.9': 18, 't0*1.1': 19, 's3=-1': 30, 'K0 broken': 30, 't2 -> -t2': 30}
  rejection reasons: {'t0*0.9': ['fails (K1)', 'fails (K4)'], 't0*1.1': ['fails (K1)', 'fails (K2)', 'fails (K3 prefix 1)', 'fails (K3 prefix 3)', 'fails (K4)'], 's3=-1': ['s3 != +1'], 'K0 broken': ['K0: a2 + a3 < a1 possi'], 't2 -> -t2': ['t_{D-4} <= 0']}
  (s3 = -1, broken K0 and negative leading coefficient must be rejected for all 30; the t0 scalings are expected to fail for most): True
  K: PASS
== D: corrupted vertex-decoupled cells
  30 sampled decoupled cells; rejected: {'one certificate removed': 30, 'one b moved by 1e-15': 30, 'one c0 lowered by 2^-7': 30, 'one F at the W2 threshold': 30}
  rejection reasons: {'one certificate removed': ['15 certificates for 16 p', '7 certificates for 8 poi'], 'one b moved by 1e-15': ['no certificate for the p'], 'one c0 lowered by 2^-7': ["W1 fails at a=['103/160'", "W1 fails at a=['2/5', '3", "W1 fails at a=['23/40', ", "W1 fails at a=['3/4', '9", "W1 fails at a=['3/5', '1", "W1 fails at a=['3/5', '2", "W1 fails at a=['3/5', '4", "W1 fails at a=['3/5', '7", "W1 fails at a=['31/40', ", "W1 fails at a=['39/80', ", "W1 fails at a=['41/80', ", "W1 fails at a=['43/80', ", "W1 fails at a=['47/80', ", "W1 fails at a=['49/80', ", "W1 fails at a=['5/8', '2", "W1 fails at a=['5/8', '4", "W1 fails at a=['51/80', ", "W1 fails at a=['79/160',", "W1 fails at a=['81/160',", "W1 fails at a=['83/160',", "W1 fails at a=['9/16', '", "W1 fails at a=['91/160',", "W1 fails at a=['97/160',"], 'one F at the W2 threshold': ['W2  margin 0']}
  D: PASS
== X: corrupted cells, and sharpness of the W1 check
  40 sampled cells; rejected corruptions: {'c0-1e-2 (W1)': 40, 'c0-2^-7 (W1)': 40, 'F at threshold': 40, 'F < max Phi': 40, 'box widened': 40}; rejection reasons ['W1 fails ', 'widened: W1 fails at a=', 'widened: W2 F <= Phi so', 'widened: exception Valu']
  (c0 lowered by 1e-2 and F at the threshold must be rejected for all 40: True; F/4 and the widened box are expected to fail for most cells, not necessarily all)
  sharpness: certified c0-threshold (bisection, 12 steps) vs dense float W1 margin
   cell10f_3 w1=patch float margin 2.7481e-03; certified pass up to 2.7466e-03, fails from 2.7490e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.2547e-03; certified pass up to 3.2520e-03, fails from 3.2544e-03; ratio 0.999
   cell10f   w1=patch float margin 1.1453e-03; certified pass up to 1.1450e-03, fails from 1.1475e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.4803e-03; certified pass up to 3.4790e-03, fails from 3.4814e-03; ratio 1.000
   cell10f   w1=box   float margin 1.2708e-03; certified pass up to 1.2695e-03, fails from 1.2720e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.6393e-03; certified pass up to 2.6392e-03, fails from 2.6416e-03; ratio 1.000
   cell10f_3 w1=patch float margin 2.7980e-03; certified pass up to 2.7979e-03, fails from 2.8003e-03; ratio 1.000
   cell10f_3 w1=patch float margin 2.9711e-03; certified pass up to 2.9688e-03, fails from 2.9712e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.8133e-03; certified pass up to 2.8125e-03, fails from 2.8149e-03; ratio 1.000
   cell10f_3 w1=box   float margin 2.5114e-03; certified pass up to 2.5098e-03, fails from 2.5122e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.7284e-03; certified pass up to 2.7271e-03, fails from 2.7295e-03; ratio 1.000
   cell10f   w1=patch float margin 2.1108e-03; certified pass up to 2.1094e-03, fails from 2.1118e-03; ratio 0.999
  soundness (certified threshold <= float margin): True
  X: PASS
summary {'T': True, 'N': True, 'K': True, 'D': True, 'X': True}; 112 s
ALL NEGATIVE TESTS BEHAVE

real	1m52.855s
user	1m53.411s
sys	0m0.068s
