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

fn nat_dist_u8(a: u8, b: u8) -> usize {
    a.abs_diff(b) as usize
}

/// (Lean: isDetectedLoop)
pub fn detected_loop_at(data: &[u8], i: usize, tol: usize) -> bool {
    if i + 3 >= data.len() {
        return false;
    }
    let a = data[i];
    let b = data[i + 1];
    let c = data[i + 2];
    let d = data[i + 3];
    let close = nat_dist_u8(a, d) <= tol;
    let middle_far = nat_dist_u8(a, b) > tol || nat_dist_u8(a, c) > tol;
    close && middle_far
}

/// (Lean: betti1_heuristic)
pub fn betti1_heuristic(data: &[u8], tol: usize) -> usize {
    (0..data.len()).filter(|i| detected_loop_at(data, *i, tol)).count()
}

/// Runtime bridge value from an exact/proxy Betti provider.
pub fn betti1_bridge_value(betti1_exact_or_proxy: usize) -> usize {
    betti1_exact_or_proxy
}

/// (Lean: betti_error_bound)
/// One-sided overlap form: `heuristic <= b + (n - 3)`.
pub fn betti_error_bound_check(data: &[u8], tol: usize, betti1_exact_or_proxy: usize) -> bool {
    let h = betti1_heuristic(data, tol);
    let b = betti1_bridge_value(betti1_exact_or_proxy);
    let overlap = data.len().saturating_sub(3);
    h <= b + overlap
}

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

    #[test]
    fn test_betti_bound_check() {
        let data = [1u8, 9, 8, 2, 7, 6, 1, 2];
        assert!(betti_error_bound_check(&data, 3, 5));
    }
}