check_note.py -- AMR-150-0035 -- Python 3.13.5
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=2 k=1                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=2 k=1 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=2 k=1 
PASS   A4 (9) commutator formula  p=2 k=1                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=2 k=1 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=2 k=1                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=2 k=2                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=2 k=2 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=2 k=2 
PASS   A4 (9) commutator formula  p=2 k=2                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=2 k=2 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=2 k=2                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=2 k=3                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=2 k=3 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=2 k=3 
PASS   A4 (9) commutator formula  p=2 k=3                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=2 k=3 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=2 k=3                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=2 k=4                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=2 k=4 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=2 k=4 
PASS   A4 (9) commutator formula  p=2 k=4                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=2 k=4 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=2 k=4                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=3 k=1                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=3 k=1 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=3 k=1 
PASS   A4 (9) commutator formula  p=3 k=1                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=3 k=1 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=3 k=1                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=3 k=2                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=3 k=2 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=3 k=2 
PASS   A4 (9) commutator formula  p=3 k=2                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=3 k=2 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=3 k=2                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=5 k=1                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=5 k=1 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=5 k=1 
PASS   A4 (9) commutator formula  p=5 k=1                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=5 k=1 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=5 k=1                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=5 k=2                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=5 k=2 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=5 k=2 
PASS   A4 (9) commutator formula  p=5 k=2                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=5 k=2 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=5 k=2                    
PASS   A1 group law, inverse, x v x^-1 = (1+t)v  p=7 k=1                      
PASS   A2 (6) valuations, (1+t)^(p^n) = 1 + t^(p^n), coefficient of t  p=7 k=1 
PASS   A3 (8) powers (x^lam v)^n and (x^lam v)^(p^e) = x^(p^e lam) u^(p^e-1) v  p=7 k=1 
PASS   A4 (9) commutator formula  p=7 k=1                                     
PASS   A5 W_k -> W_j homomorphisms, kernel S(j,p^j) normal of the right order  p=7 k=1 
PASS   A6 x, y generate W_k (log_p order k + p^k)  p=7 k=1                    
PASS   A7 (s-1)^(p^j) = s^(p^j) - 1 in F_p[s]  (p <= 7, j <= 3)               
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=2 k=1          non-normal controls: 1
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=2 k=1 15 terms; wrong formulas detected at 8 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=2 k=2          non-normal controls: 5
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=2 k=2 22 terms; wrong formulas detected at 14 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=2 k=3          non-normal controls: 17
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=2 k=3 33 terms; wrong formulas detected at 24 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=2 k=4          non-normal controls: 49
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=2 k=4 52 terms; wrong formulas detected at 42 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=2 k=5          non-normal controls: 129
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=2 k=5 87 terms; wrong formulas detected at 76 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=3 k=1          non-normal controls: 2
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=3 k=1 17 terms; wrong formulas detected at 10 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=3 k=2          non-normal controls: 14
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=3 k=2 32 terms; wrong formulas detected at 24 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=3 k=3          non-normal controls: 68
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=3 k=3 71 terms; wrong formulas detected at 62 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=5 k=1          non-normal controls: 4
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=5 k=1 21 terms; wrong formulas detected at 14 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=5 k=2          non-normal controls: 44
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=5 k=2 64 terms; wrong formulas detected at 56 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=7 k=1          non-normal controls: 6
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=7 k=1 25 terms; wrong formulas detected at 18 terms
PASS   B1 S(a,b) normal of index p^(a+b) iff p^a >= b (a<k)  p=7 k=2          non-normal controls: 90
PASS   B2 five standard series of W_k from the definitions = S(a,b) of Prop. 4.2  p=7 k=2 112 terms; wrong formulas detected at 104 terms
PASS   B3 brute force: series as sets of elements agree  p=2 k=1              15 terms
PASS   B3 brute force: series as sets of elements agree  p=2 k=2              22 terms
PASS   B3 brute force: series as sets of elements agree  p=3 k=1              17 terms
PASS   C1 (12): log_p|U_A S : S| = |A cap [0,b)| for all series terms and K_j 5900 comparisons; control with (1+t)^j-coordinates violates (12) 87 times
PASS   C2 Lemma 4.3(c): coset x^lam w S(a,b) meets U_A iff criterion (brute force) 120114 cosets
PASS   D1 Thm 1.3 Step 2: log_p|K P_i : P_i| = (i-1-n) + |J cap [0,i-1)|      765 comparisons (a formula off by one fails in all of them)
PASS   D2 Thm 1.3 Step 2: J + p^n contained in J (inside [0,p^k))             
PASS   D3 Thm 1.3 Step 3: K_{n,m} = <x^(p^n)> U_A(n,m) has K cap B = U_A(n,m) 31 cases
PASS   E1 inequalities: p^(i-1)>=i, f_(i+1)=f_i+p^i, e_ceil(i/p)=e_i-1, (p-1)p^(e-1)+ceil(i/p)>=i, p^n(p^c-1)>=n+c 
PASS   E2 index sequences: p^a>=b, b strictly increasing, ratio bounds of the table, a/b small 
PASS   F  Lemma 3.2 on "alternating 3/10, 7/10"                               (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 6, 18), (2, 40, 160), (3, 374, 1870)]; tail min 0.2791
PASS   F  Lemma 3.2 on "1/2 + (-1)^k/(k+2)"                                   (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 6, 18), (2, 48, 192), (3, 480, 2400)]; tail min 0.2981
PASS   F  Lemma 3.2 on "constant 0"                                           (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 6, 18), (2, 24, 96), (3, 120, 600), (4, 720, 4320)]; tail min 0.1427
PASS   F  Lemma 3.2 on "constant 1"                                           (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 6, 18), (2, 24, 96), (3, 120, 600), (4, 720, 4320)]; tail min 0.7934
PASS   F  Lemma 3.2 on "1 - 1/(k+1), 1/(k+1) alternating"                     (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 5, 15), (2, 23, 92), (3, 246, 1230)]; tail min 0.2470
PASS   F  Lemma 3.2 on "lower approximations of sqrt2-1 / 9/10"               (UI) True count True bounds True transit True hits True; phases [(0, 2, 4), (1, 6, 18), (2, 30, 120), (3, 354, 1770)]; tail min 0.3824
PASS   G  Remark 5.3: counts for A = N minus [4*9^m, 8*9^m)                   delta(8*9^12) = 0.437500000000, delta(3*9^12-1) = 0.833333333334, delta(9^m-1) = 1/2
PASS   H  Remark 5.4: I_j = S(j, beta_j) (normal subgroups of index <= p^j, of all) p=2 k=2 j=0: 1 of 13; p=2 k=2 j=1: 4 of 13; p=2 k=2 j=2: 7 of 13; p=2 k=3 j=0: 1 of 26; p=2 k=3 j=1: 4 of 26; p=2 k=3 j=2: 7 of 26; p=2 k=3 j=3: 12 of 26; p=3 k=1 j=0: 1 of 8; p=3 k=1 j=1: 5 of 8
97 checks, 0 failed, running time 27.6 s
ALL CHECKS PASSED
