[0] Lemma 1 vs sympy differentiation of p*f (6 random p, deg <= 6, n <= 14): PASS
[1] Thm A step 4, hard data, J=150, n_J=2890, 915 non-zero a_m, max M/delta = 9.98e+11: n a_(n-1) in {0} u {|w|>=2}: PASS
    Remark A', p = c z^3 with |c| = 1: |s_n| >= 2|c| at all non-zero s_n: PASS
    Remark A', p = c z^1 with |c| = 0.001: |s_n| >= 2|c| at all non-zero s_n: PASS
    Remark A', p = c z^12 with |c| = 1: |s_n| >= 2|c| at all non-zero s_n: PASS
    Remark A', p = c z^7 with |c| = 0.3333: |s_n| >= 2|c| at all non-zero s_n: PASS
[2] Thm B Claim, hard data, layout B-min (B1 + L1 only, B2 not imposed), J=130, n_J=2.036e+15, block degrees 0..12 (mean 4.93), max M/delta = 2.4e+13
  [z] d=1 j0=6 n_*=300017: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 300 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^2] d=2 j0=6 n_*=300017: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 9.001e+07 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^5] d=5 j0=6 n_*=300017: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.431e+24 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^12] d=12 j0=12 n_*=414720101: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.589e+103 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1+z] d=1 j0=8 n_*=414720000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.147e+05 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1/5+z] d=1 j0=32 n_*=205765401676: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.058e+08 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z+z^2] d=2 j0=8 n_*=414720000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.72e+14 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1-z+z^2] d=2 j0=10 n_*=414720049: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.072e+13 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(3+4i)/5+z^3] d=3 j0=8 n_*=414720000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.061e+10 >= S+2: True; viol. below n_*: 2 (last zone 1)
  [1+z^9 (sparse)] d=9 j0=9 n_*=414720028: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 900 >= S+2: True; viol. below n_*: 16 (last zone 8)
  [1+z+...+z^6] d=6 j0=18 n_*=10810800188: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.031e+28 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(z-1)^2] d=2 j0=12 n_*=414720101: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.096e+17 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(z-1/2)^2] d=2 j0=34 n_*=205765401814: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.234e+19 >= S+2: True; viol. below n_*: 0 (last zone None)
  [i+(1+i)z^2-z^4] d=4 j0=12 n_*=414720101: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.565e+15 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [unit-modulus quartic] d=4 j0=14 n_*=10810800039: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.185e+23 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1/3+2z] d=1 j0=26 n_*=10810800582: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.115e+08 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1+(i/2)z+z^5/4] d=5 j0=30 n_*=10810800818: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 8.86e+47 >= S+2: True; viol. below n_*: 0 (last zone None)
  [all 1/10, d=6] d=6 j0=54 n_*=73287244800346: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.549e+79 >= S+2: True; viol. below n_*: 0 (last zone None)
  [2+3z^10] d=10 j0=10 n_*=414720049: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 120 >= S+2: True; viol. below n_*: 12 (last zone 9)
  [100z (large coeff., j0=3)] d=1 j0=3 n_*=1181: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1223 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(60+80i)+100iz (j0=5)] d=1 j0=5 n_*=300000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.999e+04 >= S+2: True; viol. below n_*: 0 (last zone None)
  [50+100z^2 (j0=7)] d=2 j0=7 n_*=300033: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.161e+11 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [1000+1000z^3 (j0=5)] d=3 j0=5 n_*=300000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.074e+07 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #0 (d=7)] d=7 j0=47 n_*=205765402931: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.502e+76 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #1 (d=6)] d=6 j0=22 n_*=10810800365: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.193e+57 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #2 (d=2)] d=2 j0=9 n_*=414720028: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.045e+13 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #3 (d=4)] d=4 j0=23 n_*=10810800418: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 9.106e+36 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #4 (d=5)] d=5 j0=18 n_*=10810800188: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.031e+28 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #5 (d=5)] d=5 j0=46 n_*=205765402837: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.496e+54 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [random #6 (d=7)] d=7 j0=42 n_*=205765402465: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 7.809e+75 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #7 (d=3)] d=3 j0=26 n_*=10810800582: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 6.781e+28 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #8 (d=8)] d=8 j0=71 n_*=73287244802556: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.34e+108 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #9 (d=4)] d=4 j0=52 n_*=73287244800116: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 9.616e+51 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #10 (d=2)] d=2 j0=4 n_*=24000: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.153e+06 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #11 (d=8)] d=8 j0=35 n_*=205765401884: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 6.371e+80 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #12 (d=4)] d=4 j0=56 n_*=73287244800579: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.442e+52 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #13 (d=3)] d=3 j0=20 n_*=10810800272: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.263e+27 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #14 (d=6)] d=6 j0=74 n_*=73287244803002: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 7.747e+79 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #15 (d=3)] d=3 j0=28 n_*=10810800700: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.644e+28 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [random #16 (d=8)] d=8 j0=75 n_*=73287244803158: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.497e+108 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #17 (d=4)] d=4 j0=42 n_*=205765402465: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 8.963e+41 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #18 (d=2)] d=2 j0=6 n_*=300017: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.701e+08 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #19 (d=7)] d=7 j0=20 n_*=10810800272: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.225e+34 >= S+2: True; viol. below n_*: 0 (last zone None)
[2b] Thm B Claim, TIGHT data (all |b_jk| = 1, M = delta = 1, degrees 0..12), B-min, J=130, n_J=17946
  [z] d=1 j0=6 n_*=70: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 77 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^2] d=2 j0=6 n_*=70: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 6006 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^5] d=5 j0=6 n_*=70: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.075e+09 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^12] d=12 j0=12 n_*=213: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.366e+28 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1+z] d=1 j0=8 n_*=110: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 119 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1/5+z] d=1 j0=32 n_*=1231: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1264 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [z+z^2] d=2 j0=8 n_*=110: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.428e+04 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1-z+z^2] d=2 j0=10 n_*=167: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.186e+04 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(3+4i)/5+z^3] d=3 j0=8 n_*=110: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.728e+06 >= S+2: True; viol. below n_*: 3 (last zone 2)
  [1+z^9 (sparse)] d=9 j0=9 n_*=140: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 18 >= S+2: True; viol. below n_*: 21 (last zone 8)
  [1+z+...+z^6] d=6 j0=18 n_*=439: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 9.532e+15 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(z-1)^2] d=2 j0=12 n_*=213: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 5.085e+04 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(z-1/2)^2] d=2 j0=34 n_*=1384: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.014e+06 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [i+(1+i)z^2-z^4] d=4 j0=12 n_*=213: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.679e+09 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [unit-modulus quartic] d=4 j0=14 n_*=275: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 7.211e+09 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1/3+2z] d=1 j0=26 n_*=852: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1758 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [1+(i/2)z+z^5/4] d=5 j0=30 n_*=1094: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.545e+14 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [all 1/10, d=6] d=6 j0=54 n_*=3282: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.387e+20 >= S+2: True; viol. below n_*: 2 (last zone 1)
  [2+3z^10] d=10 j0=10 n_*=167: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 40 >= S+2: True; viol. below n_*: 0 (last zone None)
  [100z (large coeff., j0=3)] d=1 j0=3 n_*=25: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2900 >= S+2: True; viol. below n_*: 0 (last zone None)
  [(60+80i)+100iz (j0=5)] d=1 j0=5 n_*=57: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 6399 >= S+2: True; viol. below n_*: 0 (last zone None)
  [50+100z^2 (j0=7)] d=2 j0=7 n_*=92: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.01e+06 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1000+1000z^3 (j0=5)] d=3 j0=5 n_*=57: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1e+06 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #0 (d=5)] d=5 j0=17 n_*=403: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.063e+13 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #1 (d=5)] d=5 j0=24 n_*=737: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 5.209e+14 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [random #2 (d=6)] d=6 j0=18 n_*=439: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.036e+16 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #3 (d=3)] d=3 j0=24 n_*=737: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.257e+09 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #4 (d=8)] d=8 j0=60 n_*=3998: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.484e+29 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [random #5 (d=3)] d=3 j0=30 n_*=1094: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.285e+09 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #6 (d=1)] d=1 j0=18 n_*=439: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 458.3 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [random #7 (d=1)] d=1 j0=7 n_*=92: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 201.1 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #8 (d=1)] d=1 j0=6 n_*=70: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 231.8 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #9 (d=8)] d=8 j0=99 n_*=10488: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 4.751e+32 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #10 (d=7)] d=7 j0=58 n_*=3747: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.326e+25 >= S+2: True; viol. below n_*: 0 (last zone None)
  [random #11 (d=7)] d=7 j0=60 n_*=3998: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 9.124e+24 >= S+2: True; viol. below n_*: 0 (last zone None)
[3] Thm B Claim, small-coefficient p, hard data (deg <= 8), B-min, J=250
  [z/50] d=1 j0=202 n_*=391104003193: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 7.822e+06 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [7+z/7 (small leading coeff.)] d=1 j0=128 n_*=4392001531: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 6.274e+05 >= S+2: True; viol. below n_*: 1 (last zone 1)
  [1/40+z (small constant)] d=1 j0=242 n_*=391104021106: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.911e+08 >= S+2: True; viol. below n_*: 1 (last zone 1)
[4] mutation tests (violations at n >= n_* are EXPECTED here)
  [M1 ramp removed, g_j = 1/7, p = 1+z] (mutation) violations at n >= n_*: 33 (first [89, 108, 129]) -> DETECTED as expected
  [M2 flat ramp of height 1, p = 1/5+z] (mutation) violations at n >= n_*: 9 (first [1056, 1122, 1190]) -> DETECTED as expected
  [M3 (B1) dropped, g_j = (1+z)/1000, p = z] (mutation) violations at n >= n_*: 70 (first [54, 55, 70]) -> DETECTED as expected
[5] B-full (explicit formula after (B2)), moderate data, J=45, n_J=33955: (B2) exact at N_j^0 and N_j >= N_j^0 >= j-2 for all j: PASS
  [z] d=1 j0=6 n_*=1807: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 274.4 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^2] d=2 j0=6 n_*=1807: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 5.275e+05 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^5] d=5 j0=6 n_*=1807: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3.757e+15 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z^12] d=12 j0=12 n_*=3247: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 2.1e+41 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1+z] d=1 j0=8 n_*=1911: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 276.3 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1/5+z] d=1 j0=32 n_*=26880: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 3845 >= S+2: True; viol. below n_*: 0 (last zone None)
  [z+z^2] d=2 j0=8 n_*=1911: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 5.311e+05 >= S+2: True; viol. below n_*: 0 (last zone None)
  [1-z+z^2] d=2 j0=10 n_*=3090: viol. n>=n_*: 0 PASS; min|s_n| (n>=n_*, s_n!=0) = 1.519e+06 >= S+2: True; viol. below n_*: 0 (last zone None)
    exact zone-i contributions to f_B^(n_j) on |z| <= j (1 <= j <= 5, j < i <= j+6): all <= 2^-i: PASS (max of 2^i * contribution = 1.913e-04)
elapsed 16.6 s
ALL CHECKS PASSED
