nx_probability.nx source
↩ module page · 140 lines · 6532 B
1// nx_probability.nx -- probability-measure substrate.
2//
3// Closes the LAST named blocker for Wikipedia "probabilistic proof"
4// method. Per user 2026-05-15: "no losses".
5//
6// Provides:
7// - Term constructors: Pr(A), Omega (sample space), set ops
8// intersection / union / complement on event symbols
9// - Kolmogorov axioms K1..K3 as v2 kernel axiom emitters
10// - common derived axioms: Pr(~A) = 1 - Pr(A); inclusion-exclusion
11//
12// Patent-clean: built on the v2 kernel + Term machinery only. Sym IDs
13// reserved 412001..412020 (probability family; distinct from arith
14// 410xxx and connectives 400xxx).
15
16// nx_safety_envelope:
17// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
18// sil_target: SIL1
19// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
20// verdict: NOT_YET_EVALUATED
21
22import "nx_kernel_v2.nx"
23
24const NX_PROB_SYM_PR: nx_int = 412001 // unary: Pr(A)
25const NX_PROB_SYM_OMEGA: nx_int = 412002 // sample space
26const NX_PROB_SYM_EMPTY: nx_int = 412003 // empty event
27const NX_PROB_SYM_INTERSECT: nx_int = 412004 // binary: A ∩ B
28const NX_PROB_SYM_UNION: nx_int = 412005 // binary: A ∪ B
29const NX_PROB_SYM_COMPLEMENT: nx_int = 412006 // unary: ~A (set complement)
30const NX_PROB_SYM_LE: nx_int = 412007 // binary: x <= y
31const NX_PROB_SYM_ZERO_R: nx_int = 412008 // real 0
32const NX_PROB_SYM_ONE_R: nx_int = 412009 // real 1
33const NX_PROB_SYM_PLUS_R: nx_int = 412010 // binary: x + y over R
34const NX_PROB_SYM_MINUS_R: nx_int = 412011 // binary: x - y over R
35
36// ===== Term constructors ============================================
37func nx_prob_pr(event: *Term) -> *Term {
38 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
39 arg.kind = event.kind; arg.sym = event.sym
40 arg.n_args = event.n_args; arg.args = event.args
41 return nx_term_app(NX_PROB_SYM_PR, 1, arg)
42}
43
44func nx_prob_omega() -> *Term { return nx_term_const(NX_PROB_SYM_OMEGA) }
45func nx_prob_empty() -> *Term { return nx_term_const(NX_PROB_SYM_EMPTY) }
46func nx_prob_zero() -> *Term { return nx_term_const(NX_PROB_SYM_ZERO_R) }
47func nx_prob_one() -> *Term { return nx_term_const(NX_PROB_SYM_ONE_R) }
48
49func nx_prob_intersect(a: *Term, b: *Term) -> *Term {
50 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
51 let a0: *Term = args
52 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
53 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
54 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
55 return nx_term_app(NX_PROB_SYM_INTERSECT, 2, args)
56}
57
58func nx_prob_union(a: *Term, b: *Term) -> *Term {
59 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
60 let a0: *Term = args
61 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
62 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
63 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
64 return nx_term_app(NX_PROB_SYM_UNION, 2, args)
65}
66
67func nx_prob_complement(a: *Term) -> *Term {
68 let arg: *Term = (sys_mmap(NX_TERM_BYTES as i64)) as *Term
69 arg.kind = a.kind; arg.sym = a.sym; arg.n_args = a.n_args; arg.args = a.args
70 return nx_term_app(NX_PROB_SYM_COMPLEMENT, 1, arg)
71}
72
73func nx_prob_plus(a: *Term, b: *Term) -> *Term {
74 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
75 let a0: *Term = args
76 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
77 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
78 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
79 return nx_term_app(NX_PROB_SYM_PLUS_R, 2, args)
80}
81
82func nx_prob_minus(a: *Term, b: *Term) -> *Term {
83 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
84 let a0: *Term = args
85 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
86 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
87 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
88 return nx_term_app(NX_PROB_SYM_MINUS_R, 2, args)
89}
90
91func nx_prob_le(a: *Term, b: *Term) -> *Term {
92 let args: *Term = (sys_mmap((2 * NX_TERM_BYTES) as i64)) as *Term
93 let a0: *Term = args
94 a0.kind = a.kind; a0.sym = a.sym; a0.n_args = a.n_args; a0.args = a.args
95 let a1: *Term = ((args as nx_int) + NX_TERM_BYTES) as *Term
96 a1.kind = b.kind; a1.sym = b.sym; a1.n_args = b.n_args; a1.args = b.args
97 return nx_term_app(NX_PROB_SYM_LE, 2, args)
98}
99
100// ===== Kolmogorov axiom emitters ====================================
101
102// K1: Pr(A) >= 0 (encoded as 0 <= Pr(A))
103func nx_prob_axiom_k1(ch: *K2Chain, event: *Term) -> nx_int {
104 return nx_k2_axiom(ch, nx_prob_le(nx_prob_zero(), nx_prob_pr(event)))
105}
106
107// K2: Pr(Omega) = 1
108func nx_prob_axiom_k2(ch: *K2Chain) -> nx_int {
109 return nx_k2_axiom(ch, nx_k2_eq(nx_prob_pr(nx_prob_omega()), nx_prob_one()))
110}
111
112// K3 (finite additivity, specialised to a binary disjoint pair):
113// Pr(A ∪ B) = Pr(A) + Pr(B) when (A ∩ B) = empty
114// Caller supplies a separate disjointness premise; this emitter just
115// encodes the additivity equality conditional on disjointness, as
116// (A ∩ B == empty) => (Pr(A∪B) == Pr(A) + Pr(B))
117func nx_prob_axiom_k3_disjoint(ch: *K2Chain, a: *Term, b: *Term) -> nx_int {
118 let disjoint: *Term = nx_k2_eq(nx_prob_intersect(a, b), nx_prob_empty())
119 let union_pr: *Term = nx_prob_pr(nx_prob_union(a, b))
120 let sum_pr: *Term = nx_prob_plus(nx_prob_pr(a), nx_prob_pr(b))
121 return nx_k2_axiom(ch, nx_k2_imp(disjoint, nx_k2_eq(union_pr, sum_pr)))
122}
123
124// Common derived: Pr(~A) = 1 - Pr(A). Shipped as an axiom emitter
125// because deriving it from K1+K2+K3 would need full real-number
126// arithmetic substrate (named follow-up; same shape as nat substrate).
127func nx_prob_axiom_complement(ch: *K2Chain, a: *Term) -> nx_int {
128 let lhs: *Term = nx_prob_pr(nx_prob_complement(a))
129 let rhs: *Term = nx_prob_minus(nx_prob_one(), nx_prob_pr(a))
130 return nx_k2_axiom(ch, nx_k2_eq(lhs, rhs))
131}
132
133// Inclusion-exclusion (binary):
134// Pr(A ∪ B) = Pr(A) + Pr(B) - Pr(A ∩ B)
135func nx_prob_axiom_inclusion_exclusion_2(ch: *K2Chain, a: *Term, b: *Term) -> nx_int {
136 let lhs: *Term = nx_prob_pr(nx_prob_union(a, b))
137 let part_sum: *Term = nx_prob_plus(nx_prob_pr(a), nx_prob_pr(b))
138 let rhs: *Term = nx_prob_minus(part_sum, nx_prob_pr(nx_prob_intersect(a, b)))
139 return nx_k2_axiom(ch, nx_k2_eq(lhs, rhs))
140}