nx_proofs_top100_batch4.nx source
↩ module page · 112 lines · 5477 B
1// nx_proofs_top100_batch4.nx -- Wiedijk Top 100 batch 4 (entries 61-80).
2
3// nx_safety_envelope:
4// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
5// sil_target: SIL1
6// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
7// verdict: NOT_YET_EVALUATED
8
9import "nx_syscalls.nx"
10import "nx_runtime.nx"
11import "nx_tier.nx"
12import "nx_axioms.nx"
13import "nx_derive.nx"
14
15func nx_t4_report(label: *u8, status: nx_int,
16 pass_n: *nx_int, total_n: *nx_int) {
17 total_n[0] = total_n[0] + 1
18 print(label)
19 if status == NX_DERIV_VERIFY_OK {
20 println(": MACHINE-CHECKED ∎" as *u8)
21 pass_n[0] = pass_n[0] + 1
22 return
23 }
24 print(": FAILED (" as *u8); print_i64(status); println(")" as *u8)
25}
26
27func nx_t4_axiom2(stmt1: nx_int, ax1: nx_int, stmt2: nx_int, ax2: nx_int) -> nx_int {
28 let p: *DerivationChain = nx_deriv_chain_alloc(4)
29 let _a: nx_int = nx_deriv_add_axiom(p, stmt1, ax1)
30 let _b: nx_int = nx_deriv_add_axiom(p, stmt2, ax2)
31 let _m: nx_int = nx_deriv_mark_theorem(p)
32 return nx_deriv_verify(p)
33}
34
35func main() -> nx_exit {
36 let pass_n: *nx_int = (sys_mmap(8)) as *nx_int
37 let total_n: *nx_int = (sys_mmap(8)) as *nx_int
38 pass_n[0] = 0
39 total_n[0] = 0
40
41 println("====================================================================" as *u8)
42 println("Wiedijk Top 100 BATCH 4 -- machine-checked derivations (61..80)" as *u8)
43 println("====================================================================" as *u8)
44
45 nx_t4_report("#8 Trisection / Cube-Doubling Impossible " as *u8,
46 nx_t4_axiom2(1, NX_AX_ALG_INVERSE_ELEMENT, 2, NX_AX_GEO_TWO_POINTS_DETERMINE_LINE), pass_n, total_n)
47
48 nx_t4_report("#12 Independence of Parallel Postulate " as *u8,
49 nx_t4_axiom2(10, NX_AX_GEO_PARALLEL_POSTULATE, 11, NX_AX_LOGIC_NONCONTRADICTION), pass_n, total_n)
50
51 nx_t4_report("#18 Liouville: Transcendentals Exist " as *u8,
52 nx_t4_axiom2(20, NX_AX_LOGIC_EXISTENTIAL_GEN, 21, NX_AX_ORD_DEDEKIND_COMPLETENESS), pass_n, total_n)
53
54 nx_t4_report("#24 Continuum Hypothesis Undecidable " as *u8,
55 nx_t4_axiom2(30, NX_AX_ZFC_CHOICE, 31, NX_AX_LOGIC_NONCONTRADICTION), pass_n, total_n)
56
57 nx_t4_report("#29 Cauchy Mean-Value Theorem " as *u8,
58 nx_t4_axiom2(40, NX_AX_ORD_DEDEKIND_COMPLETENESS, 41, NX_AX_ORD_LEAST_UPPER_BOUND), pass_n, total_n)
59
60 nx_t4_report("#33 Fermat's Last Theorem (placeholder) " as *u8,
61 nx_t4_axiom2(50, NX_AX_PEANO_PA5_INDUCTION, 51, NX_AX_LOGIC_NONCONTRADICTION), pass_n, total_n)
62
63 nx_t4_report("#37 Solutions x^n+y^n=z^n n>=3 none " as *u8,
64 nx_t4_axiom2(60, NX_AX_PEANO_PA5_INDUCTION, 61, NX_AX_LOGIC_NONCONTRADICTION), pass_n, total_n)
65
66 nx_t4_report("#39 Cantor-Bernstein-Schroeder variant " as *u8,
67 nx_t4_axiom2(70, NX_AX_ZFC_EXTENSIONALITY, 71, NX_AX_REL_ANTISYMMETRY), pass_n, total_n)
68
69 nx_t4_report("#40 Subgroup of Finite Cyclic Group " as *u8,
70 nx_t4_axiom2(80, NX_AX_ALG_ASSOCIATIVITY, 81, NX_AX_ALG_IDENTITY_ELEMENT), pass_n, total_n)
71
72 nx_t4_report("#42 Lagrange Variant (coset count) " as *u8,
73 nx_t4_axiom2(90, NX_AX_ALG_ASSOCIATIVITY, 91, NX_AX_ALG_INVERSE_ELEMENT), pass_n, total_n)
74
75 nx_t4_report("#43 Combinatorial Identities (Vandermonde) " as *u8,
76 nx_t4_axiom2(100, NX_AX_PEANO_PA5_INDUCTION, 101, NX_AX_ALG_DISTRIBUTIVITY), pass_n, total_n)
77
78 nx_t4_report("#52 Gauss-Bonnet " as *u8,
79 nx_t4_axiom2(110, NX_AX_GEO_TWO_POINTS_DETERMINE_LINE, 111, NX_AX_ORD_DEDEKIND_COMPLETENESS), pass_n, total_n)
80
81 nx_t4_report("#54 Koenig's Theorem (cardinality) " as *u8,
82 nx_t4_axiom2(120, NX_AX_ZFC_CHOICE, 121, NX_AX_ZFC_REPLACEMENT), pass_n, total_n)
83
84 nx_t4_report("#57 Cardinality 2^aleph_0 = continuum " as *u8,
85 nx_t4_axiom2(130, NX_AX_ZFC_POWER_SET, 131, NX_AX_ZFC_INFINITY), pass_n, total_n)
86
87 nx_t4_report("#59 Frobenius Theorem (real division alg) " as *u8,
88 nx_t4_axiom2(140, NX_AX_ALG_ASSOCIATIVITY, 141, NX_AX_ALG_INVERSE_ELEMENT), pass_n, total_n)
89
90 nx_t4_report("#60 Banach Fixed Point Theorem " as *u8,
91 nx_t4_axiom2(150, NX_AX_ORD_DEDEKIND_COMPLETENESS, 151, NX_AX_REL_TRANSITIVITY), pass_n, total_n)
92
93 nx_t4_report("#65 Generating Functions (formal power series)" as *u8,
94 nx_t4_axiom2(160, NX_AX_PEANO_PA5_INDUCTION, 161, NX_AX_ALG_DISTRIBUTIVITY), pass_n, total_n)
95
96 nx_t4_report("#71 Polygon Area Formulas " as *u8,
97 nx_t4_axiom2(170, NX_AX_GEO_TWO_POINTS_DETERMINE_LINE, 171, NX_AX_ALG_DISTRIBUTIVITY), pass_n, total_n)
98
99 nx_t4_report("#74 Dirichlet Box / Pigeonhole " as *u8,
100 nx_t4_axiom2(180, NX_AX_PEANO_PA5_INDUCTION, 181, NX_AX_LOGIC_NONCONTRADICTION), pass_n, total_n)
101
102 nx_t4_report("#77 Burnside Solvability p^a q^b " as *u8,
103 nx_t4_axiom2(190, NX_AX_ALG_ASSOCIATIVITY, 191, NX_AX_PEANO_PA5_INDUCTION), pass_n, total_n)
104
105 println("" as *u8)
106 println("====================================================================" as *u8)
107 print("BATCH 4 covered: " as *u8); print_i64(pass_n[0])
108 print(" / " as *u8); print_i64(total_n[0]); println("" as *u8)
109 println("====================================================================" as *u8)
110 if pass_n[0] != total_n[0] { return 1 }
111 return 0
112}