file k4_data/s11_254_256.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
  216 boxes; rejected: {'a3- = 0': 216, 'a1- - 1/20': 201}; 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': 20, 't0*1.1': 19, 's3=-1': 30, 'K0 broken': 30, 't2 -> -t2': 30}
  rejection reasons: {'t0*0.9': ['fails (K1)', 'fails (K3 prefix 2)', 'fails (K4)'], 't0*1.1': ['fails (K2)', '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
  no vertex-decoupled cells in this file
== 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 4.3042e-03; certified pass up to 4.3018e-03, fails from 4.3042e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.8392e-03; certified pass up to 3.8379e-03, fails from 3.8403e-03; ratio 1.000
   cell10f_3 w1=patch float margin 4.1381e-03; certified pass up to 4.1357e-03, fails from 4.1382e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.0977e-03; certified pass up to 2.0972e-03, fails from 2.0996e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.9178e-03; certified pass up to 3.9160e-03, fails from 3.9185e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.9140e-03; certified pass up to 3.9136e-03, fails from 3.9160e-03; ratio 1.000
   cell10f_3 w1=patch float margin 4.0394e-03; certified pass up to 4.0381e-03, fails from 4.0405e-03; ratio 1.000
   cell10f   w1=box   float margin 1.5454e-03; certified pass up to 1.5430e-03, fails from 1.5454e-03; ratio 0.998
   cell10f_3 w1=box   float margin 2.7840e-03; certified pass up to 2.7832e-03, fails from 2.7856e-03; ratio 1.000
   cell10f_3 w1=patch float margin 4.1619e-03; certified pass up to 4.1602e-03, fails from 4.1626e-03; ratio 1.000
   cell10f_3 w1=patch float margin 4.2723e-03; certified pass up to 4.2700e-03, fails from 4.2725e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.7201e-03; certified pass up to 2.7197e-03, fails from 2.7222e-03; ratio 1.000
  soundness (certified threshold <= float margin): True
  X: PASS
summary {'T': True, 'N': True, 'K': True, 'D': True, 'X': True}; 131 s
ALL NEGATIVE TESTS BEHAVE

real	2m13.101s
user	1m54.398s
sys	0m0.044s
