infotheory/
axioms.rs

1//! # Axioms: Mathematical Property Verifiers
2//!
3//! This module provides generic functions to verify mathematical properties
4//! that should hold for any correct implementation of information-theoretic
5//! measures.
6
7// ============================================================================
8// Metric Axioms
9// ============================================================================
10
11/// Verify that a distance function d(x,x) is close to 0 (allow for small overhead).
12pub fn verify_identity<F>(metric: F, x: &[u8], tolerance: f64) -> bool
13where
14    F: Fn(&[u8], &[u8]) -> f64,
15{
16    let d = metric(x, x);
17    d.abs() <= tolerance
18}
19
20/// Verify symmetry: d(x,y) ≈ d(y,x).
21pub fn verify_symmetry<F>(metric: F, x: &[u8], y: &[u8], tolerance: f64) -> bool
22where
23    F: Fn(&[u8], &[u8]) -> f64,
24{
25    let d_xy = metric(x, y);
26    let d_yx = metric(y, x);
27    (d_xy - d_yx).abs() <= tolerance
28}
29
30/// Verify triangle inequality: d(x,z) ≤ d(x,y) + d(y,z).
31pub fn verify_triangle_inequality<F>(
32    metric: F,
33    x: &[u8],
34    y: &[u8],
35    z: &[u8],
36    tolerance: f64,
37) -> bool
38where
39    F: Fn(&[u8], &[u8]) -> f64,
40{
41    let d_xy = metric(x, y);
42    let d_yz = metric(y, z);
43    let d_xz = metric(x, z);
44    d_xz <= (d_xy + d_yz + tolerance)
45}
46
47/// Verify non-negativity: d(x,y) ≥ 0.
48pub fn verify_non_negativity<F>(metric: F, x: &[u8], y: &[u8]) -> bool
49where
50    F: Fn(&[u8], &[u8]) -> f64,
51{
52    // Allow tiny floating point errors slightly below zero
53    metric(x, y) >= -1e-12
54}
55
56// ============================================================================
57// Information Inequalities
58// ============================================================================
59
60/// Verify mutual information non-negativity: I(X;Y) ≥ 0.
61pub fn verify_mi_nonnegative<F>(mi: F, x: &[u8], y: &[u8]) -> bool
62where
63    F: Fn(&[u8], &[u8]) -> f64,
64{
65    mi(x, y) >= -1e-12
66}
67
68/// Verify subadditivity: H(X,Y) ≤ H(X) + H(Y).
69///
70/// This is equivalent to I(X;Y) ≥ 0.
71pub fn verify_subadditivity<FJoint, FMarg>(
72    joint_entropy: FJoint,
73    marginal_entropy: FMarg,
74    x: &[u8],
75    y: &[u8],
76    tolerance: f64,
77) -> bool
78where
79    FJoint: Fn(&[u8], &[u8]) -> f64,
80    FMarg: Fn(&[u8]) -> f64,
81{
82    let h_xy = joint_entropy(x, y);
83    let h_x = marginal_entropy(x);
84    let h_y = marginal_entropy(y);
85    h_xy <= (h_x + h_y + tolerance)
86}
87
88/// Verify conditioning reduces entropy: H(X|Y) ≤ H(X).
89pub fn verify_conditioning_reduces_entropy<FCond, FMarg>(
90    conditional_entropy: FCond,
91    marginal_entropy: FMarg,
92    x: &[u8],
93    y: &[u8],
94    tolerance: f64,
95) -> bool
96where
97    FCond: Fn(&[u8], &[u8]) -> f64,
98    FMarg: Fn(&[u8]) -> f64,
99{
100    let h_x_given_y = conditional_entropy(x, y);
101    let h_x = marginal_entropy(x);
102    h_x_given_y <= (h_x + tolerance)
103}
104
105/// Verify chain rule: H(X,Y) = H(X) + H(Y|X).
106pub fn verify_chain_rule<FJoint, FMarg, FCond>(
107    joint: FJoint,
108    marginal: FMarg,
109    conditional: FCond,
110    x: &[u8],
111    y: &[u8],
112    tolerance: f64,
113) -> bool
114where
115    FJoint: Fn(&[u8], &[u8]) -> f64,
116    FMarg: Fn(&[u8]) -> f64,
117    FCond: Fn(&[u8], &[u8]) -> f64, // H(Y|X)
118{
119    let h_xy = joint(x, y);
120    let h_x = marginal(x);
121    let h_y_given_x = conditional(y, x);
122
123    (h_xy - (h_x + h_y_given_x)).abs() <= tolerance
124}
125
126// ============================================================================
127// Bounds
128// ============================================================================
129
130/// Verify NCD range: 0 ≤ NCD ≤ 1+epsilon.
131///
132/// NCD theoretically can slightly exceed 1 due to compression overhead, so we allow
133/// a small margin or just check it's not egregiously large. Usually NCD <= 1.1 is safe.
134pub fn verify_ncd_bounds<F>(ncd: F, x: &[u8], y: &[u8]) -> bool
135where
136    F: Fn(&[u8], &[u8]) -> f64,
137{
138    let val = ncd(x, y);
139    val >= -1e-12 && val <= 1.1
140}
141
142/// Verify entropy is bounded by log2(alphabet_size).
143/// For bytes, max entropy is 8.0 bits/byte.
144pub fn verify_entropy_bounds<F>(entropy: F, data: &[u8]) -> bool
145where
146    F: Fn(&[u8]) -> f64,
147{
148    let h = entropy(data);
149    h >= -1e-12 && h <= 8.0 + 1e-12
150}