PASS  Fricke identity and Lemma 3.1 (trace recursion, k = 1..12)  [2850 random pairs over 19 fields, q <= 1009; mismatches: 0]
PASS  Lemma 3.3 (every (s,t) with s^2 != 4 is (tr y, tr[x,y])), construction of the proof  [5648 pairs (s,t) over 16 fields q <= 32; failures: 0]
PASS  exact Engel depth of PSL(2,4)  [|PSL|=60, 5 classes, mu(PSL)=3, mu(SL)=3, minimal law [x,_3 y]=[x,_63 y] (Brandl-Nikolova table: r=3, s=63)]
PASS  exact Engel depth of PSL(2,5)  [|PSL|=60, 5 classes, mu(PSL)=3, mu(SL)=3, minimal law [x,_3 y]=[x,_63 y] (PSL(2,5) = PSL(2,4) = A_5; Nikolova 1984: [x,_3 y]=[x,_63 y])]
PASS  exact Engel depth of PSL(2,7)  [|PSL|=168, 6 classes, mu(PSL)=4, mu(SL)=4, minimal law [x,_4 y]=[x,_172 y] (Brandl-Nikolova table: r=4, s=172)]
PASS  exact Engel depth of PSL(2,8)  [|PSL|=504, 9 classes, mu(PSL)=3, mu(SL)=3, minimal law [x,_3 y]=[x,_129 y] (Brandl-Nikolova table: r=3, s=129)]
PASS  exact Engel depth of PSL(2,9)  [|PSL|=360, 7 classes, mu(PSL)=4, mu(SL)=4, minimal law [x,_4 y]=[x,_124 y] (Brandl-Nikolova table: r=4, s=124) (A_6; Nikolova 1984: [x,_4 y]=[x,_124 y])]
PASS  exact Engel depth of PSL(2,11)  [|PSL|=660, 8 classes, mu(PSL)=6, mu(SL)=6, minimal law [x,_6 y]=[x,_1986 y] (Brandl-Nikolova table: r=6, s=1986)]
PASS  exact Engel depth of PSL(2,13)  [|PSL|=1092, 9 classes, mu(PSL)=7, mu(SL)=7, minimal law [x,_7 y]=[x,_2191 y] (Brandl-Nikolova table: r=7, s=2191)]
PASS  exact Engel depth of PSL(2,16)  [|PSL|=4080, 17 classes, mu(PSL)=5, mu(SL)=5, minimal law [x,_5 y]=[x,_2045 y]]
PASS  Lemma 2.4(b): tail(rho, tau) = n in the dihedral group of order 2^(n+1), n = 2..10
PASS  Lemma 2.4(c): D of order 2^(k+1) inside A_(2^k+2), even generators, tail k (k = 2..6)  [A_6: 2, A_10: 3, A_18: 4, A_34: 5, A_66: 6]
PASS  Lemma 3.4(a): R_r(h,c) monic in h, = h^(2^r) mod c, constant term c (Eisenstein), r = 1..6
PASS  Lemma 3.4(b): R_r(h,-tau(tau+4)) monic, = h^(2^r) mod tau, constant term -4tau-tau^2, r = 1..5
PASS  Lemma 3.4: Newton polygon = one segment of slope -2^-r (p = 2,3,5,7 resp. 3,5,7; fails for p = 2 in (b))
PASS  Lemma 3.4: total degrees 2^r (r <= 6) and 3*2^(r-1) (r <= 5)
PASS  Theorem 3.5: Q_r = ((d-1)(d-2)+2)^2 for r = 1..7 (q odd), 1..4 (q even)  [odd: [16, 484, 12544, 258064]; even: [4, 64, 1936, 44944]]
PASS  Theorem 3.5: point count positive for q > Q_r, and Q_r < 2^(4r+4) (r = 1..40)
PASS  Theorem 3.5 construction: point with c != 0, pair (x,y), PSL tail >= r+1 (>= r+2 if q even or s != 0)  [38 cases, 22 of them with q > Q_r; a point was found in every case]
PASS  Sz(8): generators preserve J; <U(1,0), U(0,1), M(c), T> has order 29120 = 8^2(8^2+1)(8-1)  [order 29120]
PASS  Sz(8): mu >= 62 from the pair printed in sz8_exact_all.txt  [x = U(1,1) M(1) T U(1,0); y = U(4,3) M(2) T U(0,3); exact tail 62, period 90 (all terms stored); pair found in the recorded output; 0.0s]
PASS  Sz(32): mu >= 527 from the pair printed in sz32_exact_all.txt  [x = U(0,0) M(25) T U(17,27); y = U(28,18) M(3) T U(4,26); exact tail 527, period 1275 (all terms stored); pair found in the recorded output; 0.0s]
PASS  Sz(128): mu >= 3759 from the pair printed in sz128_sample.txt  [x = U(59,88) M(116) T U(46,80); y = U(52,55) M(68) T U(55,34); tail certificate: a_56083 = a_3759, a_56082 != a_3758; pair found in the recorded output; 0.8s]
PASS  Sz(128): mu >= 3554 from the pair printed in sz128_quot.txt  [x = U(88,73) M(98) T U(72,65); y = U(0,0) M(33); tail certificate: torus orbits of a_3966, a_3554 equal; of a_3965, a_3553 different; pair found in the recorded output; 0.0s]
PASS  Sz(512): mu >= 24814 from the pair printed in sz512_quot.txt  [x = U(283,406) M(18) T U(443,310); y = U(0,0) M(150); tail certificate: torus orbits of a_25105, a_24814 equal; of a_25104, a_24813 different; pair found in the recorded output; 0.4s]
PASS  Sz(2048): mu >= 183810 from the pair printed in sz2048_quot.txt  [x = U(1411,53) M(685) T U(1609,1128); y = U(0,0) M(553); tail certificate: torus orbits of a_194365, a_183810 equal; of a_194364, a_183809 different; pair found in the recorded output; 2.8s]
PASS  Sz(8192): mu >= 792500 from the pair printed in sz8192_quot.txt  [x = U(1629,10) M(2415) T U(3571,3855); y = U(0,0) M(3585); tail certificate: torus orbits of a_1071904, a_792500 equal; of a_1071903, a_792499 different; pair found in the recorded output; 14.9s]
PASS  Corollary 5.4: for 3 <= r <= 61 the undecided Sz(2^n) (n odd < 200) are those with gcd(n,15015) = 1  [n = [17, 19, 23, 29, 31, 37, 41, 43], ...]
SUMMARY: 28 of 28 checks passed (21 s)
