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

/// (Lean: upperBoundScore)
pub fn upper_bound_score(q: &[f64], centroid: &[f64], radius: f64) -> f64 {
    let qn = libm::sqrt(q.iter().map(|x| x * x).sum::<f64>());
    let cn = libm::sqrt(centroid.iter().map(|x| x * x).sum::<f64>());
    qn * (cn + radius)
}

/// (Lean: can_prune_sound)
pub fn can_prune(q: &[f64], centroid: &[f64], radius: f64, threshold: f64) -> bool {
    upper_bound_score(q, centroid, radius) < threshold
}

/// (Lean: prune_safe)
pub fn prune_safe_check(q: &[f64], k: &[f64], centroid: &[f64], radius: f64, threshold: f64) -> bool {
    if !can_prune(q, centroid, radius, threshold) {
        return false;
    }
    let dot: f64 = q.iter().zip(k.iter()).map(|(a, b)| a * b).sum();
    dot < threshold
}

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

    #[test]
    fn test_prune_safe() {
        let q = [1.0, 0.0, 0.0];
        let centroid = [0.1, 0.0, 0.0];
        let k = [0.15, 0.0, 0.0];
        assert!(can_prune(&q, &centroid, 0.1, 0.5));
        assert!(prune_safe_check(&q, &k, &centroid, 0.1, 0.5));
    }
}