check_note.py -- OWR-720-011 (Python 3.13, standard library only)
[1] The constants beta_b = binom(2b,b)/4^b (Lemmas 3.1, 3.2), exact rational arithmetic, b <= 2000
   PASS beta_0 = 1, beta_1 = 1/2, beta_2 = 3/8
   PASS beta_{b+1} = beta_b (2b+1)/(2b+2)
   PASS beta_b - beta_{b+1} = beta_b/(2b+2) > 0
   PASS (beta_{b+1}-beta_{b+2}) = (beta_b-beta_{b+1}) (2b+1)/(2b+4)  (differences strictly decreasing)
   PASS sum_{a=0}^n beta_a beta_{n-a} = 1 for n <= 300  ((1-x)^{-1/2} squared is (1-x)^{-1})

[2] Theorems 1.1(b) and 1.2 as identities of formal power series in eps (exact, up to order eps^12)
   PASS bilateral part: <U psi, psi_{i,0}> = u_i = gamma_i + eps gamma_{i-1}, |i| <= 14
   PASS sum_i u_i^2 = 1 (|g| = 1) up to order eps^12
   PASS leading coefficient of u_i has sign (-1)^{i+1} (i >= 1), (-1)^i (i <= 0), |i| < 12
      u_-1 = -1/2 eps + 3/16 eps^3 + 5/128 eps^5 + ...   (u_-1 = -Lambda_1)
   PASS b = 0 term of Lambda_1 is eps(beta_1 - eps^2 beta_2) = eps(1/2 - 3eps^2/8)
   PASS chain: (U e_nu)_n = u_{n-nu} - u_{n+nu+2}, nu <= 4, n <= nu+14
   PASS chain: <(A*A)^{-1/2} e_nu, e_n> = gamma_{n-nu} - gamma_{n+nu+2}, nu <= 3
   PASS chain: <U e_nu, U e_mu> = delta_{nu,mu} for nu, mu <= 3 (U isometric on the chain)
   PASS index pairs: U psi_{j,k} = sum_q (u_q - u_{q+2nu(k)+2}) psi_{j+q, 2^q k} (k != 0), sum_q u_q psi_{j+q,0} (k = 0); support in the summand of psi_{j,k}; 10 pairs
   PASS (AA*)^{-1/2} A psi_{j,k} = A (A*A)^{-1/2} psi_{j,k} (Theorem 1.1(b)), 7 pairs
   PASS canonical dual: S^{-1} eta_{j,k} = sum_{n=0}^{nu(k)} (-eps)^n psi_{j-n,k/2^n} (k != 0), sum_n (-eps)^n psi_{j-n,0} (k = 0) (Remark 7.1)

[3] Lemma 3.2 (signs) and Theorem 1.2 (signs of the coefficients) on a grid of eps; decimal arithmetic with 100 digits,
    series truncated with remainder <= 1e-90 (the smallest compared quantity is printed below)
      eps = 0.01   indices k, |i| <= 27,  23 series terms:  367 sign checks
      eps = 0.05   indices k, |i| <= 42,  35 series terms:  747 sign checks
      eps = 0.1    indices k, |i| <= 55,  46 series terms: 1166 sign checks
      eps = 0.2    indices k, |i| <= 60,  65 series terms: 1368 sign checks
      eps = 0.25   indices k, |i| <= 60,  75 series terms: 1368 sign checks
      eps = 0.3    indices k, |i| <= 60,  87 series terms: 1368 sign checks
      eps = 0.4    indices k, |i| <= 60, 114 series terms: 1368 sign checks
      eps = 0.5    indices k, |i| <= 60, 150 series terms: 1368 sign checks
      eps = 0.6    indices k, |i| <= 60, 204 series terms: 1368 sign checks
      eps = 0.7    indices k, |i| <= 60, 292 series terms: 1368 sign checks
      eps = 0.75   indices k, |i| <= 60, 362 series terms: 1368 sign checks
      eps = 0.8    indices k, |i| <= 60, 467 series terms: 1368 sign checks
      eps = 0.9    indices k, |i| <= 60, 992 series terms: 1368 sign checks
      eps = 0.95   indices k, |i| <= 60, 2043 series terms: 1368 sign checks
      eps = 0.99   indices k, |i| <= 60, 10505 series terms: 1368 sign checks
   PASS all sign statements of Lemma 3.2 and Theorem 1.2 on the grid (18696 checks)
   PASS every compared quantity exceeds 1e-80 in absolute value (errors of the evaluation <= 1e-89)  (smallest: 1.96e-60)

[4] Theorem 1.1(c) and Proposition 4.1: d(eps) = ||S^{-1/2} T_1 eta - T_1 S^{-1/2} eta||
      eps    d = (1-u_0^2-u_1^2)^(1/2)   direct sum (truncated)   Lambda_1 = |u_-1|   eps(1/2-3eps^2/8)   recorded (FFT)
      0.05   0.024996089777605          0.024996089777605         0.024976550280      0.024953125000      0.024996089778
      0.1    0.049968622389939          0.049968622389939         0.049812107656      0.049625000000      0.049968622390
      0.25   0.124498907138401          0.124498907138401         0.122031084237      0.119140625000      0.124498907138
      0.5    0.245637063646370          0.245637063646370         0.225185851019      0.203125000000      0.245637063646
      0.75   0.357473205045176          0.357473205045176         0.283187443918      0.216796875000      0.357473205045
      0.9    0.413269368312527          0.413269368312527         0.273453305473      0.176625000000      0.413269368313
      0.99   0.434598962561950          (not computed)            0.225997623238      0.131137875000      0.434598962562
   PASS d = (1-u_0^2-u_1^2)^(1/2) agrees with the direct sum within its truncation bound; d >= Lambda_1 >= eps(1/2-3eps^2/8) >= eps/8; agreement with the recorded FFT values to 1e-11

[5] Index bookkeeping (exact): chains (Lemma 2.1(iii)), Lemma 5.1, Proposition 5.2
   PASS every (j,k), k != 0, lies on exactly one chain C_{i,m}; B moves it one step along the chain, B* one step back, and B* kills exactly the chain starts (|j| <= 8, |k| <= 64)
   PASS Lemma 5.1: T_t psi_{i,0} = psi_{i,2^i t} is the basis vector number i+a of the chain C_{-a,b} for i >= -a, and 2^i t is not an integer for i < -a (10400 cases)
   PASS Proposition 5.2: the case analysis of the proof (k0 = 0; s = 0; nu(s) <, =, > nu(k0)) gives 'T_k e in E iff k0 != 0 and j0 + nu(k) > nu(k0)', with image U psi_{j0, k0 + 2^j0 k} (84240 cases, 38400 in E)

[6] Remark 5.3: dist(T_1 U psi_{J,0}, E) <= ||T_1 U psi_{J,0} - U psi_{J,2^J}|| = (sum_{i<-J} u_i^2 + sum_{i>=J+2} u_i^2)^(1/2) <= sqrt2 eps^{J+1} (1-eps^2)^{-3/2}
      eps = 0.1  J = 0..8: 5.00e-02 3.75e-03 3.12e-04 2.73e-05 2.46e-06 2.26e-07 2.09e-08 1.96e-09 1.85e-10
      eps = 0.5  J = 0..8: 2.46e-01 9.22e-02 3.85e-02 1.69e-02 7.61e-03 3.49e-03 1.62e-03 7.61e-04 3.60e-04
      eps = 0.9  J = 0..8: 4.13e-01 2.77e-01 2.09e-01 1.65e-01 1.35e-01 1.12e-01 9.38e-02 7.94e-02 6.78e-02
   PASS the distances are below the bound for every J printed (they tend to 0 geometrically)

[7] Proposition 1.3 (Shannon wavelet)
   PASS beta_i >= 1/(2 sqrt i) for 1 <= i <= 3000 (exact: 4 i binom(2i,i)^2 >= 16^i); beta_{i+1}^2 (i+1) / (beta_i^2 i) = (2i+1)^2/(4i(i+1)) > 1
   PASS Lambda_i >= (1-eps^2) eps^i beta_i on the grid of [3]
      eps = 0.3  2eps^2 = 0.18   partial sums of 1 + sum (2^i-1) Lambda_i^2 at i = 20, 40, 60: 1.0246775885  1.0246775885  1.0246775885
      eps = 0.5  2eps^2 = 0.50   partial sums of 1 + sum (2^i-1) Lambda_i^2 at i = 20, 40, 60: 1.0857817909  1.0857818012  1.0857818012
      eps = 0.7  2eps^2 = 0.98   partial sums of 1 + sum (2^i-1) Lambda_i^2 at i = 20, 40, 60: 1.4196764326  1.4815936333  1.5056664627
      eps = 0.75 2eps^2 = 1.1250 partial sums of 1 + sum (2^i-1) Lambda_i^2 at i = 20, 40, 60: 2.1386721729  5.9798731251  30.9856872050
      eps = 0.9  2eps^2 = 1.62   partial sums of 1 + sum (2^i-1) Lambda_i^2 at i = 20, 40, 60: 149.4196672846  1038108.2276752298  10402649001.5002212524
      j = 0: sum_{|k| <= 400000} |<psi, T_{k/2^j} psi>|^2 = 1.0000000  (2^j = 1; omitted terms <= 2.0e-06)
      j = 1: sum_{|k| <= 400000} |<psi, T_{k/2^j} psi>|^2 = 1.9999990  (2^j = 2; omitted terms <= 8.1e-06)
      j = 2: sum_{|k| <= 400000} |<psi, T_{k/2^j} psi>|^2 = 3.9999919  (2^j = 4; omitted terms <= 3.2e-05)
      j = 3: sum_{|k| <= 400000} |<psi, T_{k/2^j} psi>|^2 = 7.9999676  (2^j = 8; omitted terms <= 1.3e-04)
   PASS sum_k |<psi, T_{k/2^j} psi>|^2 = 2^j for j = 0..3 within the tail bound 8*4^j/(pi^2 K)

ALL CHECKS PASSED
