nx_measure.nx source
↩ module page · 88 lines · 3256 B
1// nx_measure.nx -- Lebesgue measure primitives.
2//
3// Substrate-level measure-theoretic foundation:
4// * interval length on [a, b]
5// * simple-function integration
6// * sigma-additivity verifier on disjoint intervals
7//
8// genealogy_id: lebesgue_1902 + borel_1898 + caratheodory_1914
9// lineage_id: measure_theory + sigma_additivity + integration
10// axioms: NX_AX_PROB_NONNEGATIVITY, NX_AX_MEAS_NULL_EMPTY,
11// NX_AX_MEAS_MONOTONICITY, NX_AX_MEAS_SUBADDITIVITY,
12// NX_AX_PROB_COUNTABLE_ADDITIVITY
13
14// nx_safety_envelope:
15// intended_use: AUTO_APPLIED -- primitive-specific tuning queued
16// sil_target: SIL1
17// evidence: [bulk_applied_2026-05-16, see-file-comment-for-detail]
18// verdict: NOT_YET_EVALUATED
19
20import "syscalls.nx"
21import "nx_axioms.nx"
22import "nx_i128.nx"
23
24// Length (Lebesgue measure) of [a, b]: max(b - a, 0).
25func nx_measure_interval_length(a: i64, b: i64) -> i64 {
26 if b <= a { return 0 }
27 return b - a
28}
29
30// Sum of lengths of n disjoint intervals (intervals[2i]=a_i, intervals[2i+1]=b_i).
31// Caller responsible for disjointness; primitive computes simple sum.
32func nx_measure_finite_union_length(intervals: *i64, n: i64) -> i64 {
33 var total: i64 = 0
34 var i: i64 = 0
35 while i < n {
36 total = total + nx_measure_interval_length(intervals[2*i], intervals[2*i+1])
37 i = i + 1
38 }
39 return total
40}
41
42// Integration of a piecewise-constant (simple) function over a finite
43// partition. vals[i] is the value on [intervals[2i], intervals[2i+1]).
44// Returns sum of val_i * length_i.
45func nx_measure_simple_integral(intervals: *i64, vals: *i64, n: i64) -> i64 {
46 var sum: i64 = 0
47 var i: i64 = 0
48 while i < n {
49 let len: i64 = nx_measure_interval_length(intervals[2*i], intervals[2*i+1])
50 sum = sum + nx_muldiv_i64(vals[i], len, 1)
51 i = i + 1
52 }
53 return sum
54}
55
56// Verify sigma-additivity on a finite family of disjoint intervals:
57// mu(union) == sum of mu(each)
58// Substrate trivially holds for finite disjoint unions (the deep
59// content of Lebesgue is the EXTENSION to countable unions; we verify
60// the finite predicate as a sub-axiom witness).
61func nx_measure_finite_additivity_check(intervals: *i64, n: i64) -> i64 {
62 let union_total: i64 = nx_measure_finite_union_length(intervals, n)
63 var sum_parts: i64 = 0
64 var i: i64 = 0
65 while i < n {
66 sum_parts = sum_parts + nx_measure_interval_length(intervals[2*i], intervals[2*i+1])
67 i = i + 1
68 }
69 if union_total == sum_parts { return 1 }
70 return 0
71}
72
73// Verify monotonicity: A ⊆ B -> mu(A) <= mu(B).
74// For intervals: if [a1, b1] ⊆ [a2, b2], then b1 - a1 <= b2 - a2.
75func nx_measure_monotonicity_check(a1: i64, b1: i64, a2: i64, b2: i64) -> i64 {
76 if a1 < a2 { return 1 } // not subset, vacuous
77 if b1 > b2 { return 1 } // not subset, vacuous
78 // Subset condition holds; check measure inequality.
79 let m1: i64 = nx_measure_interval_length(a1, b1)
80 let m2: i64 = nx_measure_interval_length(a2, b2)
81 if m1 <= m2 { return 1 }
82 return 0
83}
84
85// Empty set has measure 0.
86func nx_measure_empty_set() -> i64 {
87 return 0
88}