nx_theorem_card.nx source
↩ module page · 268 lines · 9942 B
1// nx_theorem_card.nx -- substrate-enforced TheoremCard per
2// S_CLASS_MATH_DOCTRINE.
3//
4// Every theorem the substrate exposes must populate a TheoremCard on
5// all 8 axes. Production-path dispatch consults the card via
6// nx_card_check_or_refuse; wobbly cards (any axis unproven) halt.
7//
8// genealogy_id: nishi_substrate_2026
9// lineage_id: formal_proof_theory + benchmarking_discipline
10// axioms: NX_AX_LOGIC_NONCONTRADICTION (no claim + counter-claim)
11
12// nx_safety_envelope:
13// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
14// sil_target: SIL1
15// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
16// verdict: NOT_YET_EVALUATED
17
18import "syscalls.nx"
19import "nx_axioms.nx"
20const NX_MAGIC_125000000: i64 = 125000000
21const NX_MAGIC_1000000000: i64 = 1000000000
22
23// ===== sealed enums ===================================================
24
25const NX_XCHECK_NO_REF: i64 = 0
26const NX_XCHECK_MATCHES_INDEPENDENT: i64 = 1
27const NX_XCHECK_DIFFERS_INVESTIGATING: i64 = 2
28const NX_XCHECK_DIFFERS_WE_RIGHT: i64 = 3
29const NX_XCHECK_DIFFERS_WE_WRONG: i64 = 4
30
31const NX_DETERMINISM_BIT_IDENTICAL: i64 = 0
32const NX_DETERMINISM_WITHIN_TOLERANCE: i64 = 1
33const NX_DETERMINISM_NONDETERMINISTIC: i64 = 2
34
35const NX_FOUNDATION_SUFFICIENT: i64 = 0 // bits up; full chain
36const NX_FOUNDATION_PARTIAL: i64 = 1 // missing some link
37const NX_FOUNDATION_TBD: i64 = 2 // not yet audited
38
39const NX_PERF_NO_BASELINE: i64 = 0 // incumbent N/A
40const NX_PERF_WINS: i64 = 1 // ours ≤ theirs
41const NX_PERF_LOSES: i64 = 2 // ours > theirs by ≥10%
42const NX_PERF_TIES: i64 = 3 // within 10%
43
44// ===== the card =======================================================
45
46struct TheoremCard {
47 theorem_id: i64,
48 name: *u8,
49 n_genealogy: i64,
50 n_lineage: i64,
51 lineage_axiom_codes: *i64, // array of NX_AX_*
52 perf_vs_mathematica_status: i64,
53 perf_vs_numpy_status: i64,
54 perf_vs_julia_status: i64,
55 perf_vs_sage_status: i64,
56 perf_vs_matlab_status: i64,
57 perf_vs_r_status: i64,
58 smoke_pass: i64, // 1 if green
59 cross_check_status: i64,
60 determinism_status: i64,
61 foundation_reach: i64,
62 wobbly_flag: i64, // 0 = ok, 1 = NOT READY
63 completeness_score_ppb: i64, // 0..1e9 = axes proven
64}
65
66const NX_CARD_BYTES: i64 = 144
67
68func nx_card_alloc() -> *TheoremCard {
69 let raw: *u8 = sys_mmap(NX_CARD_BYTES)
70 let c: *TheoremCard = raw as *TheoremCard
71 c.theorem_id = 0
72 c.name = (0 as *u8)
73 c.n_genealogy = 0
74 c.n_lineage = 0
75 c.lineage_axiom_codes = (0 as *i64)
76 c.perf_vs_mathematica_status = NX_PERF_NO_BASELINE
77 c.perf_vs_numpy_status = NX_PERF_NO_BASELINE
78 c.perf_vs_julia_status = NX_PERF_NO_BASELINE
79 c.perf_vs_sage_status = NX_PERF_NO_BASELINE
80 c.perf_vs_matlab_status = NX_PERF_NO_BASELINE
81 c.perf_vs_r_status = NX_PERF_NO_BASELINE
82 c.smoke_pass = 0
83 c.cross_check_status = NX_XCHECK_NO_REF
84 c.determinism_status = NX_DETERMINISM_NONDETERMINISTIC
85 c.foundation_reach = NX_FOUNDATION_TBD
86 c.wobbly_flag = 1 // default = NOT READY
87 c.completeness_score_ppb = 0
88 return c
89}
90
91// Compute completeness: count axes that are non-default. Eight axes
92// total; each filled axis adds 1/8 ~ 125_000_000 ppb.
93func nx_card_compute_completeness(c: *TheoremCard) -> i64 {
94 var score: i64 = 0
95 if c.n_genealogy > 0 { score = score + NX_MAGIC_125000000 } // axis 1
96 if c.n_lineage > 0 { score = score + NX_MAGIC_125000000 } // axis 2
97 // Axis 3: at least one perf benchmark non-default.
98 var perf_any: i64 = 0
99 if c.perf_vs_mathematica_status != NX_PERF_NO_BASELINE { perf_any = 1 }
100 if c.perf_vs_numpy_status != NX_PERF_NO_BASELINE { perf_any = 1 }
101 if c.perf_vs_julia_status != NX_PERF_NO_BASELINE { perf_any = 1 }
102 if c.perf_vs_sage_status != NX_PERF_NO_BASELINE { perf_any = 1 }
103 if c.perf_vs_matlab_status != NX_PERF_NO_BASELINE { perf_any = 1 }
104 if c.perf_vs_r_status != NX_PERF_NO_BASELINE { perf_any = 1 }
105 if perf_any == 1 { score = score + NX_MAGIC_125000000 }
106 if c.smoke_pass == 1 { score = score + NX_MAGIC_125000000 } // axis 4
107 if c.cross_check_status != NX_XCHECK_NO_REF { score = score + NX_MAGIC_125000000 } // axis 5
108 if c.determinism_status == NX_DETERMINISM_BIT_IDENTICAL { score = score + NX_MAGIC_125000000 } // axis 6
109 // Axis 7: no-hallucination -- proxied by n_lineage > 0 AND foundation != TBD
110 if c.foundation_reach != NX_FOUNDATION_TBD {
111 if c.n_lineage > 0 { score = score + NX_MAGIC_125000000 }
112 }
113 // Axis 8: foundation_reach == SUFFICIENT
114 if c.foundation_reach == NX_FOUNDATION_SUFFICIENT { score = score + NX_MAGIC_125000000 }
115 c.completeness_score_ppb = score
116 if score >= NX_MAGIC_1000000000 { c.wobbly_flag = 0 }
117 if score < NX_MAGIC_1000000000 { c.wobbly_flag = 1 }
118 return score
119}
120
121// Card builder convenience: declare a card with sealed axiom lineage.
122func nx_card_set_lineage(c: *TheoremCard, codes: *i64, n: i64) -> i64 {
123 c.lineage_axiom_codes = codes
124 c.n_lineage = n
125 return 0
126}
127
128func nx_card_set_genealogy_count(c: *TheoremCard, n: i64) -> i64 {
129 c.n_genealogy = n
130 return 0
131}
132
133// ===== refusal primitive ===============================================
134//
135// Production callers gate dispatch on this; refusing if card is wobbly.
136// Returns 1 if OK, 0 if refused.
137
138func nx_card_check_or_refuse(c: *TheoremCard) -> i64 {
139 if c.wobbly_flag == 1 {
140 sys_write(2, "card: theorem WOBBLY -- refusing dispatch\n" as *u8, 42)
141 return 0
142 }
143 return 1
144}
145
146// ===== ledger emission =================================================
147//
148// Emits a JSON-line per card to fd_ledger. Schema:
149// {"theorem_id":N, "name":"...", "n_genealogy":N, "n_lineage":N,
150// "perf":{...}, "smoke":N, "xcheck":N, "det":N, "found":N,
151// "wobbly":N, "score_ppb":N}
152
153func cd_putc(fd: i64, c: i64) -> i64 {
154 let buf: *u8 = sys_mmap(1)
155 buf[0] = c & 0xFF
156 sys_write(fd, buf, 1)
157 return 0
158}
159
160func cd_str(fd: i64, s: *u8, len: i64) -> i64 {
161 sys_write(fd, s, len)
162 return 0
163}
164
165func cd_strz(fd: i64, s: *u8) -> i64 {
166 var i: i64 = 0
167 while s[i] != 0 { i = i + 1 }
168 sys_write(fd, s, i)
169 return i
170}
171
172func cd_i64(fd: i64, n: i64) -> i64 {
173 if n < 0 {
174 cd_putc(fd, 45)
175 return cd_i64(fd, -n)
176 }
177 if n == 0 {
178 cd_putc(fd, 48)
179 return 0
180 }
181 let digits: *u8 = sys_mmap(32)
182 var d: i64 = 0
183 var v: i64 = n
184 while v > 0 {
185 digits[d] = (v % 10) + 48
186 v = v / 10
187 d = d + 1
188 }
189 while d > 0 {
190 d = d - 1
191 cd_putc(fd, digits[d])
192 }
193 return 0
194}
195
196func nx_card_emit(fd: i64, c: *TheoremCard) -> i64 {
197 cd_str(fd, "{\"theorem_id\":", 14)
198 cd_i64(fd, c.theorem_id)
199 cd_str(fd, ",\"name\":\"", 9)
200 if c.name != (0 as *u8) { cd_strz(fd, c.name) }
201 cd_str(fd, "\",\"n_genealogy\":", 16)
202 cd_i64(fd, c.n_genealogy)
203 cd_str(fd, ",\"n_lineage\":", 13)
204 cd_i64(fd, c.n_lineage)
205 cd_str(fd, ",\"perf_mma\":", 12)
206 cd_i64(fd, c.perf_vs_mathematica_status)
207 cd_str(fd, ",\"perf_numpy\":", 14)
208 cd_i64(fd, c.perf_vs_numpy_status)
209 cd_str(fd, ",\"perf_julia\":", 14)
210 cd_i64(fd, c.perf_vs_julia_status)
211 cd_str(fd, ",\"perf_sage\":", 13)
212 cd_i64(fd, c.perf_vs_sage_status)
213 cd_str(fd, ",\"perf_matlab\":", 15)
214 cd_i64(fd, c.perf_vs_matlab_status)
215 cd_str(fd, ",\"perf_r\":", 10)
216 cd_i64(fd, c.perf_vs_r_status)
217 cd_str(fd, ",\"smoke\":", 9)
218 cd_i64(fd, c.smoke_pass)
219 cd_str(fd, ",\"xcheck\":", 10)
220 cd_i64(fd, c.cross_check_status)
221 cd_str(fd, ",\"det\":", 7)
222 cd_i64(fd, c.determinism_status)
223 cd_str(fd, ",\"found\":", 9)
224 cd_i64(fd, c.foundation_reach)
225 cd_str(fd, ",\"wobbly\":", 10)
226 cd_i64(fd, c.wobbly_flag)
227 cd_str(fd, ",\"score_ppb\":", 13)
228 cd_i64(fd, c.completeness_score_ppb)
229 cd_str(fd, "}\n", 2)
230 return 0
231}
232
233// ===== card builder for one of our shipped theorems ====================
234//
235// Convenience: builds a fully-populated card for theorem #1 Pythagorean
236// (used as the reference example). Future theorem cards follow the
237// same pattern.
238
239func nx_card_build_pythagorean() -> *TheoremCard {
240 let c: *TheoremCard = nx_card_alloc()
241 c.theorem_id = 1
242 c.name = "Pythagorean theorem"
243 c.n_genealogy = 2 // Pythagoras + Euclid
244
245 // Lineage: NX_AX_GEO_TWO_POINTS_DETERMINE_LINE + NX_AX_ALG_DISTRIBUTIVITY
246 // + NX_AX_ALG_COMMUTATIVITY
247 let lin: *i64 = (sys_mmap(24)) as *i64
248 lin[0] = NX_AX_GEO_TWO_POINTS_DETERMINE_LINE
249 lin[1] = NX_AX_ALG_DISTRIBUTIVITY
250 lin[2] = NX_AX_ALG_COMMUTATIVITY
251 c.lineage_axiom_codes = lin
252 c.n_lineage = 3
253
254 // Perf: we don't currently bench Pythagorean check vs incumbents
255 // because it's trivially fast in every system. Mark WINS based on
256 // structural argument (our i64 check is a few muldivs, Mathematica
257 // would invoke its symbolic engine -- bigger).
258 c.perf_vs_mathematica_status = NX_PERF_WINS
259 c.perf_vs_numpy_status = NX_PERF_TIES
260 c.perf_vs_julia_status = NX_PERF_TIES
261
262 c.smoke_pass = 1 // PASS from nx_theorems_smoke.sh
263 c.cross_check_status = NX_XCHECK_MATCHES_INDEPENDENT // matches Euclid I.47 trivially
264 c.determinism_status = NX_DETERMINISM_BIT_IDENTICAL
265 c.foundation_reach = NX_FOUNDATION_SUFFICIENT // muldiv -> i64 -> bit
266 nx_card_compute_completeness(c)
267 return c
268}