(1) recurrence for W_m checked for m <= 7
(2) reversal-negation and (3) insertion of NS checked for lengths <= 7 and <= 4
(4) padding lemma checked for k <= 3, n <= 4; (5) concatenation for n, m <= 3
(6a) DP values equal brute force for n <= 6 at a in {-1,-1/2,0,2}; Q_n polynomials (coefficient lists, n=1..6):
   n=1 [2]
   n=2 [8, 2]
   n=3 [44, 24, 2]
   n=4 [288, 246, 52, 2]
   n=5 [2100, 2464, 882, 96, 2]
   n=6 [16480, 24756, 12724, 2502, 164, 2]
(6b) Q_(n+2k+2)(a) >= weight of loops inside [-k,inf)^2 checked where n+2k+2 <= 6
(7) a=0/1: max over 1<=n<=200 of Q_n(a)/G(a)^n = 0.171573
(7) a=1/1: max over 1<=n<=200 of Q_n(a)/G(a)^n = 0.125
(7) a=2/1: max over 1<=n<=200 of Q_n(a)/G(a)^n = 0.101021
ALL CHECKS PASSED
