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

↩ module page · 195 lines · 14602 B
1// nx_appliedmath_gate.nx -- THE APPLIED MATHEMATICS THE ESTATE ALREADY COMPUTES, PROVED BY IDENTITY.
2//
3// WHY THIS EXISTS (measured 2026-09-03): a capability census found real applied mathematics scattered across
4// this estate and presented as MATHEMATICS NOWHERE -- a Weibull wear-and-tear core in pure integer fixed point,
5// loan amortization whose header claims "conservation-proven" with no gate to prove it, single-pass streaming
6// statistics with a parallel MERGE, and general matrix algebra. /compare/computational grades only the SYMBOLIC
7// stack against Wolfram and SymPy; none of these organs appear on any board, and none had a gate.
8//
9// THE FIELD'S OWN COMPLAINT IS THE OPPORTUNITY. The mathematics community's documented grievance against
10// computer algebra is not breadth, it is TRUST: a published account records Mathematica computing a determinant
11// wrongly and returning DIFFERENT answers for the same determinant on two evaluations, inside a system whose
12// source cannot be inspected. Meanwhile numerical analysis is the branch largely ABSENT from mathlib, so the
13// applied half of mathematics has almost no machine-checked corpus at all. This estate's applied math is
14// integer-exact and bit-reproducible by construction, which is worth nothing until something CHECKS it. This
15// gate is that check.
16//
17// EVERY TOOTH IS AN IDENTITY OR A CONSERVATION LAW, TRUE INDEPENDENTLY OF ANY IMPLEMENTATION:
18//   money      -- the principal repaid over the schedule equals the principal borrowed, to the penny
19//   survival   -- ln and exp are inverses; ln(1)=0; exp(0)=1; a longer exposure cannot lower failure probability
20//   statistics -- merging two streams gives the mean, count and extrema of the single stream over their union
21//   matrices   -- transpose is an involution, (AB)^T = B^T A^T, a repeated row makes the determinant vanish
22// Tolerances are DECLARED, never implied: the fixed-point transcendentals are checked to a stated number of
23// Q20 units, and the tolerance is named in the tooth so a reader cannot mistake approximate for exact.
24// license_tier: ORIGINAL
25import "nx_amort_lib.nx"
26import "nx_hazard_lib.nx"
27import "nx_sketch_stream_stats.nx"
28import "nx_matrix.nx"
29import "nx_gate_verdict.nx"
30
31const AM_Q14: i64 = 16384                 // nx_matrix's fixed-point unit
32const AM_LN_TOL: i64 = 2000               // Q20 units accepted on an ln/exp round trip (~0.0019 absolute)
33const AM_LN2_TOL: i64 = 200               // Q20 units accepted against the banked ln(2) constant
34const AM_PRINCIPAL: i64 = 25000000        // 250,000.00 in pennies
35const AM_RATE_BP: i64 = 625               // 6.25% annual, in basis points
36const AM_TERM: i64 = 360                  // 30 years, monthly
37const AM_BPS: i64 = 10000
38
39func am_abs(v: i64) -> i64 { if v < 0 { return 0 - v } return v }
40func am_near(a: i64, b: i64, tol: i64) -> i64 { if am_abs(a - b) <= tol { return 1 } return 0 }
41
42// THE VALUE EMITTER MOVED TO THE BASE CLASS. This gate was where the defect was found and it was fixed here
43// first, with a local am_kv -- which made it the SECOND printer in the estate for a law the estate already
44// had. A correction with no callable home fixes exactly one site, so gv_kv and gv_values_head now live in
45// nx_gate_verdict.nx and EVERY gate inherits them. This file deliberately keeps no twin.
46// element-wise matrix equality
47func am_meq(a: *Matrix, b: *Matrix, rows: i64, cols: i64) -> i64 {
  var r: i64 = 0
  while r < rows {
      var c: i64 = 0
      while c < cols {
          if nx_matrix_get(a, r, c) != nx_matrix_get(b, r, c) { return 0 }
          c = c + 1
      }
      r = r + 1
  }
  return 1
58}
59
60func main() -> i64 {
  gv_head("NX-APPLIEDMATH-GATE -- the applied mathematics this estate already computes, proved by CONSERVATION and IDENTITY: money that must balance to the penny, a survival core whose ln and exp must invert, streaming statistics whose merge must equal the single stream, and matrix laws that hold at any scale" as *u8)
  let ctr: *i64 = gv_ctr()
63
  // ---- MONEY: the conservation law the amortization header claims and nothing checked -------------------
  let pay: i64 = amort_level_payment(AM_PRINCIPAL, AM_RATE_BP, AM_TERM)
  gv_check("fixture-reached-the-condition: a real 30-year schedule at 6.25 percent produces a positive level payment" as *u8, ((pay > 0) as i64) & ((pay < AM_PRINCIPAL) as i64), ctr)
  let psum: i64 = amort_principal_sum(AM_PRINCIPAL, AM_RATE_BP, AM_TERM)
  gv_check_eq("CONSERVATION-every-penny-of-principal-is-repaid-exactly-once-over-the-whole-schedule" as *u8, psum, AM_PRINCIPAL, ctr)
  let interest0: i64 = amort_monthly_interest(AM_PRINCIPAL, 0)
  gv_check_eq("a-zero-rate-loan-accrues-exactly-zero-interest" as *u8, interest0, 0, ctr)
  let i1: i64 = amort_monthly_interest(1200000, AM_RATE_BP)
  let i2: i64 = amort_monthly_interest(2400000, AM_RATE_BP)
  gv_check_eq("monthly-interest-is-LINEAR-in-the-balance-doubling-the-balance-doubles-the-interest" as *u8, i2, i1 * 2, ctr)
  // A ZERO-RATE LOAN COSTING EXACTLY THE PRINCIPAL is the non-circular tooth here: total_interest is DEFINED
  // as total-paid-minus-principal, so asserting that relation would test the definition against itself. The
  // zero-rate case is real content -- it can only hold if the payment schedule itself is right.
  let ti0: i64 = amort_total_interest(AM_PRINCIPAL, 0, AM_TERM)
  gv_check_eq("a-zero-rate-loan-costs-EXACTLY-the-principal-and-not-one-penny-more" as *u8, ti0, 0, ctr)
  let ti: i64 = amort_total_interest(AM_PRINCIPAL, AM_RATE_BP, AM_TERM)
  // MEASURED, and it corrected this gate's first draft: at 6.25 percent over 30 years the interest EXCEEDS
  // the principal. The first version of this tooth asserted interest < principal and FAILED -- the schedule
  // was right and the assertion was wrong. Recorded so the next reader does not re-derive the same error.
  gv_check("interest-on-a-real-30-year-mortgage-is-positive-and-EXCEEDS-the-principal-at-6.25-percent" as *u8, ((ti > 0) as i64) & ((ti > AM_PRINCIPAL) as i64), ctr)
  let bal_end: i64 = amort_balance_after(AM_PRINCIPAL, AM_RATE_BP, pay, AM_TERM)
  gv_check("the-balance-after-the-final-scheduled-payment-is-driven-to-zero-or-below-never-left-outstanding" as *u8, (bal_end <= 0) as i64, ctr)
86
  // ---- SURVIVAL: fixed-point ln and exp must be inverses, or every hazard number downstream is fiction --
  gv_check_eq("ln-of-one-is-exactly-zero" as *u8, hz_ln(HZ_FP), 0, ctr)
  gv_check_eq("exp-of-zero-is-exactly-one" as *u8, hz_exp(0), HZ_FP, ctr)
  gv_check_near("ln-of-two-reproduces-the-banked-constant-within-a-DECLARED-200-Q20-units" as *u8, hz_ln(HZ_FP * 2), HZ_LN2, AM_LN2_TOL, ctr)
  let x1: i64 = HZ_FP * 3
  let rt1: i64 = hz_ln(hz_exp(hz_ln(x1)))
  gv_check_near("ln-and-exp-INVERT-each-other-on-a-real-value-within-a-DECLARED-2000-Q20-units" as *u8, rt1, hz_ln(x1), AM_LN_TOL, ctr)
  let beta: i64 = HZ_FP * 2
  let eta: i64 = 1000
  let short_risk: i64 = hz_cond_pfail_bps(500, 600, beta, eta)
  let long_risk: i64 = hz_cond_pfail_bps(500, 900, beta, eta)
  gv_check("fixture-reached-the-condition: the shorter exposure returns a real probability, not an error code" as *u8, ((short_risk >= 0) as i64) & ((short_risk <= AM_BPS) as i64), ctr)
  gv_check("SURVIVAL-MONOTONICITY-a-longer-exposure-can-never-carry-a-lower-conditional-failure-probability" as *u8, (long_risk >= short_risk) as i64, ctr)
  gv_check_eq("expected-cost-is-the-failure-probability-times-the-repair-cost-in-basis-points" as *u8, hz_expected_cost(2500, 40000), (2500 * 40000) / AM_BPS, ctr)
  let mr1: i64 = hz_median_rank_fp(1, 10)
  let mr5: i64 = hz_median_rank_fp(5, 10)
  gv_check("median-ranks-increase-with-order-statistic-so-the-Weibull-fit-reads-a-sorted-sample" as *u8, (mr5 > mr1) as i64, ctr)
104
  // ---- STATISTICS: the MERGE law -- a parallel summary must equal the single pass over the union --------
  let sa: *StreamStats = nx_stats_alloc()
  let sb: *StreamStats = nx_stats_alloc()
  let all: *StreamStats = nx_stats_alloc()
  nx_stats_add(sa, 4); nx_stats_add(sa, 8); nx_stats_add(sa, 15)
  nx_stats_add(sb, 16); nx_stats_add(sb, 23); nx_stats_add(sb, 42)
  nx_stats_add(all, 4); nx_stats_add(all, 8); nx_stats_add(all, 15)
  nx_stats_add(all, 16); nx_stats_add(all, 23); nx_stats_add(all, 42)
  let m: *StreamStats = nx_stats_merge(sa, sb)
  gv_check("fixture-reached-the-condition: both partial streams are non-empty so the merge is not a copy" as *u8, ((nx_stats_count(sa) == 3) as i64) & ((nx_stats_count(sb) == 3) as i64), ctr)
  gv_check_eq("MERGE-LAW-count-of-the-merge-equals-the-single-pass-over-the-union" as *u8, nx_stats_count(m), nx_stats_count(all), ctr)
  gv_check_eq("MERGE-LAW-mean-of-the-merge-equals-the-single-pass-mean" as *u8, nx_stats_mean(m), nx_stats_mean(all), ctr)
  gv_check("MERGE-LAW-extrema-of-the-merge-equal-the-single-pass-extrema" as *u8, ((nx_stats_min(m) == nx_stats_min(all)) as i64) & ((nx_stats_max(m) == nx_stats_max(all)) as i64), ctr)
  let flat: *StreamStats = nx_stats_alloc()
  nx_stats_add(flat, 7); nx_stats_add(flat, 7); nx_stats_add(flat, 7)
  gv_check_eq("a-stream-with-no-spread-has-exactly-zero-variance" as *u8, nx_stats_variance(flat), 0, ctr)
  gv_bite("neg-control-variance-fires-on-a-varying-stream-and-is-silent-on-a-constant-one" as *u8, (nx_stats_variance(all) != 0) as i64, (nx_stats_variance(flat) != 0) as i64, ctr)
122
  // ---- MATRICES: laws that hold at ANY fixed-point scale, so the scaling cannot hide a wrong product ----
  let A: *Matrix = nx_matrix_alloc(2, 2)
  let B: *Matrix = nx_matrix_alloc(2, 2)
  let I: *Matrix = nx_matrix_alloc(2, 2)
  nx_matrix_set(A, 0, 0, 3 * AM_Q14); nx_matrix_set(A, 0, 1, 1 * AM_Q14)
  nx_matrix_set(A, 1, 0, 2 * AM_Q14); nx_matrix_set(A, 1, 1, 4 * AM_Q14)
  nx_matrix_set(B, 0, 0, 5 * AM_Q14); nx_matrix_set(B, 0, 1, 0 - (2 * AM_Q14))
  nx_matrix_set(B, 1, 0, 1 * AM_Q14); nx_matrix_set(B, 1, 1, 6 * AM_Q14)
  // DECLARED PROPERTY, MEASURED FROM THE SOURCE: nx_matrix_multiply accumulates a plain integer product and
  // does NOT rescale, so the CALLER owns the fixed point. The multiplicative identity is therefore the matrix
  // with unit 1, not with unit Q14 -- this gate's first draft used Q14 and FAILED, because A times that
  // matrix is A scaled by 16384. The library is right; the assumption was wrong, and it is written down here
  // because a caller who assumes Q14 rescaling will silently inflate every product by the scale factor.
  nx_matrix_identity(I, 1)
  let AI: *Matrix = nx_matrix_alloc(2, 2)
  nx_matrix_multiply(A, I, AI)
  gv_check("multiplying-by-the-unit-identity-returns-the-matrix-unchanged-the-caller-owns-the-fixed-point-scale" as *u8, am_meq(AI, A, 2, 2), ctr)
  let AT: *Matrix = nx_matrix_transpose(A)
  let ATT: *Matrix = nx_matrix_transpose(AT)
  gv_check("TRANSPOSE-IS-AN-INVOLUTION-transposing-twice-returns-the-original-exactly" as *u8, am_meq(ATT, A, 2, 2), ctr)
  let AB: *Matrix = nx_matrix_alloc(2, 2)
  nx_matrix_multiply(A, B, AB)
  let ABT: *Matrix = nx_matrix_transpose(AB)
  let BT: *Matrix = nx_matrix_transpose(B)
  let BTAT: *Matrix = nx_matrix_alloc(2, 2)
  nx_matrix_multiply(BT, AT, BTAT)
  gv_check("REVERSAL-LAW-the-transpose-of-a-product-is-the-product-of-the-transposes-in-reverse-order" as *u8, am_meq(ABT, BTAT, 2, 2), ctr)
  let S: *Matrix = nx_matrix_alloc(2, 2)
  nx_matrix_set(S, 0, 0, 7 * AM_Q14); nx_matrix_set(S, 0, 1, 3 * AM_Q14)
  nx_matrix_set(S, 1, 0, 7 * AM_Q14); nx_matrix_set(S, 1, 1, 3 * AM_Q14)
  gv_check_eq("a-matrix-with-a-REPEATED-ROW-is-singular-so-its-determinant-vanishes" as *u8, nx_matrix_det_2x2(S), 0, ctr)
  gv_bite("neg-control-the-determinant-is-non-zero-for-an-invertible-matrix-and-zero-for-a-singular-one" as *u8, (nx_matrix_det_2x2(A) != 0) as i64, (nx_matrix_det_2x2(S) != 0) as i64, ctr)
155
  // ---- EMITTED VALUES: every number the teeth above rest on, printed so an INDEPENDENT arithmetic
  // OUTSIDE this estate can recompute it from the declared inputs and DISAGREE. This is the second
  // method class made possible: a witness that cannot see a value cannot refute one. The verdict line
  // is still written LAST by gv_verdict, so positional readers are unaffected by this block.
  gv_values_head()
  gv_puts("  units: money in integer pennies, transcendentals in Q20 fixed point, risk in basis points\n" as *u8)
  gv_kv("loan_principal_pennies" as *u8, AM_PRINCIPAL)
  gv_kv("loan_annual_rate_basis_points" as *u8, AM_RATE_BP)
  gv_kv("loan_term_months" as *u8, AM_TERM)
  gv_kv("level_payment_pennies" as *u8, pay)
  gv_kv("principal_repaid_over_whole_schedule_pennies" as *u8, psum)
  gv_kv("total_interest_pennies" as *u8, ti)
  gv_kv("total_interest_at_zero_rate_pennies" as *u8, ti0)
  gv_kv("first_month_interest_at_zero_rate_pennies" as *u8, interest0)
  gv_kv("monthly_interest_on_balance_1200000_pennies" as *u8, i1)
  gv_kv("monthly_interest_on_balance_2400000_pennies" as *u8, i2)
  gv_kv("balance_after_final_scheduled_payment_pennies" as *u8, bal_end)
  gv_kv("fixed_point_one_q20" as *u8, HZ_FP)
  gv_kv("ln_of_two_computed_q20" as *u8, hz_ln(HZ_FP * 2))
  gv_kv("ln_of_two_banked_constant_q20" as *u8, HZ_LN2)
  gv_kv("ln_of_three_computed_q20" as *u8, hz_ln(x1))
  gv_kv("ln_exp_ln_of_three_roundtrip_q20" as *u8, rt1)
  gv_kv("conditional_pfail_over_600_hours_basis_points" as *u8, short_risk)
  gv_kv("conditional_pfail_over_900_hours_basis_points" as *u8, long_risk)
  gv_kv("median_rank_order_1_of_10_q20" as *u8, mr1)
  gv_kv("median_rank_order_5_of_10_q20" as *u8, mr5)
  gv_kv("merged_stream_count" as *u8, nx_stats_count(m))
  gv_kv("merged_stream_mean" as *u8, nx_stats_mean(m))
  gv_kv("merged_stream_min" as *u8, nx_stats_min(m))
  gv_kv("merged_stream_max" as *u8, nx_stats_max(m))
  gv_kv("single_pass_union_count" as *u8, nx_stats_count(all))
  gv_kv("single_pass_union_mean" as *u8, nx_stats_mean(all))
  gv_kv("determinant_of_invertible_2x2_at_q14_scale" as *u8, nx_matrix_det_2x2(A))
  gv_kv("determinant_of_repeated_row_2x2" as *u8, nx_matrix_det_2x2(S))
  gv_puts("\n" as *u8)
191
  let rc: i64 = gv_verdict("appliedmath-gate" as *u8, ctr, "money conserved to the penny, ln and exp proved mutual inverses within a declared tolerance, survival monotone, the streaming merge law equal to the single pass, and matrix laws that hold at any scale -- with three comparators bite-proven" as *u8)
  sys_exit(rc)
  return rc
195}
nx_appliedmath_gate.nx source

`nx_appliedmath_gate.nx` source
