nx_theorems9_test.nx source
↩ module page · 105 lines · 4616 B
1// nx_theorems9_test.nx -- batch 9 verification.
2
3import "syscalls.nx"
4import "nx_group.nx"
5import "nx_lattice.nx"
6import "nx_qed_freek.nx"
7
8func main() -> i64 {
9 // === group primitives sanity ===
10 // Cyclic group Z_3: table[i*3+j] = (i+j) mod 3.
11 let t3: *i64 = (sys_mmap(72)) as *i64
12 var i: i64 = 0
13 while i < 3 {
14 var j: i64 = 0
15 while j < 3 {
16 t3[i * 3 + j] = (i + j) - ((i + j) / 3) * 3
17 j = j + 1
18 }
19 i = i + 1
20 }
21 if nx_group_verify_axioms(t3, 3) != 1 { return 1 }
22 if nx_group_element_order(t3, 3, 1) != 3 { return 2 }
23 if nx_group_element_order(t3, 3, 0) != 1 { return 3 }
24
25 // === lattice sanity ===
26 // Disk R=1: points (0,0), (±1,0), (0,±1) = 5 points.
27 if nx_lattice_disk_point_count(1) != 5 { return 4 }
28 // Rect A=2, B=3: (2*2+1)*(2*3+1) = 35 points.
29 if nx_lattice_rect_point_count(2, 3) != 35 { return 5 }
30
31 // #15 FTC: integrate p(x) = 2x + 1 over [0, 3].
32 // P(x) = x^2 + x. P(3) - P(0) = 12. Scaled (deg+1)! = 2.
33 // Our antideriv returns P(x) * fact. fact = 2! = 2.
34 // Antideriv: coeffs [1, 2]; P(x) = 1*x*2/1 + 2*x^2*2/2 = 2x + 2x^2.
35 // (2*3 + 2*9) - (0 + 0) = 24. out_scale = 2.
36 // True integral = 12. 24/2 = 12 ✓
37 let p15: *i64 = (sys_mmap(16)) as *i64
38 p15[0] = 1; p15[1] = 2
39 let out_scale: *i64 = (sys_mmap(8)) as *i64
40 let v: i64 = nx_th_ftc_definite_integral_scaled(p15, 1, 0, 3, out_scale)
41 if v / out_scale[0] != 12 { return 15 }
42
43 // #16 Quintic insolvable.
44 if nx_th_quintic_galois_group_order() != 120 { return 16 }
45 if nx_th_quintic_solvable_by_radicals() != 0 { return 17 }
46
47 // #18 Liouville: |sqrt(2) - 1/1| = 0.414 > 1/(3*1) = 0.333. PASS.
48 if nx_th_liouville_sqrt2_bound_check(1, 1) != 1 { return 18 }
49 // |sqrt(2) - 7/5| = 0.014, q=5, bound = 1/75 = 0.0133. Closely passes.
50 if nx_th_liouville_sqrt2_bound_check(7, 5) != 1 { return 19 }
51
52 // #40 Minkowski fundamental: rectangle A=2, B=2 (area = 16 > 4) -> has lattice points.
53 if nx_th_minkowski_fundamental_check(2, 2) != 1 { return 40 }
54 // A=B=1 (area = 4) NOT strictly > 4 -> may or may not work. We test
55 // the strict A*B > 1 case.
56 if nx_th_minkowski_fundamental_check(1, 1) != 0 { return 41 }
57
58 // #41 Puiseux y^2 = x: exponent 1/2.
59 if nx_th_puiseux_leading_num(1, 2) != 1 { return 42 }
60 if nx_th_puiseux_leading_denom(1, 2) != 2 { return 43 }
61 // y^3 = x^2: exponent 2/3.
62 if nx_th_puiseux_leading_num(2, 3) != 2 { return 44 }
63 if nx_th_puiseux_leading_denom(2, 3) != 3 { return 45 }
64 // y^4 = x^2: exponent 1/2 (reduced).
65 if nx_th_puiseux_leading_num(2, 4) != 1 { return 46 }
66 if nx_th_puiseux_leading_denom(2, 4) != 2 { return 47 }
67
68 // #53 pi not root of constants 1, 2, x - 3.
69 let pp: *i64 = (sys_mmap(32)) as *i64
70 pp[0] = 1; pp[1] = 0; pp[2] = 0; pp[3] = 0
71 if nx_th_pi_not_root_of(pp, 0, 1000) != 1 { return 53 }
72 pp[0] = -3; pp[1] = 1
73 if nx_th_pi_not_root_of(pp, 1, 100000) != 1 { return 54 }
74 // x^2 - 9 (roots ±3): pi^2 ~ 9.87, so pi^2 - 9 = 0.87 -- not a root.
75 pp[0] = -9; pp[1] = 0; pp[2] = 1
76 if nx_th_pi_not_root_of(pp, 2, 100000) != 1 { return 55 }
77
78 // #56 Hermite-Lindemann.
79 if nx_th_hermite_lindemann_e_to_alpha_transcendental(0) != 0 { return 56 } // α=0 case algebraic
80 if nx_th_hermite_lindemann_e_to_alpha_transcendental(1) != 1 { return 57 } // α≠0 case trans
81
82 // #72 Sylow. n=12, p=2: 12 = 4*3, so Sylow 2-subgroup has order 4.
83 if nx_th_sylow_subgroup_order(12, 2) != 4 { return 72 }
84 if nx_th_sylow_subgroup_order(12, 3) != 3 { return 73 }
85 if nx_th_sylow_subgroup_order(60, 5) != 5 { return 74 }
86 // Z_12 cyclic: unique Sylow 2 (n_2 = 1).
87 if nx_th_sylow_count_cyclic(12, 2) != 1 { return 75 }
88 // n=12, p=2, n_p=1: m=3, n_p=1 | 3 OK; n_p=1 ≡ 1 (mod 2) OK.
89 if nx_th_sylow_count_consistency_check(12, 2, 1) != 1 { return 76 }
90 // n=12, p=2, n_p=3: m=3, 3 | 3 OK; 3 ≡ 1 (mod 2) OK.
91 if nx_th_sylow_count_consistency_check(12, 2, 3) != 1 { return 77 }
92
93 // #6 Godel incompleteness fact.
94 if nx_th_godel_incompleteness_holds() != 1 { return 6 }
95
96 // #8 Angle trisection impossible.
97 if nx_th_angle_trisection_impossible() != 1 { return 8 }
98
99 // #12 Parallel postulate independence.
100 if nx_th_parallel_postulate_independent() != 1 { return 12 }
101 if nx_th_parallel_postulate_lines(0) != 1 { return 13 }
102 if nx_th_parallel_postulate_lines(2) != 0 { return 14 }
103
104 return 0
105}