// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Padic.Valuation
// Theorem preserved: padic_norm_sum_le_max, padic_norm_sub_le_max, appr_lt_pow

/// p-adic valuation: largest power of p dividing n.
/// Returns `None` for n == 0 (v_p(0) = ∞ by convention).
pub fn padic_val(p: u64, n: u64) -> Option<u32> {
    if n == 0 {
        return None;
    }
    let mut v = 0u32;
    let mut m = n;
    while m % p == 0 {
        m /= p;
        v += 1;
    }
    Some(v)
}

/// p-adic norm: |n|_p = p^{-v_p(n)}.
pub fn padic_norm(p: u64, n: i64) -> f64 {
    if n == 0 {
        return 0.0;
    }
    let abs_n = n.unsigned_abs();
    match padic_val(p, abs_n) {
        Some(v) => (p as f64).powf(-(v as f64)),
        None => 0.0,
    }
}

/// Theorem preserved: padic_norm_sum_le_max
/// |q + r|_p ≤ max(|q|_p, |r|_p)
pub fn check_ultrametric(p: u64, q: i64, r: i64) -> bool {
    let nq = padic_norm(p, q);
    let nr = padic_norm(p, r);
    let nsum = padic_norm(p, q + r);
    nsum <= nq.max(nr) + 1e-12
}

/// Theorem preserved: appr_lt_pow
/// x.appr(k) < p^k
pub fn check_appr_bound(p: u64, k: u32, appr_val: u64) -> bool {
    let bound = p.pow(k);
    appr_val < bound
}

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

    #[test]
    fn valuation_basic() {
        assert_eq!(padic_val(2, 8), Some(3));
        assert_eq!(padic_val(3, 9), Some(2));
        assert_eq!(padic_val(5, 7), Some(0));
        assert_eq!(padic_val(2, 0), None);
    }

    #[test]
    fn norm_basic() {
        assert!((padic_norm(2, 4) - 0.25).abs() < 1e-12);
        assert_eq!(padic_norm(2, 0), 0.0);
    }

    #[test]
    fn ultrametric_holds() {
        assert!(check_ultrametric(2, 4, 6));
        assert!(check_ultrametric(3, 9, 27));
    }

    #[test]
    fn appr_bound() {
        assert!(check_appr_bound(2, 3, 7)); // 7 < 8
        assert!(!check_appr_bound(2, 3, 8)); // 8 not < 8
    }
}