nx_theorems_test.nx source
↩ module page · 88 lines · 3707 B
1// nx_theorems_test.nx -- verify the batch-1 theorem primitives.
2
3import "syscalls.nx"
4import "nx_qed_freek.nx"
5
6func main() -> i64 {
7 // #1 Pythagorean -- (3, 4, 5) is a triple; (3, 4, 6) is not.
8 if nx_th_pythagorean_check(3, 4, 5) != 1 { return 1 }
9 if nx_th_pythagorean_check(5, 12, 13) != 1 { return 2 }
10 if nx_th_pythagorean_check(3, 4, 6) != 0 { return 3 }
11
12 // #2 GCD -- gcd(48, 18) = 6; gcd(0, 5) = 5; gcd(17, 13) = 1.
13 if nx_th_gcd(48, 18) != 6 { return 11 }
14 if nx_th_gcd(0, 5) != 5 { return 12 }
15 if nx_th_gcd(17, 13) != 1 { return 13 }
16
17 // #3 Bezout -- gcd(30, 18) = 6 with 30*s + 18*t = 6.
18 let bz: *BezoutResult = nx_th_bezout_alloc()
19 nx_th_bezout(30, 18, bz)
20 if bz.g != 6 { return 21 }
21 if 30 * bz.s + 18 * bz.t != 6 { return 22 }
22
23 // #4 Markov bound -- if E[X]=0.3, P(X>=1) <= 0.3.
24 let mb: i64 = nx_th_markov_bound_ppb(300000000, 1000000000)
25 if mb != 300000000 { return 31 }
26 // E[X]=0.5, P(X>=0.5) <= 1.0 (trivial).
27 let mb2: i64 = nx_th_markov_bound_ppb(500000000, 500000000)
28 if mb2 != 1000000000 { return 32 }
29
30 // #5 Chebyshev -- P(|X-mu|>=2sigma) <= 0.25.
31 let cb: i64 = nx_th_chebyshev_bound_ppb(20)
32 if cb != 250000000 { return 41 }
33 // P(|X-mu|>=3sigma) <= 1/9 ~ 0.111.
34 let cb2: i64 = nx_th_chebyshev_bound_ppb(30)
35 if cb2 < 111000000 { return 42 }
36 if cb2 > 112000000 { return 43 }
37
38 // #6 Cauchy-Schwarz -- u=(1,2,3), v=(2,4,6): equality (collinear).
39 let u: *i64 = (sys_mmap(24)) as *i64
40 let v: *i64 = (sys_mmap(24)) as *i64
41 u[0] = 1; u[1] = 2; u[2] = 3
42 v[0] = 2; v[1] = 4; v[2] = 6
43 if nx_th_cauchy_schwarz_check(u, v, 3) != 1 { return 51 }
44 // u=(1,0,0), v=(0,1,0): orthogonal so |<u,v>|^2=0 < uu*vv=1.
45 u[0] = 1; u[1] = 0; u[2] = 0
46 v[0] = 0; v[1] = 1; v[2] = 0
47 if nx_th_cauchy_schwarz_check(u, v, 3) != 1 { return 52 }
48
49 // #7 Jensen on x^2 -- data {1, 2, 3}: mean=2, mean^2=4,
50 // mean(x^2) = (1+4+9)/3 = 14/3 = 4 (int trunc). 4 <= 4 PASS.
51 let d: *i64 = (sys_mmap(24)) as *i64
52 d[0] = 1; d[1] = 2; d[2] = 3
53 if nx_th_jensen_check_sq(d, 3) != 1 { return 61 }
54
55 // Data {0, 10}: mean=5, mean^2=25; mean(x^2) = (0+100)/2 = 50. 25<=50 PASS.
56 d[0] = 0; d[1] = 10
57 if nx_th_jensen_check_sq(d, 2) != 1 { return 62 }
58
59 // #8 Binomial -- C(5,2)=10; C(10,3)=120; C(6,6)=1; C(7,0)=1.
60 if nx_th_binomial(5, 2) != 10 { return 71 }
61 if nx_th_binomial(10, 3) != 120 { return 72 }
62 if nx_th_binomial(6, 6) != 1 { return 73 }
63 if nx_th_binomial(7, 0) != 1 { return 74 }
64 if nx_th_binomial(7, -1) != 0 { return 75 }
65 if nx_th_binomial(7, 8) != 0 { return 76 }
66
67 // #9 Pigeonhole -- 10 pigeons in 3 holes: ceil(10/3) = 4.
68 if nx_th_pigeonhole_min_max(10, 3) != 4 { return 81 }
69 if nx_th_pigeonhole_min_max(100, 7) != 15 { return 82 }
70 if nx_th_pigeonhole_min_max(5, 5) != 1 { return 83 }
71
72 // #10 Bayes -- P(B|A)=0.9, P(A)=0.01, P(B)=0.1 -> P(A|B)=0.09.
73 let bayes: i64 = nx_th_bayes_posterior_ppb(900000000, 10000000, 100000000)
74 if bayes != 90000000 { return 91 }
75
76 // #11 Hoeffding bound at n=100, t=0.1, W=1.0:
77 // arg = 2*100*0.01/1 = 2 -> exp(-2) ~ 0.135 -> bound ~ 0.27.
78 let hb: i64 = nx_th_hoeffding_bound_ppb(100, 100000000, 1000000000)
79 if hb < 200000000 { return 101 }
80 if hb > 400000000 { return 102 }
81
82 // #12 Inclusion-exclusion -- |A|=10, |B|=8, |A^B|=3 -> 15.
83 if nx_th_incl_excl_2(10, 8, 3) != 15 { return 111 }
84 // 3-set: A=B=C=10 each; pairwise 4 each; triple 2 -> 10+10+10-4-4-4+2=20.
85 if nx_th_incl_excl_3(10, 10, 10, 4, 4, 4, 2) != 20 { return 112 }
86
87 return 0
88}