semantic test of the MAIN-6 data (56 files, 2808 + 1059 boxes): 40800 (alpha, u) samples (40000 random, 800 on four extremisers for u across [U_LO, U_HI]); 7s
claims by the step of the proof that makes them: {'L0 TC+': 2295, 'L0 TC-': 247, 'L0 cut': 29, 'L1 A4': 1291, 'L1 TC+': 385, 'L1 TC-': 15, 'L1 TCS A4': 46, 'L1 TCS cut': 15, 'L1 cut': 352, 'L2 A5': 1246, 'L2 TC+': 177, 'L2 TC-': 3, 'L2 TCS A5': 1029, 'L2 TCS cut': 62, 'L2 cut': 2, 'L3 TCS A6': 807, 'lpv': 22944, 'nobox': 9854, 'two': 1}
no claim (near-sphere test outside [q6, q5], or box file not yet delivered; gaps would be listed here): {'no box (file not delivered)': 9854, 'A6 outside [q6,q5]': 373, 'A4 outside [q6,q5]': 407, 'A5 outside [q6,q5]': 794}
smallest relative slack (T - E|L|)/T per step: {'L0 TC+': '4.903e-03', 'L0 TC-': '4.973e-02', 'L0 cut': '2.940e-02', 'L1 A4': '4.685e-08', 'L1 TC+': '2.143e-03', 'L1 TC-': '7.944e-02', 'L1 TCS A4': '1.947e-03', 'L1 TCS cut': '1.730e-02', 'L1 cut': '1.345e-02', 'L2 A5': '-5.046e-16', 'L2 TC+': '3.371e-03', 'L2 TC-': '6.349e-02', 'L2 TCS A5': '-5.048e-16', 'L2 TCS cut': '2.020e-02', 'L2 cut': '3.404e-02', 'L3 TCS A6': '6.252e-09', 'lpv': '6.625e-03', 'two': '4.491e-01'}
where the smallest slack of each near-sphere step occurs (u - u5, u6 - u, sorted |alpha_i| > 1e-3):
   L1 A4: slack 4.685e-08, u - u5 = 3.042e-07, u6 - u = 3.262e-01, |alpha| = [0.500174 0.500019 0.49991  0.499896]
   L1 TCS A4: slack 1.947e-03, u - u5 = 4.375e-05, u6 - u = 3.261e-01, |alpha| = [0.528377 0.527286 0.487027 0.453423]
   L2 A5: slack -5.046e-16, u - u5 = 5.729e-02, u6 - u = 2.689e-01, |alpha| = [0.447214 0.447214 0.447214 0.447214 0.447214]
   L2 TCS A5: slack -5.048e-16, u - u5 = 1.138e-02, u6 - u = 3.148e-01, |alpha| = [0.447214 0.447214 0.447214 0.447214 0.447214]
   L3 TCS A6: slack 6.252e-09, u - u5 = 3.262e-01, u6 - u = 3.962e-08, |alpha| = [0.408311 0.408261 0.408255 0.408254 0.408217 0.408192]
violations: 0
RESULT: PASS (9854 samples fell in slabs whose files are not yet delivered)
EXIT=0
