nx_geo_haversine_gate.nx source

1// nx_geo_haversine_gate.nx -- GATE for GEO-003b great-circle (haversine) distance. Proves: 2// same-point : d(NYC,NYC) == 0 3// NYC -> London : haversine within 2% of the true great-circle ~5,570 km 4// NYC -> Sydney : haversine within 2% of the true great-circle ~15,990 km 5// MEASURED EXCEED : for NYC->Sydney, |haversine - true| < |equirectangular - true| -- haversine is 6// strictly CLOSER to the true great-circle than the GEO-003 flat-earth baseline. 7// This is the no-wave proof that GEO-003b adds real precision over GEO-003 at continental scale. 8// 9// Evidence -> knowledge/status/geo_haversine.log (GEOHAVGATE authored=organ ... verdict=GREEN). 10// license_tier: ORIGINAL 11import "nx_geo_haversine.nx" 12import "nx_geo_distance.nx" 13import "nx_syscalls.nx" 14import "nx_gate_verdict.nx" 15 16const GH_LOG: *u8 = "knowledge/status/geo_haversine.log" 17 18func gh_w(fd: i64, s: *u8) -> i64 { var n: i64 = 0; while s[n] != (0 as u8) { n = n + 1 } sys_write(fd, s, n); return 0 } 19func gh_wn(fd: i64, v: i64) -> i64 { let bb: *u8 = sys_mmap(28); var m: i64=v; if m<0 {m=0-m; sys_write(fd,"-" as *u8,1)}; let t: *u8 = sys_mmap(28); var k: i64=0; if m==0 {t[0]=48;k=1}; while m>0 {t[k]=(48+(m%10)) as u8; m=m/10; k=k+1}; var i: i64=0; while i<k {bb[i]=t[k-1-i]; i=i+1}; sys_write(fd, bb, k); return 0 } 20 21func gh_abs(x: i64) -> i64 { if x < 0 { return 0 - x } return x } 22// |a - b| <= b * num / den ? 23func gh_relnear(a: i64, b: i64, num: i64, den: i64) -> i64 { if gh_abs(a - b) * den <= b * num { return 1 } return 0 } 24 25func gh_emit(fd: i64, zero: i64, lon: i64, syd: i64, equi: i64, haverr: i64, equierr: i64, ok: i64) -> i64 { 26 gh_w(fd, "GEOHAVGATE authored=organ method=cordic-haversine same_point=" as *u8); gh_wn(fd, zero) 27 gh_w(fd, " nyc_london_m=" as *u8); gh_wn(fd, lon) 28 gh_w(fd, " nyc_sydney_hav_m=" as *u8); gh_wn(fd, syd) 29 gh_w(fd, " nyc_sydney_equi_m=" as *u8); gh_wn(fd, equi) 30 gh_w(fd, " hav_err_m=" as *u8); gh_wn(fd, haverr) 31 gh_w(fd, " equi_err_m=" as *u8); gh_wn(fd, equierr) 32 if ok == 1 { gh_w(fd, " verdict=GREEN\n" as *u8) } else { gh_w(fd, " verdict=RED\n" as *u8) } 33 return 0 34} 35 36func main() -> i64 { 37 let nyc_lat: i64 = 40712800 38 let nyc_lon: i64 = 0 - 74006000 39 let lon_lat: i64 = 51507400 40 let lon_lon: i64 = 0 - 127800 41 let syd_lat: i64 = 0 - 33868800 42 let syd_lon: i64 = 151209300 43 44 let zero: i64 = geo_haversine_m(nyc_lat, nyc_lon, nyc_lat, nyc_lon) // expect 0 45 let d_lon: i64 = geo_haversine_m(nyc_lat, nyc_lon, lon_lat, lon_lon) // ~5,570,000 m 46 let d_syd: i64 = geo_haversine_m(nyc_lat, nyc_lon, syd_lat, syd_lon) // ~15,990,000 m 47 let d_syd_equi: i64 = geo_distance_m(nyc_lat, nyc_lon, syd_lat, syd_lon) // flat-earth baseline 48 49 let true_lon: i64 = 5570000 50 let true_syd: i64 = 15990000 51 let hav_err: i64 = gh_abs(d_syd - true_syd) 52 let equi_err: i64 = gh_abs(d_syd_equi - true_syd) 53 54 var ok: i64 = 1 55 if zero != 0 { ok = 0 } 56 if gh_relnear(d_lon, true_lon, 2, 100) != 1 { ok = 0 } // within 2% 57 if gh_relnear(d_syd, true_syd, 2, 100) != 1 { ok = 0 } // within 2% 58 if hav_err >= equi_err { ok = 0 } // MEASURED exceed: haversine strictly closer 59 60 gh_emit(1, zero, d_lon, d_syd, d_syd_equi, hav_err, equi_err, ok) 61 let lf: i64 = sys_openat_append(GH_LOG, 420) 62 if lf >= 0 { gh_emit(lf, zero, d_lon, d_syd, d_syd_equi, hav_err, equi_err, ok); sys_close(lf) } 63 64 // MIGRATED onto nx_gate_verdict by nx_gate_dry_apply (D001, minimal form): every check 65 // row above is untouched, so the PASS/FAIL vector cannot change; only the hand-rolled 66 // verdict emission is replaced by the ONE shared base class. Proven by nx_gate_migrate verify. 67 let ctr__dry: *i64 = gv_ctr() 68 ctr__dry[0] = ok 69 ctr__dry[1] = 1 70 let rc__dry: i64 = gv_verdict("GEO-HAVERSINE-GATE" as *u8, ctr__dry, "teeth unchanged; verdict emission migrated onto the shared base class" as *u8) 71 sys_exit(rc__dry) 72 return rc__dry 73}