== Lemma 2 (eventual independence) checks
  shift k=1 N=1: failing n = [0]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=1 N=4: failing n = [0, 1, 2, 3]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=1 N=7: failing n = [0, 1, 2, 3, 4, 5, 6]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=2 N=1: failing n = [0]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=2 N=4: failing n = [0, 1, 2, 3]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=2 N=7: failing n = [0, 1, 2, 3, 4, 5, 6]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=3 N=1: failing n = [0]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=3 N=4: failing n = [0, 1, 2, 3]  (Lemma 2 bound predicts exactly 0..N-1: True)
  shift k=3 N=7: failing n = [0, 1, 2, 3, 4, 5, 6]  (Lemma 2 bound predicts exactly 0..N-1: True)
  stair k=1 dimW=8: failing n = [0, 1, 2]  (finitely many, all < 40: True)
  stair k=3 dimW=8: failing n = [0, 1, 2]  (finitely many, all < 40: True)
  laurent k=1 dimW=8: failing n = [0, 1, 2]  (finitely many, all < 40: True)
  laurent k=3 dimW=8: failing n = [0, 1, 2, 3]  (finitely many, all < 40: True)
  NEGATIVE CONTROL torsion eig: fails for all n in 0..60: True
  NEGATIVE CONTROL torsion rot: fails for all n in 0..60: True
== Theorem B construction, example: shift
   50 requirements, dim W = 101, last n = 99, rejected times = 49, M = 102
   primal (T^n S c)_(<k) == sum_l Lam[i][l] c_(j_l): 250 checks, all equal: True
   targeted 3-tuple hits (exact): 18/18
   Theorem C on this omega instance: S'a=S0a True, S'e=T S0 a True, S'u=S0 w+phi(u)T S0 a True
== Theorem B construction, example: stair (non-constant coeffs)
   50 requirements, dim W = 97, last n = 66, rejected times = 16, M = 133
   primal (T^n S c)_(<k) == sum_l Lam[i][l] c_(j_l): 250 checks, all equal: True
   targeted 3-tuple hits (exact): 18/18
   Theorem C on this omega instance: S'a=S0a True, S'e=T S0 a True, S'u=S0 w+phi(u)T S0 a True
== Theorem B construction, example: laurent K[t,1/t]
   50 requirements, dim W = 95, last n = 95, rejected times = 45, M = 191
   primal (T^n S c)_(<k) == sum_l Lam[i][l] c_(j_l): 250 checks, all equal: True
   targeted 3-tuple hits (exact): 18/18
   Theorem C on this omega instance: S'a=S0a True, S'e=T S0 a True, S'u=S0 w+phi(u)T S0 a True
INDEPENDENT CHECK: ALL PASSED
