RQ-REF3 heavy_verify.py; start 2026-10-23 01:56:55 UTC
md5 dfb3785938544196796e8a0bac22381d  heavy_verify.py
md5 e23d52dd72764e98fb579ae6dba2b85c  certs_v1_r0.jsonl
md5 ee9307ee5d40850c0e6199df6478b610  certs_v1_r1.jsonl
md5 f5fe9a23f7ddd05ff70b7217731aa1af  certs_v1_r2.jsonl
md5 6d495261e3af634ebc32ef8c7ef18c63  certs_v1_r3.jsonl
md5 3033710b0d34ca792aaa15feae577299  certs_v1_r4.jsonl
C5 lower bound used: (32/25) sqrt(2 ln 5/4) rounded down = 0.855100455470819
436 box records
box tiling: OK (436 leaves, 0 unused (nested or outside the rectangle))
verified boxes: 280 ok, 156 empty, 0 failures; 1237 cells; 5 s
worst certified bound beta + eps = 0.8548832 in box [6, 3, 6, 39] cell [2, 3, 1]
  box level d = 0: 96 certified, 134 empty
  box level d = 1: 71 certified, 12 empty
  box level d = 2: 66 certified, 6 empty
  box level d = 3: 44 certified, 3 empty
  box level d = 4: 3 certified, 1 empty
cell outcomes: {'ok': 1236, 'farkas': 1}
my bound - stored float bound: min -1.234e-09, max -2.414e-13
  bound 0.8548832  box [6, 3, 6, 39] cell (2, 3, 1)
  bound 0.8548785  box [6, 4, 6, 34] cell (0, 0, 0)
  bound 0.8548675  box [6, 2, 6, 40] cell (2, 3, 1)
  bound 0.8548619  box [7, 4, 7, 74] cell (1, 1, 0)
  bound 0.8548327  box [6, 0, 6, 40] cell (2, 3, 1)
  bound 0.8548224  box [5, 3, 5, 29] cell (1, 1, 0)
  bound 0.8548146  box [5, 4, 5, 21] cell (1, 1, 0)
  bound 0.8548036  box [5, 3, 5, 26] cell (1, 1, 0)
RESULT: ALL CHECKS PASSED
---- negative controls (each must FAIL) ----
  drop box [4,0,4,0]                                           -> rejected (good)
  move box [4,15,4,11] out of grid                             -> rejected (good)
  drop one cell of box [4, 3, 4, 10]                           -> rejected (good)
  relabel ok box [4, 2, 4, 6] as empty                         -> rejected (good)
  Farkas multipliers (0, 0) in box [7, 1, 7, 79]               -> rejected (good)
  c16 made negative in box [4, 4, 4, 5]                        -> rejected (good)
  L below tau a1 + A b1 in box [4, 2, 4, 6]                    -> rejected (good)
  phi coefficient c2 scaled by 0.97 in box [4, 3, 4, 9]        -> rejected (good)
  target C5 - 1e-4: 0 of 280 non-empty boxes fail
  target C5 - 3e-4: 9 of 280 non-empty boxes fail
  target C5 - 1e-3: 50 of 280 non-empty boxes fail
end 2026-10-23 01:57:13 UTC
