code wiki / (root) / nx_theorems8_test.nx

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}