//! hybrid_zeckendorf_density.rs
//!
//! Safe Rust transpilation from verified C (CAB pipeline).
//! Source: HeytingLean.Bridge.Veselov.HybridZeckendorf.DensityBounds
//!
//! Logarithmic density bounds on the active level count of hybrid numbers,
//! derived from the doubly-exponential weight tower.
//!
//! Provenance: Lean 4 -> LambdaIR -> MiniC -> C -> Rust
//! Correctness inherited from verified C source.

use crate::hybrid_zeckendorf_eval::{eval, HybridNumber, MAX_LEVELS};
use crate::hybrid_zeckendorf_fib::lazy_eval_fib;

/// Count of active (non-zero) levels in a hybrid number.
pub fn active_level_count(x: &HybridNumber) -> u32 {
    let mut count = 0u32;
    for i in 0..MAX_LEVELS {
        if !x.levels[i].is_empty() {
            count += 1;
        }
    }
    count
}

/// Upper bound on the number of active levels.
///
/// `active_levels(X) <= floor(log_1000(eval(X))) + 2`
///
/// (Lean: `active_levels_bound`)
///
/// Proof: the highest active level k satisfies `weight(k) <= eval(X)`.
/// Since `weight(k) = 1000^(2^(k-1))` for `k >= 1`, taking `log_1000` gives
/// `2^(k-1) <= log_1000(eval(X))`, and `k <= 2^(k-1) + 1` for `k >= 1`.
pub fn active_levels_bound(x: &HybridNumber) -> u32 {
    let val = eval(x);
    if val == 0 {
        return 0;
    }
    if val == 1 {
        return 1;
    }
    let log_val = (val as f64).log(1000.0);
    log_val as u32 + 2
}

/// Density statistic: `rho(X) = active_levels(X) / log_phi(eval(X))`
///
/// (Lean: `density`)
///
/// Measures how many levels are used relative to the information-theoretic
/// minimum for the represented value. Lower density = sparser representation.
pub fn density(x: &HybridNumber) -> f64 {
    let val = eval(x);
    if val <= 1 {
        return 0.0;
    }

    let phi: f64 = (1.0 + 5.0_f64.sqrt()) / 2.0;
    let log_phi_val = (val as f64).ln() / phi.ln();
    if log_phi_val < 1e-15 {
        return 0.0;
    }

    active_level_count(x) as f64 / log_phi_val
}

/// Upper bound on the density statistic.
///
/// `density(X) <= (log_1000(eval(X)) + 2) / log_phi(eval(X))`
///
/// (Lean: `density_upper_bound`)
///
/// This ratio decreases as `eval(X)` grows because the numerator has
/// base 1000 while the denominator has base phi (smaller base = larger log).
pub fn density_upper_bound(x: &HybridNumber) -> f64 {
    let val = eval(x);
    if val <= 1 {
        return 0.0;
    }

    let phi: f64 = (1.0 + 5.0_f64.sqrt()) / 2.0;
    let log_phi_val = (val as f64).ln() / phi.ln();
    if log_phi_val < 1e-15 {
        return 0.0;
    }

    let log_1000_val = (val as f64).ln() / 1000.0_f64.ln();
    (log_1000_val + 2.0) / log_phi_val
}

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

    #[test]
    fn test_active_levels_bound_holds() {
        let x = from_nat(123456);
        let actual = active_level_count(&x);
        let bound = active_levels_bound(&x);
        assert!(actual <= bound, "actual {} > bound {}", actual, bound);
    }

    #[test]
    fn test_density_bounded() {
        let x = from_nat(999999);
        let d = density(&x);
        let ub = density_upper_bound(&x);
        assert!(d <= ub + 1e-10, "density {} > upper bound {}", d, ub);
    }
}