file k4_data/s13_2640_2660.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
  6 boxes; rejected: {'a3- = 0': 6, 'a1- - 1/20': 6}; reasons ['K b+^2', 'atom']
  (a3- = 0 must be rejected for all): True
  N: PASS
== K: corrupted comparison boxes
  51 sampled boxes (30 of kind comp3, all 21 of kind comp8); rejected: {'t0*0.9': 41, 't0*1.1': 43, 's3=-1': 51, 'K0 broken': 51, 't2 -> -t2': 51}
  rejection reasons: {'t0*0.9': ['fails (K1)', 'fails (K4)'], 't0*1.1': ['fails (K1)', '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 51; 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=['1/2', '7", "W1 fails at a=['11/20', ", "W1 fails at a=['17/32', ", "W1 fails at a=['19/32', ", "W1 fails at a=['21/40', ", "W1 fails at a=['23/40', ", "W1 fails at a=['3/5', '1", "W1 fails at a=['3/5', '7", "W1 fails at a=['39/80', ", "W1 fails at a=['41/80', ", "W1 fails at a=['43/80', ", "W1 fails at a=['5/8', '3", "W1 fails at a=['79/160',", "W1 fails at a=['83/160',", "W1 fails at a=['89/160',", "W1 fails at a=['93/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']
  (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   w1=patch float margin 1.6201e-03; certified pass up to 1.6187e-03, fails from 1.6211e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.6568e-03; certified pass up to 2.6563e-03, fails from 2.6587e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.6054e-03; certified pass up to 3.6035e-03, fails from 3.6060e-03; ratio 0.999
   cell10f   w1=patch float margin 1.9558e-03; certified pass up to 1.9531e-03, fails from 1.9556e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.5891e-03; certified pass up to 3.5889e-03, fails from 3.5913e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.5363e-03; certified pass up to 3.5352e-03, fails from 3.5376e-03; ratio 1.000
   cell10f   w1=patch float margin 1.0373e-03; certified pass up to 1.0352e-03, fails from 1.0376e-03; ratio 0.998
   cell10f_3 w1=patch float margin 2.6640e-03; certified pass up to 2.6636e-03, fails from 2.6660e-03; ratio 1.000
   cell10f   w1=box   float margin 1.1614e-03; certified pass up to 1.1597e-03, fails from 1.1621e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.5142e-03; certified pass up to 2.5122e-03, fails from 2.5146e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.6447e-03; certified pass up to 3.6426e-03, fails from 3.6450e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.6545e-03; certified pass up to 3.6523e-03, fails from 3.6548e-03; ratio 0.999
  soundness (certified threshold <= float margin): True
  X: PASS
summary {'T': True, 'N': True, 'K': True, 'D': True, 'X': True}; 124 s
ALL NEGATIVE TESTS BEHAVE

real	2m5.544s
user	2m6.216s
sys	0m0.104s
