check_note.py (OWR-12872-018); Python 3.9.6
PASS A1 Lemma 2.1: W_{m+1} = S W_m + (a-1) T W_{m-1}, all words m <= 7, 6 exact points (also a = -3/4: the recurrence does not need a >= 0)
PASS A2 S^2 - 4T >= 8 on a grid of 1421 exact points (x, y) > 0
PASS A3 closed form W_m = sum lambda_+^k lambda_-^(m-k), lambda_+ >= |lambda_-|, 0 <= W_m <= (m+1) Lambda^m (floats, m <= 40, 25 points, a in {0,0.3,1,2.5,10})
PASS A4 W_m(1,1) >= c_a lambda^m exactly for m <= 60 at a = 0, 1/2 (c_a = 1, in Q(sqrt 2), Q(sqrt 3)), a = 1 (W_m = 4^m) and a = 7 (c_a = 1/2, W_m = (6^(m+1)-(-2)^(m+1))/8)
   [partA done in 1.0 s]
PASS B1 Lemma 2.2: reversal-negation keeps c, negates the endpoint, is an involution (all words, m <= 7)
PASS B2 the diagonal reflection N<->E, S<->W exchanges the factors NW and ES: keeps c, swaps X and Y (all words, m <= 7)
   [partB done in 0.2 s]
PASS C1 c(w1 N S w2) = c(w1) + c(w2) for all pairs of words of length m <= 3
PASS C2 the endpoints of words of length m are the (m+1)^2 points |i|+|j| <= m, i+j = m mod 2 (enumerated for m <= 7, counted for m <= 8)
PASS C3 Lemma 2.3: N_m(P) = N_m(-P) and L_{m+1} >= sum_P N_m(P)^2 >= W_m(1,1)^2/(m+1)^2, exact, m <= 6, a in {0, 1/2, 1, 3}
   [partC done in 0.1 s]
PASS D1 Lemma 2.4: exact weight of loops of length 2n visiting x = -k-1 is at most max(1,a)(2n-1)(n+1)^2 e^{-2 delta (k+1)} Lambda_delta^{2n}; n <= 9, k <= 3, a in {0,1/2,1,3}, 8 values of delta -- largest ratio weight/bound = 0.144
PASS D2 the y-case: B^y_n(k) = B^x_n(k) as polynomials in a (n <= 9, k <= 3)
PASS D3 Lambda is the same at the four tilts (e^{+-delta},1), (1,e^{+-delta}) and equals f(2 cosh delta)
   [partD done in 0.2 s]
PASS E1 Lemma 2.5: P w F is a quadrant loop, 4k+4 letters longer, with the same c, for all loops of length <= 8 inside [-k,inf)^2, k <= 2 -- 9651 cases
   [partE done in 0.2 s]
PASS F1 Q_1..Q_5 as printed in Section 1 (2, 8+2a, 44+24a+2a^2, 288+246a+52a^2+2a^3, 2100+2464a+882a^2+96a^3+2a^4)
PASS F2 transfer matrix = brute force over all words for Q_n and L_n, n <= 4, at a = -3/4
PASS F3 Q_n(1) = C_n C_{n+1} and Q_n(-1) = sum_i binom(n,i) C_i C_{n-i} [AB, Prop. 15], n <= 30
PASS F4 L_n(1) = binom(2n,n)^2 and L_n(-1) = sum_i binom(n,i) binom(2i,i) binom(2n-2i,n-i) [AB, Prop. 20], n <= 12
PASS F5 Q_n(a) has nonnegative integer coefficients and degree <= n-1 (n <= 30)
PASS F6 Lemma 2.6: quadrant loops start with N/E and end with S/W, concatenation adds corners (half-length <= 3); Q_{m+n} >= Q_m Q_n and Q_n >= 1 exactly, m+n <= 30, a in {0,1/2,1,2}
PASS F7 Theorem 1.1: Q_n(a) <= G(a)^n exactly for n <= 30 at a = 0, 1/2, 1, 7
PASS F8 recorded data (original program, n <= 200, 7 values of a): equal to the transfer matrix of this program for n <= 30, all positive, identities at a = +-1 for n <= 200, Q_n <= G^n exactly for n <= 200 at a = 0, 1, 2 -- max_n Q_n/G^n: a=0: 0.171573, a=1: 0.125000, a=2: 0.101021
   [partF done in 0.5 s]
PASS G1 proof of Theorem 1.1: f' > 1/2 on [2, 2cosh 1], Lambda_delta <= lambda + K delta^2 on (0,1], and e^{-2 delta (k+1)} Lambda_delta^{2n} <= lambda^{2n} e^{-delta eps n} for delta = min(1, eps lambda/(2K)), k = ceil(eps n) -- a=0: K=1.8392; a=0.5: K=1.9207; a=1: K=2.0000; a=2: K=2.2247; a=5: K=2.7321; a=50: K=6.0498
PASS G2 proof of Proposition 3.1: with k = ceil(C sqrt(n log n)), delta = k lambda/(2nK), C^2 lambda/(2K) = 6: e^{-2 delta (k+1)} Lambda_delta^{2n} <= lambda^{2n} exp(-k^2 lambda/(2nK)) <= lambda^{2n} n^{-6}
   [partG done in 0.1 s]
PASS H1 exact constants: lambda(a) root of z^2-4z-2(a-1); G(0) = 6+4 sqrt2, G(1) = 16; branches 9 at a = -1/2, 8 at a = -1, 49/6 at a = -3/4; 2(1-a)^2/(-a) > lambda(a)^2 on [-1,-1/2) via (2-s)^2-(2-s^2) = 2(1-s)^2; c_a = 2/sqrt(2+2a) for a > 1
   [partH done in 0.0 s]
PASS I1 Q_n(a) = sum over quadrant excursions of total length 2n of the 6-step model (N,E,S,W of length 1; (-1,1), (1,-1) of length 2 and weight a-1), exact, n <= 10, a in {0,1/2,2,7/2,-3/4}
   [partI done in 0.0 s]
PASS J1 the dynamic programme for S_a(V,H) = brute force over all shuffles, |V|,|H| <= 4
PASS J2 [AB, (N2)]: the class of (NNNSSS, EWEWEW) has polynomial 62a^3 + 292a^2 + 390a + 180
PASS J3 the two negative class sums of Section 5 (exact, deterministic): Dyck pair (NSNSNSNNSNSS, EEEEEWEEWWEWWWEWWW) at a = -13/20 and balanced pair (SSSNSNNSNSNNNNSSNS, EEEEEEWWEWEEWWEWWWWW) at a = -2/5; at a = -1 both equal binom(i+j, i) -- S_-13/20 = -124660942032543/256000000000 ~ -486.9568; S_-2/5 = -63526557090248/1220703125 ~ -52040.9556
PASS J4 S_{-1}(V,H) = binom(i+j,i) for all pairs of Dyck paths with half-lengths i, j <= 4
   [partJ done in 0.4 s]
TOTAL failures: 0   (2.6 s)
