file k4_data/s13_2620_2640.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
  19 boxes; rejected: {'a3- = 0': 19, 'a1- - 1/20': 19}; reasons ['K b+^2', 'atom']
  (a3- = 0 must be rejected for all): True
  N: PASS
== K: corrupted comparison boxes
  30 sampled boxes (30 of kind comp3, all 0 of kind comp8); rejected: {'t0*0.9': 26, 't0*1.1': 26, 's3=-1': 30, 'K0 broken': 30, 't2 -> -t2': 30}
  rejection reasons: {'t0*0.9': ['fails (K4)'], 't0*1.1': ['fails (K1)', 'fails (K2)'], '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=['1/2', '1", "W1 fails at a=['1/2', '4", "W1 fails at a=['1/2', '7", "W1 fails at a=['11/20', ", "W1 fails at a=['17/20', ", "W1 fails at a=['19/32', ", "W1 fails at a=['19/40', ", "W1 fails at a=['21/40', ", "W1 fails at a=['23/40', ", "W1 fails at a=['3/5', '8", "W1 fails at a=['43/80', ", "W1 fails at a=['47/80', ", "W1 fails at a=['49/80', ", "W1 fails at a=['5/8', '4", "W1 fails at a=['7/10', '", "W1 fails at a=['9/16', '"], '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 3.6275e-03; certified pass up to 3.6255e-03, fails from 3.6279e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.6006e-03; certified pass up to 3.5986e-03, fails from 3.6011e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.0482e-03; certified pass up to 3.0469e-03, fails from 3.0493e-03; ratio 1.000
   cell10f_3 w1=patch float margin 2.6242e-03; certified pass up to 2.6221e-03, fails from 2.6245e-03; ratio 0.999
   cell10f_3 w1=patch float margin 2.4041e-03; certified pass up to 2.4023e-03, fails from 2.4048e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.5073e-03; certified pass up to 3.5059e-03, fails from 3.5083e-03; ratio 1.000
   cell10f_3 w1=patch float margin 2.8466e-03; certified pass up to 2.8442e-03, fails from 2.8467e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.7658e-03; certified pass up to 3.7646e-03, fails from 3.7671e-03; ratio 1.000
   cell10f_3 w1=patch float margin 2.7302e-03; certified pass up to 2.7295e-03, fails from 2.7319e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.7351e-03; certified pass up to 3.7329e-03, fails from 3.7354e-03; ratio 0.999
   cell10f_3 w1=patch float margin 3.8237e-03; certified pass up to 3.8232e-03, fails from 3.8257e-03; ratio 1.000
   cell10f_3 w1=patch float margin 3.0364e-03; certified pass up to 3.0347e-03, fails from 3.0371e-03; ratio 0.999
  soundness (certified threshold <= float margin): True
  X: PASS
summary {'T': True, 'N': True, 'K': True, 'D': True, 'X': True}; 130 s
ALL NEGATIVE TESTS BEHAVE

real	2m11.691s
user	2m12.395s
sys	0m0.064s
