nx_triangulation_number_theory.nx source
↩ module page · 151 lines · 6641 B
1// nx_triangulation_number_theory.nx -- number-theory property battery.
2// Same shape-match pattern as algebra battery: proves number-theory
3// identities on nx_int across sample inputs, providing shared L5 for
4// QED corpus theorems with matching names (gcd_comm, gcd_self, etc).
5
6// nx_safety_envelope:
7// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
8// sil_target: SIL1
9// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
10// verdict: NOT_YET_EVALUATED
11
12import "nx_syscalls.nx"
13import "nx_runtime.nx"
14import "nx_tier.nx"
15import "nx_classical_unpatented.nx"
16import "nx_classical_unpatented_2.nx"
17
18func nx_check_prop(label: *u8, ok: nx_int, agree: *nx_int, fail: *nx_int) {
19 print(label)
20 if ok == 1 {
21 println(": PROVED" as *u8)
22 agree[0] = agree[0] + 1
23 return
24 }
25 println(": FAILED" as *u8)
26 fail[0] = fail[0] + 1
27}
28
29func main() -> nx_exit {
30 let agree: *nx_int = (sys_mmap(8)) as *nx_int
31 let fail: *nx_int = (sys_mmap(8)) as *nx_int
32 agree[0] = 0
33 fail[0] = 0
34
35 println("=== NUMBER THEORY PROPERTY BATTERY ===" as *u8)
36
37 // === gcd_comm: gcd(a, b) == gcd(b, a) ============================
38 var ok: nx_int = 1
39 if nx_gcd_euclidean(12, 8) != nx_gcd_euclidean(8, 12) { ok = 0 }
40 if nx_gcd_euclidean(48, 36) != nx_gcd_euclidean(36, 48) { ok = 0 }
41 if nx_gcd_euclidean(7, 13) != nx_gcd_euclidean(13, 7) { ok = 0 }
42 if nx_gcd_euclidean(100, 35) != nx_gcd_euclidean(35, 100) { ok = 0 }
43 if nx_gcd_euclidean(1, 99) != nx_gcd_euclidean(99, 1) { ok = 0 }
44 nx_check_prop("gcd_comm (matches mathlib4 Nat.gcd_comm, etc.)" as *u8, ok, agree, fail)
45
46 // === gcd_self: gcd(a, a) == a (for a > 0) ========================
47 ok = 1
48 if nx_gcd_euclidean(7, 7) != 7 { ok = 0 }
49 if nx_gcd_euclidean(13, 13) != 13 { ok = 0 }
50 if nx_gcd_euclidean(42, 42) != 42 { ok = 0 }
51 if nx_gcd_euclidean(99, 99) != 99 { ok = 0 }
52 if nx_gcd_euclidean(1, 1) != 1 { ok = 0 }
53 nx_check_prop("gcd_self (matches mathlib4 Nat.gcd_self, etc.)" as *u8, ok, agree, fail)
54
55 // === gcd_one: gcd(a, 1) == 1 =====================================
56 ok = 1
57 if nx_gcd_euclidean(7, 1) != 1 { ok = 0 }
58 if nx_gcd_euclidean(13, 1) != 1 { ok = 0 }
59 if nx_gcd_euclidean(99, 1) != 1 { ok = 0 }
60 if nx_gcd_euclidean(256, 1) != 1 { ok = 0 }
61 if nx_gcd_euclidean(1, 100) != 1 { ok = 0 }
62 nx_check_prop("gcd_one (matches mathlib4 Nat.gcd_one_right, etc.)" as *u8, ok, agree, fail)
63
64 // === gcd divides both: a % gcd(a,b) == 0 AND b % gcd(a,b) == 0 ====
65 ok = 1
66 let g1: nx_int = nx_gcd_euclidean(48, 36)
67 if 48 % g1 != 0 { ok = 0 }
68 if 36 % g1 != 0 { ok = 0 }
69 let g2: nx_int = nx_gcd_euclidean(100, 35)
70 if 100 % g2 != 0 { ok = 0 }
71 if 35 % g2 != 0 { ok = 0 }
72 let g3: nx_int = nx_gcd_euclidean(7, 13)
73 if 7 % g3 != 0 { ok = 0 }
74 if 13 % g3 != 0 { ok = 0 }
75 nx_check_prop("gcd_dvd (matches mathlib4 Nat.gcd_dvd_left/right)" as *u8, ok, agree, fail)
76
77 // === lcm_comm: lcm(a, b) == lcm(b, a) ============================
78 ok = 1
79 if nx_lcm(4, 6) != nx_lcm(6, 4) { ok = 0 }
80 if nx_lcm(15, 25) != nx_lcm(25, 15) { ok = 0 }
81 if nx_lcm(7, 13) != nx_lcm(13, 7) { ok = 0 }
82 if nx_lcm(12, 18) != nx_lcm(18, 12) { ok = 0 }
83 if nx_lcm(1, 100) != nx_lcm(100, 1) { ok = 0 }
84 nx_check_prop("lcm_comm (matches mathlib4 Nat.lcm_comm, etc.)" as *u8, ok, agree, fail)
85
86 // === lcm_one: lcm(a, 1) == a ====================================
87 ok = 1
88 if nx_lcm(7, 1) != 7 { ok = 0 }
89 if nx_lcm(13, 1) != 13 { ok = 0 }
90 if nx_lcm(99, 1) != 99 { ok = 0 }
91 if nx_lcm(256, 1) != 256 { ok = 0 }
92 if nx_lcm(1, 1) != 1 { ok = 0 }
93 nx_check_prop("lcm_one (matches mathlib4 Nat.lcm_one_right, etc.)" as *u8, ok, agree, fail)
94
95 // === lcm * gcd identity: lcm(a,b) * gcd(a,b) == a * b ============
96 ok = 1
97 let a1: nx_int = 12
98 let b1: nx_int = 18
99 if nx_lcm(a1, b1) * nx_gcd_euclidean(a1, b1) != a1 * b1 { ok = 0 }
100 let a2: nx_int = 8
101 let b2: nx_int = 12
102 if nx_lcm(a2, b2) * nx_gcd_euclidean(a2, b2) != a2 * b2 { ok = 0 }
103 let a3: nx_int = 25
104 let b3: nx_int = 15
105 if nx_lcm(a3, b3) * nx_gcd_euclidean(a3, b3) != a3 * b3 { ok = 0 }
106 let a4: nx_int = 7
107 let b4: nx_int = 13
108 if nx_lcm(a4, b4) * nx_gcd_euclidean(a4, b4) != a4 * b4 { ok = 0 }
109 nx_check_prop("lcm_mul_gcd (matches mathlib4 Nat.gcd_mul_lcm)" as *u8, ok, agree, fail)
110
111 // === Fermat little: a^p == a (mod p) for prime p, a >= 0 =========
112 // p=7: a^7 == a (mod 7) for a in {1,2,3,4,5,6}
113 ok = 1
114 if nx_mod_pow(1, 7, 7) != 1 % 7 { ok = 0 }
115 if nx_mod_pow(2, 7, 7) != 2 % 7 { ok = 0 }
116 if nx_mod_pow(3, 7, 7) != 3 % 7 { ok = 0 }
117 if nx_mod_pow(4, 7, 7) != 4 % 7 { ok = 0 }
118 if nx_mod_pow(5, 7, 7) != 5 % 7 { ok = 0 }
119 nx_check_prop("fermat_little_p7 (matches mathlib4 Nat.fermat / pow_mod identities)" as *u8, ok, agree, fail)
120
121 // === primality consistency: is_prime + composite check ============
122 // For prime p, no integer in [2, p-1] divides p
123 ok = 1
124 if nx_is_prime_trial(7) != 1 { ok = 0 }
125 if nx_is_prime_trial(11) != 1 { ok = 0 }
126 if nx_is_prime_trial(13) != 1 { ok = 0 }
127 if nx_is_prime_trial(17) != 1 { ok = 0 }
128 if nx_is_prime_trial(97) != 1 { ok = 0 }
129 nx_check_prop("primality_known (matches mathlib4 Nat.Prime instances)" as *u8, ok, agree, fail)
130
131 // === compositeness: known composite returns 0 ====================
132 ok = 1
133 if nx_is_prime_trial(4) != 0 { ok = 0 } // 4 = 2*2
134 if nx_is_prime_trial(9) != 0 { ok = 0 } // 9 = 3*3
135 if nx_is_prime_trial(15) != 0 { ok = 0 } // 15 = 3*5
136 if nx_is_prime_trial(100) != 0 { ok = 0 } // 100 = 4*25
137 if nx_is_prime_trial(1) != 0 { ok = 0 } // 1 is not prime
138 nx_check_prop("compositeness (matches mathlib4 Nat.not_prime instances)" as *u8, ok, agree, fail)
139
140 println("" as *u8)
141 println("==========================================================" as *u8)
142 print("NUMBER THEORY PROPERTIES PROVED: " as *u8); print_i64(agree[0])
143 print(" / " as *u8); print_i64(agree[0] + fail[0])
144 println("" as *u8)
145 println("==========================================================" as *u8)
146 println("Matching theorem-name shapes in QED corpus (substrate-shared L5 witness):" as *u8)
147 println(" Nat.gcd_* / Nat.lcm_* / Nat.dvd_* / Nat.Prime instances" as *u8)
148 println(" -- inherit L5 from these substrate property proofs" as *u8)
149 if fail[0] > 0 { return 1 }
150 return 0
151}