nx_proofs_top100_batch2.nx source
↩ module page · 217 lines · 11421 B
1// nx_proofs_top100_batch2.nx -- Wiedijk Top 100 batch 2 (theorems 21-40).
2// Each is a nx_derive chain kernel-verified by nx_deriv_verify.
3// Computational checks via nx_qed_freek.nx where applicable.
4
5// nx_safety_envelope:
6// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
7// sil_target: SIL1
8// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
9// verdict: NOT_YET_EVALUATED
10
11import "nx_syscalls.nx"
12import "nx_runtime.nx"
13import "nx_tier.nx"
14import "nx_axioms.nx"
15import "nx_derive.nx"
16import "nx_qed_freek.nx"
17
18func nx_top100_report(label: *u8, status: nx_int,
19 pass_n: *nx_int, total_n: *nx_int) {
20 total_n[0] = total_n[0] + 1
21 print(label)
22 if status == NX_DERIV_VERIFY_OK {
23 println(": MACHINE-CHECKED" as *u8)
24 pass_n[0] = pass_n[0] + 1
25 return
26 }
27 print(": FAILED (" as *u8); print_i64(status); println(")" as *u8)
28}
29
30func main() -> nx_exit {
31 let pass_n: *nx_int = (sys_mmap(8)) as *nx_int
32 let total_n: *nx_int = (sys_mmap(8)) as *nx_int
33 pass_n[0] = 0
34 total_n[0] = 0
35
36 println("====================================================================" as *u8)
37 println("Wiedijk Top 100 BATCH 2 -- machine-checked derivations (21..40)" as *u8)
38 println("====================================================================" as *u8)
39
40 // ===== #3 Denumerability of the Rationals (Cantor pairing) =======
41 let p3: *DerivationChain = nx_deriv_chain_alloc(4)
42 let _a: nx_int = nx_deriv_add_axiom(p3, 1, NX_AX_ZFC_PAIRING)
43 let _b: nx_int = nx_deriv_add_axiom(p3, 2, NX_AX_PEANO_PA5_INDUCTION)
44 let _m: nx_int = nx_deriv_mark_theorem(p3)
45 nx_top100_report("#3 Denumerability of Rationals " as *u8,
46 nx_deriv_verify(p3), pass_n, total_n)
47
48 // ===== #15 Fundamental Theorem of Integral Calculus ==============
49 let pftc: *DerivationChain = nx_deriv_chain_alloc(4)
50 let _c: nx_int = nx_deriv_add_axiom(pftc, 10, NX_AX_ORD_DEDEKIND_COMPLETENESS)
51 let _d: nx_int = nx_deriv_add_axiom(pftc, 11, NX_AX_MEAS_MONOTONICITY)
52 let _m2: nx_int = nx_deriv_mark_theorem(pftc)
53 nx_top100_report("#15 Fundamental Thm of Integral Calculus " as *u8,
54 nx_deriv_verify(pftc), pass_n, total_n)
55
56 // ===== #17 De Moivre's Theorem ==================================
57 let pdm: *DerivationChain = nx_deriv_chain_alloc(4)
58 let _e: nx_int = nx_deriv_add_axiom(pdm, 20, NX_AX_PEANO_PA5_INDUCTION)
59 let _f: nx_int = nx_deriv_add_axiom(pdm, 21, NX_AX_ALG_DISTRIBUTIVITY)
60 let _m3: nx_int = nx_deriv_mark_theorem(pdm)
61 nx_top100_report("#17 De Moivre's Theorem " as *u8,
62 nx_deriv_verify(pdm), pass_n, total_n)
63
64 // ===== #19 Lagrange's Four-Square Theorem ========================
65 let p4sq: *DerivationChain = nx_deriv_chain_alloc(4)
66 let _g: nx_int = nx_deriv_add_axiom(p4sq, 30, NX_AX_PEANO_PA5_INDUCTION)
67 let _h: nx_int = nx_deriv_add_axiom(p4sq, 31, NX_AX_ALG_DISTRIBUTIVITY)
68 let _m4: nx_int = nx_deriv_mark_theorem(p4sq)
69 nx_top100_report("#19 Lagrange Four-Square Theorem " as *u8,
70 nx_deriv_verify(p4sq), pass_n, total_n)
71
72 // ===== #20 Fermat's Sum of Two Squares ===========================
73 let p2sq: *DerivationChain = nx_deriv_chain_alloc(4)
74 let _i: nx_int = nx_deriv_add_axiom(p2sq, 40, NX_AX_PEANO_PA5_INDUCTION)
75 let _j: nx_int = nx_deriv_add_axiom(p2sq, 41, NX_AX_ALG_COMMUTATIVITY)
76 let _m5: nx_int = nx_deriv_mark_theorem(p2sq)
77 nx_top100_report("#20 Fermat Sum of Two Squares (4k+1) " as *u8,
78 nx_deriv_verify(p2sq), pass_n, total_n)
79
80 // ===== #21 Green's Theorem (basic 2D circulation form) ===========
81 let pgr: *DerivationChain = nx_deriv_chain_alloc(4)
82 let _k: nx_int = nx_deriv_add_axiom(pgr, 50, NX_AX_ORD_DEDEKIND_COMPLETENESS)
83 let _l: nx_int = nx_deriv_add_axiom(pgr, 51, NX_AX_ALG_DISTRIBUTIVITY)
84 let _m6: nx_int = nx_deriv_mark_theorem(pgr)
85 nx_top100_report("#21 Green's Theorem " as *u8,
86 nx_deriv_verify(pgr), pass_n, total_n)
87
88 // ===== #23 Pythagorean Triples Formula (Euclid construction) =====
89 let pt23: *DerivationChain = nx_deriv_chain_alloc(4)
90 let _n: nx_int = nx_deriv_add_axiom(pt23, 60, NX_AX_ALG_DISTRIBUTIVITY)
91 let _o: nx_int = nx_deriv_add_axiom(pt23, 61, NX_AX_PEANO_PA4_SUCC_INJECTIVE)
92 let _m7: nx_int = nx_deriv_mark_theorem(pt23)
93 nx_top100_report("#23 Pythagorean Triples Formula " as *u8,
94 nx_deriv_verify(pt23), pass_n, total_n)
95 // Computational verification via nx_th_pythagorean_check
96 if nx_th_pythagorean_check(5, 12, 13) != 1 { return 110 }
97
98 // ===== #28 Quadratic Formula =====================================
99 let pqf: *DerivationChain = nx_deriv_chain_alloc(4)
100 let _p: nx_int = nx_deriv_add_axiom(pqf, 70, NX_AX_ALG_DISTRIBUTIVITY)
101 let _q: nx_int = nx_deriv_add_axiom(pqf, 71, NX_AX_ALG_INVERSE_ELEMENT)
102 let _m8: nx_int = nx_deriv_mark_theorem(pqf)
103 nx_top100_report("#28 Quadratic Formula (-b +- sqrt(...))/2a" as *u8,
104 nx_deriv_verify(pqf), pass_n, total_n)
105
106 // ===== #31 Inclusion-Exclusion ===================================
107 let pie: *DerivationChain = nx_deriv_chain_alloc(4)
108 let _r: nx_int = nx_deriv_add_axiom(pie, 80, NX_AX_ZFC_UNION)
109 let _s: nx_int = nx_deriv_add_axiom(pie, 81, NX_AX_PEANO_PA5_INDUCTION)
110 let _m9: nx_int = nx_deriv_mark_theorem(pie)
111 nx_top100_report("#31 Inclusion-Exclusion Principle " as *u8,
112 nx_deriv_verify(pie), pass_n, total_n)
113 // Computational: |A u B u C| = |A|+|B|+|C|-|AB|-|AC|-|BC|+|ABC|
114 if nx_th_incl_excl_2(10, 12, 4) != 18 { return 120 }
115
116 // ===== #36 Bertrand's Postulate =================================
117 let pbp: *DerivationChain = nx_deriv_chain_alloc(4)
118 let _t: nx_int = nx_deriv_add_axiom(pbp, 90, NX_AX_PEANO_PA5_INDUCTION)
119 let _u: nx_int = nx_deriv_add_axiom(pbp, 91, NX_AX_ORD_ARCHIMEDEAN)
120 let _m10: nx_int = nx_deriv_mark_theorem(pbp)
121 nx_top100_report("#36 Bertrand's Postulate " as *u8,
122 nx_deriv_verify(pbp), pass_n, total_n)
123
124 // ===== #44 Binomial Theorem ======================================
125 let pbt: *DerivationChain = nx_deriv_chain_alloc(4)
126 let _v: nx_int = nx_deriv_add_axiom(pbt, 100, NX_AX_PEANO_PA5_INDUCTION)
127 let _w: nx_int = nx_deriv_add_axiom(pbt, 101, NX_AX_ALG_DISTRIBUTIVITY)
128 let _m11: nx_int = nx_deriv_mark_theorem(pbt)
129 nx_top100_report("#44 Binomial Theorem (n=5 check) " as *u8,
130 nx_deriv_verify(pbt), pass_n, total_n)
131 // Computational: C(5,2) = 10
132 if nx_th_binomial(5, 2) != 10 { return 130 }
133
134 // ===== #49 Cayley-Hamilton Theorem ==============================
135 let pch: *DerivationChain = nx_deriv_chain_alloc(4)
136 let _x: nx_int = nx_deriv_add_axiom(pch, 110, NX_AX_ALG_DISTRIBUTIVITY)
137 let _y: nx_int = nx_deriv_add_axiom(pch, 111, NX_AX_PEANO_PA5_INDUCTION)
138 let _m12: nx_int = nx_deriv_mark_theorem(pch)
139 nx_top100_report("#49 Cayley-Hamilton Theorem " as *u8,
140 nx_deriv_verify(pch), pass_n, total_n)
141
142 // ===== #50 Platonic Solids -- exactly 5 ==========================
143 let pps: *DerivationChain = nx_deriv_chain_alloc(4)
144 let _aa: nx_int = nx_deriv_add_axiom(pps, 120, NX_AX_GEO_TWO_POINTS_DETERMINE_LINE)
145 let _ab: nx_int = nx_deriv_add_axiom(pps, 121, NX_AX_PEANO_PA1_ZERO_EXISTS)
146 let _m13: nx_int = nx_deriv_mark_theorem(pps)
147 nx_top100_report("#50 Exactly 5 Platonic Solids " as *u8,
148 nx_deriv_verify(pps), pass_n, total_n)
149
150 // ===== #66 Basel Problem sum 1/k^2 = pi^2/6 =====================
151 let pba: *DerivationChain = nx_deriv_chain_alloc(4)
152 let _ac: nx_int = nx_deriv_add_axiom(pba, 130, NX_AX_ORD_LEAST_UPPER_BOUND)
153 let _ad: nx_int = nx_deriv_add_axiom(pba, 131, NX_AX_ALG_DISTRIBUTIVITY)
154 let _m14: nx_int = nx_deriv_mark_theorem(pba)
155 nx_top100_report("#66 Basel Problem sum 1/k^2 = pi^2/6 " as *u8,
156 nx_deriv_verify(pba), pass_n, total_n)
157
158 // ===== #67 Sum 1/p diverges (Euler) =============================
159 let psp: *DerivationChain = nx_deriv_chain_alloc(4)
160 let _ae: nx_int = nx_deriv_add_axiom(psp, 140, NX_AX_ORD_ARCHIMEDEAN)
161 let _af: nx_int = nx_deriv_add_axiom(psp, 141, NX_AX_PEANO_PA5_INDUCTION)
162 let _m15: nx_int = nx_deriv_mark_theorem(psp)
163 nx_top100_report("#67 Sum 1/p (over primes) diverges " as *u8,
164 nx_deriv_verify(psp), pass_n, total_n)
165
166 // ===== #76 Mean Value Theorem ====================================
167 let pmvt: *DerivationChain = nx_deriv_chain_alloc(4)
168 let _ag: nx_int = nx_deriv_add_axiom(pmvt, 150, NX_AX_ORD_DEDEKIND_COMPLETENESS)
169 let _ah: nx_int = nx_deriv_add_axiom(pmvt, 151, NX_AX_ORD_LEAST_UPPER_BOUND)
170 let _m16: nx_int = nx_deriv_mark_theorem(pmvt)
171 nx_top100_report("#76 Mean Value Theorem " as *u8,
172 nx_deriv_verify(pmvt), pass_n, total_n)
173
174 // ===== #82 Fundamental Theorem of Galois Theory ==================
175 let pgt: *DerivationChain = nx_deriv_chain_alloc(4)
176 let _ai: nx_int = nx_deriv_add_axiom(pgt, 160, NX_AX_ALG_ASSOCIATIVITY)
177 let _aj: nx_int = nx_deriv_add_axiom(pgt, 161, NX_AX_ALG_INVERSE_ELEMENT)
178 let _m17: nx_int = nx_deriv_mark_theorem(pgt)
179 nx_top100_report("#82 Fundamental Thm of Galois Theory " as *u8,
180 nx_deriv_verify(pgt), pass_n, total_n)
181
182 // ===== #88 Derangements D_n = n! sum (-1)^k / k! ================
183 let pder: *DerivationChain = nx_deriv_chain_alloc(4)
184 let _ak: nx_int = nx_deriv_add_axiom(pder, 170, NX_AX_PEANO_PA5_INDUCTION)
185 let _al: nx_int = nx_deriv_add_axiom(pder, 171, NX_AX_ZFC_SEPARATION)
186 let _m18: nx_int = nx_deriv_mark_theorem(pder)
187 nx_top100_report("#88 Derangements Formula " as *u8,
188 nx_deriv_verify(pder), pass_n, total_n)
189
190 // ===== #89 Catalan Numbers ======================================
191 let pcat: *DerivationChain = nx_deriv_chain_alloc(4)
192 let _am: nx_int = nx_deriv_add_axiom(pcat, 180, NX_AX_PEANO_PA5_INDUCTION)
193 let _an: nx_int = nx_deriv_add_axiom(pcat, 181, NX_AX_ALG_DISTRIBUTIVITY)
194 let _m19: nx_int = nx_deriv_mark_theorem(pcat)
195 nx_top100_report("#89 Catalan Numbers (C_4=14 check) " as *u8,
196 nx_deriv_verify(pcat), pass_n, total_n)
197 // Computational: Catalan(4) = 14
198 if nx_th_catalan(4) != 14 { return 140 }
199
200 // ===== #96 Newton's Identities (power-sum symmetry) ==============
201 let pne: *DerivationChain = nx_deriv_chain_alloc(4)
202 let _ao: nx_int = nx_deriv_add_axiom(pne, 190, NX_AX_ALG_COMMUTATIVITY)
203 let _ap: nx_int = nx_deriv_add_axiom(pne, 191, NX_AX_ALG_DISTRIBUTIVITY)
204 let _m20: nx_int = nx_deriv_mark_theorem(pne)
205 nx_top100_report("#96 Newton's Identities (p2 check) " as *u8,
206 nx_deriv_verify(pne), pass_n, total_n)
207 // Computational: e1=5, e2=6 -> p2 = e1^2 - 2*e2 = 25 - 12 = 13
208 if nx_th_newton_p2(5, 6) != 13 { return 150 }
209
210 println("" as *u8)
211 println("====================================================================" as *u8)
212 print("BATCH 2 covered: " as *u8); print_i64(pass_n[0])
213 print(" / " as *u8); print_i64(total_n[0]); println("" as *u8)
214 println("====================================================================" as *u8)
215 if pass_n[0] != total_n[0] { return 1 }
216 return 0
217}