code wiki / (root) / nx_theorems5_test.nx

nx_theorems5_test.nx source

↩ module page · 147 lines · 6401 B

1// nx_theorems5_test.nx -- Freek-100 quick-wins verification. 2 3import "syscalls.nx" 4import "nx_qed_freek.nx" 5 6func main() -> i64 { 7 // Freek #1 -- sqrt(2) irrational. 8 // For coprime (a,b), a^2 != 2 b^2. Try (3,2): 9 != 8 PASS. 9 if nx_th_sqrt2_irrational_check(3, 2) != 1 { return 1 } 10 if nx_th_sqrt2_irrational_check(7, 5) != 1 { return 2 } 11 // Non-coprime (2, 2) should NOT pass. 12 if nx_th_sqrt2_irrational_check(2, 2) != 0 { return 3 } 13 14 // Freek #3 -- Cantor pairing. 15 // pair(0, 0) = 0; pair(0, 1) = 2; pair(1, 0) = 1; pair(2, 0) = 3. 16 if nx_th_cantor_pairing(0, 0) != 0 { return 4 } 17 if nx_th_cantor_pairing(0, 1) != 2 { return 5 } 18 if nx_th_cantor_pairing(1, 0) != 1 { return 6 } 19 if nx_th_cantor_pairing(2, 0) != 3 { return 7 } 20 // Inversion: unpair(2) = (0, 1). 21 if nx_th_cantor_unpair_a(2) != 0 { return 8 } 22 if nx_th_cantor_unpair_b(2) != 1 { return 9 } 23 24 // Freek #11 -- Euclid's infinite primes. Given [2,3,5]: product=30; +1=31 is prime. 25 let primes: *i64 = (sys_mmap(40)) as *i64 26 primes[0] = 2; primes[1] = 3; primes[2] = 5 27 let w: i64 = nx_th_euclid_prime_witness(primes, 3) 28 if w != 31 { return 10 } 29 // [2,3]: product=6; +1=7 prime. 30 let p2: *i64 = (sys_mmap(16)) as *i64 31 p2[0] = 2; p2[1] = 3 32 if nx_th_euclid_prime_witness(p2, 2) != 7 { return 11 } 33 34 // Freek #23 -- Pythagorean triple (m=2, n=1): (3, 4, 5). 35 if nx_th_pyth_triple_a(2, 1) != 3 { return 12 } 36 if nx_th_pyth_triple_b(2, 1) != 4 { return 13 } 37 if nx_th_pyth_triple_c(2, 1) != 5 { return 14 } 38 if nx_th_pyth_triple_verify(2, 1) != 1 { return 15 } 39 if nx_th_pyth_triple_verify(3, 2) != 1 { return 16 } // (5, 12, 13) 40 if nx_th_pyth_triple_verify(4, 1) != 1 { return 17 } // (15, 8, 17) 41 42 // Freek #34 -- Harmonic divergence. H_4 = 1 + 1/2 + 1/3 + 1/4 = 25/12 ≈ 2.083. 43 let h4: i64 = nx_th_harmonic_ppb(4) 44 if h4 < 2000000000 { return 18 } 45 if h4 > 2200000000 { return 19 } 46 // Bound: H_{2^N} >= 1 + N/2. At N=4 (so n=16): H_16 >= 3. 47 let h16: i64 = nx_th_harmonic_ppb(16) 48 if h16 < nx_th_harmonic_lower_bound_ppb(4) { return 20 } 49 50 // Freek #65 -- Isosceles. 51 if nx_th_isosceles_check(5, 5, 6) != 1 { return 21 } 52 if nx_th_isosceles_check(5, 6, 7) != 0 { return 22 } 53 54 // Freek #66 -- Geometric series. 55 // 1 + 2 + 4 + 8 = (16-1)/(2-1) = 15. 56 if nx_th_geometric_sum(2, 4) != 15 { return 23 } 57 // 1 + 3 + 9 + 27 = 40 (r=3, n=4 -> (81-1)/2 = 40). 58 if nx_th_geometric_sum(3, 4) != 40 { return 24 } 59 // r=1 case: sum_{k=0..n-1} 1 = n. 60 if nx_th_geometric_sum(1, 5) != 5 { return 25 } 61 62 // Freek #68 -- Arithmetic series. 63 // 0 + 1 + 2 + 3 + 4 = 10 (a=0, d=1, n=5 -> 5*0 + 1*5*4/2 = 10). 64 if nx_th_arithmetic_sum(0, 1, 5) != 10 { return 26 } 65 // a=5, d=3, n=4: 5 + 8 + 11 + 14 = 38. 66 if nx_th_arithmetic_sum(5, 3, 4) != 38 { return 27 } 67 68 // Freek #80 -- Fundamental theorem of arithmetic. 69 // 12 = 2^2 * 3. 60 = 2^2 * 3 * 5. 70 let pairs: *i64 = (sys_mmap(80)) as *i64 71 let cnt12: i64 = nx_th_prime_factorize(12, pairs, 10) 72 if cnt12 != 2 { return 28 } 73 if pairs[0] != 2 { return 29 } 74 if pairs[1] != 2 { return 30 } 75 if pairs[2] != 3 { return 31 } 76 if pairs[3] != 1 { return 32 } 77 let cnt60: i64 = nx_th_prime_factorize(60, pairs, 10) 78 if cnt60 != 3 { return 33 } 79 80 // Freek #81 -- Prime reciprocal sum. At N=10: 1/2+1/3+1/5+1/7 = 0.5+0.333+0.2+0.143 = ~1.176. 81 let s: i64 = nx_th_prime_reciprocal_sum_ppb(10) 82 if s < 1100000000 { return 34 } 83 if s > 1200000000 { return 35 } 84 85 // Freek #85 -- Divisibility by 3. 86 if nx_th_divisible_by_3_via_digit_sum(12345) != 1 { return 36 } // 1+2+3+4+5=15 87 if nx_th_divisible_by_3_via_digit_sum(100) != 0 { return 37 } // 1 88 if nx_th_divisible_by_3_via_digit_sum(0) != 1 { return 38 } // 0 89 90 // Freek #88 -- Derangement. D_0=1, D_1=0, D_2=1, D_3=2, D_4=9, D_5=44. 91 if nx_th_derangement(0) != 1 { return 39 } 92 if nx_th_derangement(1) != 0 { return 40 } 93 if nx_th_derangement(2) != 1 { return 41 } 94 if nx_th_derangement(3) != 2 { return 42 } 95 if nx_th_derangement(4) != 9 { return 43 } 96 if nx_th_derangement(5) != 44 { return 44 } 97 98 // Freek #89 -- Horner / factor. 99 // f(x) = 2x^3 - 3x^2 + 0*x - 1 = 2x^3 - 3x^2 - 1 100 // coeffs [low..high]: [-1, 0, -3, 2] 101 let c: *i64 = (sys_mmap(32)) as *i64 102 c[0] = -1; c[1] = 0; c[2] = -3; c[3] = 2 103 // f(1) = -1 + 0 - 3 + 2 = -2. 104 if nx_th_horner_eval(c, 3, 1) != -2 { return 45 } 105 // f(2) = -1 + 0 - 12 + 16 = 3. 106 if nx_th_horner_eval(c, 3, 2) != 3 { return 46 } 107 // (x - 1) doesn't divide f (f(1) != 0). 108 if nx_th_factor_check(c, 3, 1) != 0 { return 47 } 109 110 // Freek #93 -- Birthday problem. P(collision among 23) ~= 0.507. 111 let bc23: i64 = nx_th_birthday_collision_ppb(23) 112 if bc23 < 500000000 { return 48 } 113 if bc23 > 520000000 { return 49 } 114 // P(no collision) at n=2 = 364/365. 115 let bnc2: i64 = nx_th_birthday_no_collision_ppb(2) 116 let expected_bnc2: i64 = (364 * 1000000000) / 365 117 if bnc2 < expected_bnc2 - 1 { return 50 } 118 if bnc2 > expected_bnc2 + 1 { return 51 } 119 120 // Freek #100 -- Descartes signs. 121 // f(x) = x^3 - 3x^2 + 2x - 1: signs +, -, +, - -> 3 changes. 122 let dc: *i64 = (sys_mmap(32)) as *i64 123 dc[0] = -1; dc[1] = 2; dc[2] = -3; dc[3] = 1 124 if nx_th_descartes_sign_changes(dc, 3) != 3 { return 52 } 125 // f(x) = x^2 + x + 1: signs +, +, + -> 0 changes. 126 dc[0] = 1; dc[1] = 1; dc[2] = 1; dc[3] = 0 127 if nx_th_descartes_sign_changes(dc, 2) != 0 { return 53 } 128 129 // Freek #74 -- Induction. 130 let pred: *i64 = (sys_mmap(80)) as *i64 131 pred[0] = 1; pred[1] = 1; pred[2] = 1; pred[3] = 1; pred[4] = 1 132 if nx_th_induction_verify(pred, 4) != 1 { return 54 } 133 pred[2] = 0 134 if nx_th_induction_verify(pred, 4) != 0 { return 55 } 135 136 // Bonus: Platonic solids count. 137 if nx_th_num_platonic_solids() != 5 { return 56 } 138 139 // Bonus: 4-square -- Lagrange. 7 = 4+1+1+1 = 2^2+1+1+1. PASS. 140 if nx_th_four_squares_witness(7) != 1 { return 57 } 141 // 23 = 9+9+4+1. PASS. 142 if nx_th_four_squares_witness(23) != 1 { return 58 } 143 // 31 = 25+4+1+1. PASS. 144 if nx_th_four_squares_witness(31) != 1 { return 59 } 145 146 return 0 147}