nx_theorems8_test.nx source
↩ module page · 99 lines · 4573 B
1// nx_theorems8_test.nx -- batch 8 verification.
2
3import "syscalls.nx"
4import "nx_qed_freek.nx"
5
6func main() -> i64 {
7 // #2 FTA quadratic: x^2 + 0x + 1 = 0 -> disc = -4 < 0 -> complex roots.
8 if nx_th_fta_quadratic_root_kind(0, 1) != -1 { return 2 }
9 // x^2 - 5x + 6 = 0 -> disc = 25 - 24 = 1 > 0 -> 2 real roots.
10 if nx_th_fta_quadratic_root_kind(-5, 6) != 1 { return 3 }
11 // x^2 - 2x + 1 = 0 -> disc = 0 -> double root.
12 if nx_th_fta_quadratic_root_kind(-2, 1) != 0 { return 4 }
13
14 // #28 Pascal hexagon: simplest collinear test.
15 // (0,0), (1,1), (2,2) collinear; (0,0), (1,1), (2,3) not.
16 if nx_th_collinear_check(0, 0, 1, 1, 2, 2) != 1 { return 28 }
17 if nx_th_collinear_check(0, 0, 1, 1, 2, 3) != 0 { return 29 }
18
19 // #29 Feuerbach: 3 non-collinear midpoints exist.
20 if nx_th_feuerbach_nine_point_exists(0, 0, 1, 0, 0, 1) != 1 { return 30 }
21 // Collinear midpoints -> no unique circle.
22 if nx_th_feuerbach_nine_point_exists(0, 0, 1, 0, 2, 0) != 0 { return 31 }
23
24 // #31 Ramsey R(3,3): in K_6 every 2-coloring has mono triangle.
25 // Construct a 6x6 coloring; substrate finds the mono triangle.
26 let col: *i64 = (sys_mmap(288)) as *i64 // 6*6 = 36 ints, but i64 each
27 var i: i64 = 0
28 while i < 36 { col[i] = 0; i = i + 1 }
29 // All edges color 0 -> trivially mono.
30 if nx_th_ramsey_find_mono_triangle(col, 6) != 1 { return 32 }
31 // K_5 (n=5) might have NO mono triangle with right coloring (Ramsey
32 // R(3,3)=6 means 5 isn't sufficient). Carefully: a 2-coloring of K_5
33 // with no mono triangle exists (5-cycle + diagonals colored alternately).
34 // For substrate, we just verify our search works correctly: feed a
35 // coloring with NO mono triangle and confirm it returns 0.
36 // 5-vertex cycle: color edges of pentagon 0, diagonals 1.
37 var j: i64 = 0
38 while j < 36 { col[j] = -1; j = j + 1 }
39 let n5: i64 = 5
40 // pentagon edges (0-1, 1-2, 2-3, 3-4, 4-0): color 0
41 col[0*n5+1] = 0; col[1*n5+0] = 0
42 col[1*n5+2] = 0; col[2*n5+1] = 0
43 col[2*n5+3] = 0; col[3*n5+2] = 0
44 col[3*n5+4] = 0; col[4*n5+3] = 0
45 col[4*n5+0] = 0; col[0*n5+4] = 0
46 // pentagon diagonals: color 1
47 col[0*n5+2] = 1; col[2*n5+0] = 1
48 col[1*n5+3] = 1; col[3*n5+1] = 1
49 col[2*n5+4] = 1; col[4*n5+2] = 1
50 col[3*n5+0] = 1; col[0*n5+3] = 1
51 col[4*n5+1] = 1; col[1*n5+4] = 1
52 // No monochromatic triangle in this K_5 coloring.
53 if nx_th_ramsey_find_mono_triangle(col, 5) != 0 { return 33 }
54
55 // #36 Brouwer 1D fixed point: f(x) = x (trivially every point).
56 // f(x) = -x + 5 on [0, 5]: f(0)=5, f(5)=0. Fixed point at x = 2.5.
57 // Integer-valued: take f(x) = 5 - x on [0, 5]: f(2)=3, f(3)=2.
58 // Function 5 - x crosses x at x=2.5 (not integer). Test f(x) = (10-x)/2:
59 // simpler: f(x) = -x+6 on [0, 6]. f(3)=3 fixed.
60 let fp: *i64 = (sys_mmap(16)) as *i64
61 fp[0] = 6; fp[1] = -1 // -x + 6
62 let outp: *i64 = (sys_mmap(8)) as *i64
63 if nx_th_brouwer_1d_fixed_point(fp, 1, 0, 6, outp) != 1 { return 36 }
64 if outp[0] != 3 { return 37 }
65
66 // #43 Isoperimetric: circle ratio ~= 1.
67 if nx_th_isoperimetric_check_circle() != 1 { return 43 }
68 if nx_th_isoperimetric_check_square() != 1 { return 44 }
69
70 // #67 e not root: polynomial 1 (constant) -- e is not a root of constant 1.
71 let pe: *i64 = (sys_mmap(40)) as *i64
72 pe[0] = 1
73 if nx_th_e_not_root_of(pe, 0, 1000000) != 1 { return 67 }
74 // p(x) = x - 3 (root at 3, not e). At x=e ~ 2.718, p(e) = -0.282 -> not near 0.
75 pe[0] = -3; pe[1] = 1
76 if nx_th_e_not_root_of(pe, 1, 100000000) != 1 { return 68 }
77
78 // #76 Fourier partial: a0=2, n=0 -> sum = 1. Check basic.
79 let an: *i64 = (sys_mmap(40)) as *i64
80 let bn: *i64 = (sys_mmap(40)) as *i64
81 var k: i64 = 0
82 while k < 5 { an[k] = 0; bn[k] = 0; k = k + 1 }
83 let f0: i64 = nx_th_fourier_partial_eval_ppb(2000000000, an, bn, 0, 0)
84 if f0 != 1000000000 { return 76 }
85 // Trig sanity: cos(0)=1, cos(180) ~ -1.
86 let c0: i64 = nx_th_cos_ppb_from_deg(0)
87 if c0 != 1000000000 { return 77 }
88
89 // #82 Min cube dissection.
90 if nx_th_min_cube_dissection() != 54 { return 82 }
91
92 // #87 Desargues axis: 3 collinear intersection points.
93 if nx_th_desargues_axis_check(0, 0, 1, 1, 2, 2) != 1 { return 87 }
94
95 // Bonus #21 Green: unit square area = 1 -> 2*Area = 2.
96 if nx_th_green_unit_square_check() != 1 { return 21 }
97
98 return 0
99}