//! aether_chebyshev.rs
//!
//! Provenance: Lean 4 -> C -> Rust
//! Source: HeytingLean.Bridge.Sharma.AetherChebyshev

fn mean(x: &[f64]) -> f64 {
    if x.is_empty() {
        0.0
    } else {
        x.iter().sum::<f64>() / (x.len() as f64)
    }
}

fn stddev(x: &[f64]) -> f64 {
    if x.is_empty() {
        return 0.0;
    }
    let m = mean(x);
    let v = x.iter().map(|v| {
        let d = *v - m;
        d * d
    }).sum::<f64>() / (x.len() as f64);
    libm::sqrt(v)
}

/// (Lean: reclaimable)
pub fn reclaimable_count(x: &[f64], k: f64) -> usize {
    let m = mean(x);
    let sd = stddev(x);
    let thr = m - k * sd;
    x.iter().filter(|v| **v <= thr).count()
}

/// (Lean: chebyshev_finite)
pub fn chebyshev_guard_check(x: &[f64], k: f64) -> bool {
    if x.is_empty() || k <= 0.0 {
        return false;
    }
    let sd = stddev(x);
    if sd <= 0.0 {
        return true;
    }
    let reclaim = reclaimable_count(x, k) as f64;
    reclaim <= (x.len() as f64) / (k * k) + 1e-12
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_guard_check() {
        let x = [1.0, 2.0, 3.0, 4.0, 10.0, 11.0];
        assert!(chebyshev_guard_check(&x, 2.0));
    }

    #[test]
    fn test_reclaimable_includes_threshold_equality() {
        let x = [0.0, 2.0, 4.0];
        // mean = 2, stddev = sqrt(8/3), threshold at k=0 is exactly mean.
        assert_eq!(reclaimable_count(&x, 0.0), 2);
    }
}