code wiki / (root) / nx_mathcore_gate.nx
`nx_mathcore_gate.nx` source

↩ module page · 259 lines · 14295 B
1// nx_mathcore_gate.nx -- THE MATH CORE HAD NO GATE AT ALL (measured 2026-09-03).
2//
3// nx_catalog says it plainly: nx_bigint_gate, nx_rational_gate, nx_complex_gate and nx_derive_gate are ALL
4// ABSENT -- no source, no binary, nothing promoted. So the estate's exact arithmetic (arbitrary-precision
5// integers and exact rationals), which /compare/computational claims presence on in its very first rows and
6// which the no-float determinism doctrine rests on, carried ZERO executable proof. That is why the board reads
7// CLAIM-ONLY on the honesty census: it asserts coverage with no evidence a referee can run.
8//
9// EVERY TOOTH HERE IS AN ALGEBRAIC IDENTITY, WHICH IS ITS OWN ORACLE. A test that compares an implementation
10// against a number a human typed proves only that the human agreed with the code. An identity -- a*(b+c) =
11// a*b + a*c, (a+b)-b = a, 1/3 + 1/6 = 1/2 -- is true independently of any implementation, so a wrong add, a
12// wrong carry or a wrong normalisation cannot satisfy it. The distributivity teeth are the load-bearing ones:
13// they multiply and add the SAME operands two different ways and demand the same bytes.
14//
15// NON-VACUITY IS ASSERTED, NOT ASSUMED: the carry teeth assert the carry actually FIRED (a round-trip through
16// a shift that never carried would pass while proving nothing), and both comparators are bite-proven -- each
17// must REPORT a difference on values that differ and stay SILENT on values that are equal. A comparator that
18// answers "equal" to everything would pass every identity above and is exactly what the bite catches.
19//
20// license_tier: ORIGINAL
21import "nx_bigint_lib.nx"
22import "nx_rational.nx"
23import "nx_complex.nx"
24import "nx_derive.nx"
25import "nx_gate_verdict.nx"
26
27const MG_LIMB_SLOTS: i64 = 8          // scratch limbs per operand (well above the 2-4 the teeth use)
28const MG_SLOT_BYTES: i64 = 64         // MG_LIMB_SLOTS * 8
29const MG_BYTES_BE: i64 = 8            // 2 limbs = 8 big-endian bytes
30const MG_N1: i64 = 1
31const MG_N2: i64 = 2
32const MG_N4: i64 = 4
33const MG_N5: i64 = 5
34const MG_TOPBIT_LIMB: i64 = 0x80000000
35const MG_FULL_LIMB: i64 = 0xFFFFFFFF
36
37func mg_new() -> *i64 {
  let p: *i64 = sys_mmap(MG_SLOT_BYTES) as *i64
  bi_zero(p, MG_LIMB_SLOTS)
  return p
41}
42// a 64-bit value as two 32-bit limbs, little-endian limb order (the layout the lib uses)
43func mg_put64(x: *i64, v: i64) -> i64 {
  bi_zero(x, MG_LIMB_SLOTS)
  x[0] = v & MG_FULL_LIMB
  x[1] = (v >> 32) & MG_FULL_LIMB
  return 0
48}
49func mg_eqn(a: *i64, b: *i64, n: i64) -> i64 {
  if bi_cmp(a, b, n) == 0 { return 1 }
  return 0
52}
53
54func main() -> i64 {
  gv_head("NX-MATHCORE-GATE -- the estate's exact arithmetic proved by ALGEBRAIC IDENTITY: multi-limb carry, add/sub inverse, distributivity computed two ways, shift round-trip, byte round-trip, and exact rationals (this core had NO gate of any kind before today)" as *u8)
  let ctr: *i64 = gv_ctr()
  let neg1: i64 = 0 - 1
58
  // ---- BIGINT: carry across a limb boundary, the classic multi-precision failure -------------------------
  let a: *i64 = mg_new()
  let b: *i64 = mg_new()
  let r: *i64 = mg_new()
  a[0] = MG_FULL_LIMB
  b[0] = 1
  bi_add(r, a, b, MG_N1)
  gv_check("carry-crosses-a-limb-0xFFFFFFFF-plus-1-is-zero-limb-and-carry-one" as *u8, ((r[0] == 0) as i64) & ((r[1] == 1) as i64), ctr)
67
  // ---- BIGINT: (a+b)-b == a, over two limbs, chosen so the sum does not leave the pair -------------------
  let x: *i64 = mg_new()
  let y: *i64 = mg_new()
  let sum: *i64 = mg_new()
  let back: *i64 = mg_new()
  mg_put64(x, 0x1234567890ABCDEF)
  mg_put64(y, 0x0000000100000001)
  bi_add(sum, x, y, MG_N2)
  let noCarryOut: i64 = (sum[2] == 0) as i64
  let borrow: i64 = bi_sub(back, sum, y, MG_N2)
  gv_check("fixture-reached-the-condition: the two-limb sum did not carry out, so the inverse is over the same width" as *u8, noCarryOut, ctr)
  gv_check("add-then-subtract-returns-the-original-with-no-borrow" as *u8, ((borrow == 0) as i64) & (mg_eqn(back, x, MG_N2)), ctr)
80
  // ---- BIGINT: DISTRIBUTIVITY, the load-bearing tooth -- a*(b+c) computed two different ways ------------
  let da: *i64 = mg_new()
  let db: *i64 = mg_new()
  let dc: *i64 = mg_new()
  mg_put64(da, 0x00000003FFFFFFFF)
  mg_put64(db, 0x0000000212345678)
  mg_put64(dc, 0x000000010FEDCBA9)
  let bc: *i64 = mg_new()
  bi_add(bc, db, dc, MG_N2)
  let bcNoCarry: i64 = (bc[2] == 0) as i64
  let left: *i64 = mg_new()
  bi_mul(left, da, MG_N2, bc, MG_N2)          // 4 limbs
  left[4] = 0                                   // zero-extend to 5 so both sides compare at one width
  let ab: *i64 = mg_new()
  let ac: *i64 = mg_new()
  bi_mul(ab, da, MG_N2, db, MG_N2)
  bi_mul(ac, da, MG_N2, dc, MG_N2)
  let right: *i64 = mg_new()
  bi_add(right, ab, ac, MG_N4)                  // 5 limbs, top is the carry
  gv_check("fixture-reached-the-condition: b+c stayed inside two limbs so both sides use the same operands" as *u8, bcNoCarry, ctr)
  gv_check("DISTRIBUTIVITY-a-times-b-plus-c-equals-ab-plus-ac-byte-for-byte-over-five-limbs" as *u8, mg_eqn(left, right, MG_N5), ctr)
102
  // ---- BIGINT: multiplicative identity and annihilator --------------------------------------------------
  let one: *i64 = mg_new()
  let zero: *i64 = mg_new()
  one[0] = 1
  let p1: *i64 = mg_new()
  bi_mul(p1, da, MG_N2, one, MG_N2)
  gv_check("multiplying-by-one-returns-the-operand" as *u8, mg_eqn(p1, da, MG_N2), ctr)
  let p0: *i64 = mg_new()
  bi_mul(p0, da, MG_N2, zero, MG_N2)
  gv_check("multiplying-by-zero-returns-zero-across-every-limb" as *u8, mg_eqn(p0, zero, MG_N4), ctr)
113
  // ---- BIGINT: shift round-trip, with the carry asserted to have actually fired -------------------------
  let s: *i64 = mg_new()
  let sOrig: *i64 = mg_new()
  mg_put64(s, 0x89ABCDEF12345678)               // top bit of the high limb is SET, so shl1 must carry out
  mg_put64(sOrig, 0x89ABCDEF12345678)
  let shiftedOut: i64 = bi_shl1(s, MG_N2)
  bi_shr1(s, MG_N2, shiftedOut)
  gv_check("fixture-reached-the-condition: the left shift really did push a one out of the top" as *u8, (shiftedOut == 1) as i64, ctr)
  gv_check("shift-left-then-right-restores-the-value-when-the-carry-is-fed-back" as *u8, mg_eqn(s, sOrig, MG_N2), ctr)
123
  // ---- BIGINT: big-endian byte round-trip ---------------------------------------------------------------
  let bytes: *u8 = sys_mmap(MG_BYTES_BE + 8)
  let rt: *i64 = mg_new()
  bi_to_bytes_be(bytes, MG_BYTES_BE, sOrig, MG_N2)
  bi_from_bytes_be(rt, MG_LIMB_SLOTS, bytes, MG_BYTES_BE)
  gv_check("big-endian-serialise-then-parse-returns-the-same-limbs" as *u8, mg_eqn(rt, sOrig, MG_N2), ctr)
130
  // ---- BIGINT: ordering is a total order, antisymmetric --------------------------------------------------
  gv_check("compare-orders-both-ways-and-calls-a-value-equal-to-itself" as *u8, ((bi_cmp(sOrig, da, MG_N2) == 1) as i64) & ((bi_cmp(da, sOrig, MG_N2) == neg1) as i64) & ((bi_cmp(da, da, MG_N2) == 0) as i64), ctr)
133
  // ---- RATIONALS: exactness is the whole point ----------------------------------------------------------
  let third: *i64 = rat_new()
  let sixth: *i64 = rat_new()
  let half: *i64 = rat_new()
  let acc: *i64 = rat_new()
  rat_set(third, 1, 3)
  rat_set(sixth, 1, 6)
  rat_set(half, 1, 2)
  rat_add(acc, third, sixth)
  gv_check("one-third-plus-one-sixth-is-EXACTLY-one-half-no-rounding-anywhere" as *u8, (rat_eq(acc, half) == 1) as i64, ctr)
144
  let twoQuarters: *i64 = rat_new()
  rat_set(twoQuarters, 2, 4)
  gv_check("two-quarters-normalises-to-the-same-canonical-pair-as-one-half" as *u8, ((rat_eq(twoQuarters, half) == 1) as i64) & ((twoQuarters[0] == 1) as i64) & ((twoQuarters[1] == 2) as i64), ctr)
148
  let negHalf: *i64 = rat_new()
  rat_set(negHalf, 1, 0 - 2)
  gv_check("a-negative-denominator-is-canonicalised-onto-the-numerator-and-the-denominator-stays-positive" as *u8, ((negHalf[1] > 0) as i64) & ((negHalf[0] == (0 - 1)) as i64) & ((negHalf[1] == 2) as i64), ctr)
152
  let twoThirds: *i64 = rat_new()
  let threeHalves: *i64 = rat_new()
  let prod: *i64 = rat_new()
  let unit: *i64 = rat_new()
  rat_set(twoThirds, 2, 3)
  rat_set(threeHalves, 3, 2)
  rat_set(unit, 1, 1)
  rat_mul(prod, twoThirds, threeHalves)
  gv_check("a-rational-times-its-reciprocal-is-exactly-one" as *u8, (rat_eq(prod, unit) == 1) as i64, ctr)
162
  // rational distributivity, again computed two different ways
  let rb: *i64 = rat_new()
  let rc: *i64 = rat_new()
  rat_set(rb, 1, 4)
  rat_set(rc, 1, 6)
  let rbc: *i64 = rat_new()
  let rleft: *i64 = rat_new()
  rat_add(rbc, rb, rc)
  rat_mul(rleft, twoThirds, rbc)
  let rab: *i64 = rat_new()
  let rac: *i64 = rat_new()
  let rright: *i64 = rat_new()
  rat_mul(rab, twoThirds, rb)
  rat_mul(rac, twoThirds, rc)
  rat_add(rright, rab, rac)
  gv_check("DISTRIBUTIVITY-over-rationals-two-thirds-times-a-sum-equals-the-sum-of-the-products" as *u8, (rat_eq(rleft, rright) == 1) as i64, ctr)
179
  // ---- THE COMPARATORS THEMSELVES: a checker that says EQUAL to everything passes every identity above ---
  gv_bite("neg-control-bigint-compare-reports-a-difference-and-is-silent-on-a-match" as *u8, (bi_cmp(sOrig, da, MG_N2) != 0) as i64, (bi_cmp(da, da, MG_N2) != 0) as i64, ctr)
  gv_bite("neg-control-rational-equality-separates-one-half-from-one-third-and-joins-one-half-to-two-quarters" as *u8, (rat_eq(half, third) == 0) as i64, (rat_eq(half, twoQuarters) == 0) as i64, ctr)
183
  // ---- COMPLEX: the defining identity, and two independent paths that must agree ------------------------
  // ADDED 2026-09-03 after the "different syscall twin" worry was REFUTED by reading the file: syscalls.nx is
  // an ALIAS STUB that splices nx_syscalls.nx under import path-dedup and says so in its own header, so there
  // was never a duplicate-symbol barrier here. A BLOCKER I NAMED WITHOUT READING THE FILE WAS NOT A BLOCKER.
  let z: *Complex = nx_cx_alloc()
  let w: *Complex = nx_cx_alloc()
  let cout: *Complex = nx_cx_alloc()
  nx_cx_set(z, 1, 2)
  nx_cx_set(w, 3, 4)
  nx_cx_add(z, w, cout)
  gv_check("complex-addition-is-componentwise" as *u8, ((cout.re == 4) as i64) & ((cout.im == 6) as i64), ctr)
195
  let ii: *Complex = nx_cx_alloc()
  nx_cx_set(ii, 0, 1)
  nx_cx_mul(ii, ii, cout)
  gv_check("i-squared-is-minus-one-the-identity-that-defines-the-complex-numbers" as *u8, ((cout.re == (0 - 1)) as i64) & ((cout.im == 0) as i64), ctr)
200
  let zc: *Complex = nx_cx_alloc()
  nx_cx_set(z, 3, 4)
  nx_cx_conj(z, zc)
  nx_cx_mul(z, zc, cout)
  gv_check("z-times-its-conjugate-is-the-squared-modulus-and-is-purely-real" as *u8, ((cout.re == nx_cx_norm_sq(z)) as i64) & ((cout.im == 0) as i64), ctr)
206
  let ca: *Complex = nx_cx_alloc()
  let cb: *Complex = nx_cx_alloc()
  let cc: *Complex = nx_cx_alloc()
  let cbc: *Complex = nx_cx_alloc()
  let cleft: *Complex = nx_cx_alloc()
  let cab: *Complex = nx_cx_alloc()
  let cac: *Complex = nx_cx_alloc()
  let cright: *Complex = nx_cx_alloc()
  nx_cx_set(ca, 2, 3)
  nx_cx_set(cb, 1, 1)
  nx_cx_set(cc, 4, 0 - 2)
  nx_cx_add(cb, cc, cbc)
  nx_cx_mul(ca, cbc, cleft)
  nx_cx_mul(ca, cb, cab)
  nx_cx_mul(ca, cc, cac)
  nx_cx_add(cab, cac, cright)
  gv_check("DISTRIBUTIVITY-over-the-complex-numbers-computed-two-different-ways" as *u8, (nx_cx_eq(cleft, cright) == 1) as i64, ctr)
224
  let pw: *Complex = nx_cx_alloc()
  let sq: *Complex = nx_cx_alloc()
  nx_cx_pow(z, 2, pw)
  nx_cx_mul(z, z, sq)
  gv_check("raising-to-the-second-power-agrees-with-multiplying-by-itself-two-independent-code-paths" as *u8, (nx_cx_eq(pw, sq) == 1) as i64, ctr)
230
  // ---- THE DERIVATION VERIFIER: every tooth here is a REFUSAL, because a checker that accepts everything --
  // ---- would pass a "well-formed chain verifies" tooth and prove nothing at all --------------------------
  gv_check("fixture-reached-the-condition: modus ponens really does take two premises, so the chain below is well-formed" as *u8, (nx_drule_arity(NX_DRULE_MODUS_PONENS) == 2) as i64, ctr)
  let ch: *DerivationChain = nx_deriv_chain_alloc(8)
  let ax0: i64 = nx_deriv_add_axiom(ch, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
  let ax1: i64 = nx_deriv_add_axiom(ch, 2, NX_AX_PEANO_PA2_SUCCESSOR)
  let st: i64 = nx_deriv_add_step(ch, 3, NX_DRULE_MODUS_PONENS, ax0, ax1)
  nx_deriv_mark_theorem(ch)
  gv_check("a-well-formed-derivation-from-two-Peano-axioms-through-modus-ponens-VERIFIES" as *u8, ((ax0 == 0) as i64) & ((ax1 == 1) as i64) & ((st == 2) as i64) & ((nx_deriv_verify(ch) == NX_DERIV_VERIFY_OK) as i64), ctr)
240
  let unmarked: *DerivationChain = nx_deriv_chain_alloc(8)
  nx_deriv_add_axiom(unmarked, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
  gv_check("neg-control-a-chain-that-concludes-NOTHING-is-refused-as-having-no-theorem" as *u8, (nx_deriv_verify(unmarked) == NX_DERIV_VERIFY_NO_THEOREM) as i64, ctr)
244
  let empty: *DerivationChain = nx_deriv_chain_alloc(8)
  gv_check("neg-control-an-empty-chain-is-refused-rather-than-vacuously-accepted" as *u8, (nx_deriv_verify(empty) == NX_DERIV_VERIFY_NO_NODES) as i64, ctr)
247
  let bad: *DerivationChain = nx_deriv_chain_alloc(8)
  gv_check("neg-control-an-axiom-citation-that-names-no-real-axiom-is-refused-AT-INSERT" as *u8, (nx_deriv_add_axiom(bad, 1, 999) == (0 - 2)) as i64, ctr)
  nx_deriv_add_axiom(bad, 1, NX_AX_PEANO_PA1_ZERO_EXISTS)
  gv_check("neg-control-a-step-citing-an-unknown-inference-rule-is-refused" as *u8, (nx_deriv_add_step(bad, 2, 999, 0, 0 - 1) == (0 - 3)) as i64, ctr)
  gv_check("neg-control-a-step-whose-premise-does-not-exist-yet-is-refused-so-the-chain-stays-topological" as *u8, (nx_deriv_add_step(bad, 2, NX_DRULE_MODUS_PONENS, 0, 7) == (0 - 7)) as i64, ctr)
253
  gv_bite("neg-control-complex-equality-separates-different-numbers-and-joins-equal-ones" as *u8, (nx_cx_eq(z, ca) == 0) as i64, (nx_cx_eq(pw, sq) == 0) as i64, ctr)
255
  let rc2: i64 = gv_verdict("mathcore-gate" as *u8, ctr, "exact integer and rational arithmetic proved by identities that hold independently of any implementation, with both comparators bite-proven and every carry asserted to have fired" as *u8)
  sys_exit(rc2)
  return rc2
259}
nx_mathcore_gate.nx source

`nx_mathcore_gate.nx` source
