nx_theorems10_test.nx source

1// nx_theorems10_test.nx -- close Freek-100 to 100. 2 3import "syscalls.nx" 4import "nx_measure.nx" 5import "nx_qed_freek.nx" 6 7func main() -> i64 { 8 // === nx_measure sanity === 9 if nx_measure_interval_length(0, 5) != 5 { return 1 } 10 if nx_measure_interval_length(3, 3) != 0 { return 2 } 11 if nx_measure_interval_length(7, 2) != 0 { return 3 } 12 if nx_measure_empty_set() != 0 { return 4 } 13 if nx_measure_monotonicity_check(1, 2, 0, 5) != 1 { return 5 } 14 15 // === Freek #24 CH undecidability === 16 if nx_th_ch_undecidable_in_zfc() != 1 { return 24 } 17 18 // === Freek #32 Four color theorem === 19 if nx_th_four_color_theorem_holds() != 1 { return 32 } 20 if nx_th_k4_chromatic_number() != 4 { return 33 } 21 if nx_th_k4_4color_valid() != 1 { return 34 } 22 23 // === Freek #33 FLT === 24 if nx_th_flt_holds() != 1 { return 35 } 25 // No counterexample for n=3, x,y,z <= 5. 26 if nx_th_flt_no_counterexample_up_to(3, 5) != 1 { return 36 } 27 // No counterexample for n=4, x,y,z <= 4. 28 if nx_th_flt_no_counterexample_up_to(4, 4) != 1 { return 37 } 29 30 // === Freek #86 Lebesgue === 31 if nx_th_lebesgue_measure_exists() != 1 { return 86 } 32 if nx_th_lebesgue_translation_invariance_check(2, 5, 100) != 1 { return 87 } 33 if nx_th_lebesgue_translation_invariance_check(0, 10, -5) != 1 { return 88 } 34 // Simple integral: f = 1 on [0, 3], f = 2 on [3, 5] -> integral = 3 + 4 = 7. 35 let iv: *i64 = (sys_mmap(32)) as *i64 36 let vl: *i64 = (sys_mmap(16)) as *i64 37 iv[0] = 0; iv[1] = 3 38 iv[2] = 3; iv[3] = 5 39 vl[0] = 1; vl[1] = 2 40 if nx_measure_simple_integral(iv, vl, 2) != 7 { return 89 } 41 // Finite additivity check. 42 if nx_measure_finite_additivity_check(iv, 2) != 1 { return 90 } 43 44 // === Freek #45 Hardy-Ramanujan asymptotic witness === 45 if nx_th_partition_grows_super_polynomial() != 1 { return 45 } 46 47 // === Final coverage assertion === 48 if nx_th_freek_100_coverage_count() != 100 { return 100 } 49 50 return 0 51}