// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Padic.UltrametricLightCone
// Theorem preserved: causalBall_convex, isosceles_triangle, mem_causalBall_iff

use crate::valuation::padic_norm;

/// causalBall(center, r) = {x | |x - center|_p ≤ r}
pub fn in_causal_ball(p: u64, center: i64, r: f64, x: i64) -> bool {
    padic_norm(p, x - center) <= r + 1e-12
}

/// Theorem preserved: causalBall_convex
/// x,y ∈ B(c,r) ⟹ |x-y|_p ≤ r
pub fn check_ball_convexity(p: u64, center: i64, r: f64, x: i64, y: i64) -> bool {
    if !in_causal_ball(p, center, r, x) {
        return true; // vacuously true
    }
    if !in_causal_ball(p, center, r, y) {
        return true;
    }
    padic_norm(p, x - y) <= r + 1e-12
}

/// Theorem preserved: isosceles_triangle
/// |q|_p ≠ |r|_p ⟹ |q+r|_p = max(|q|_p, |r|_p)
pub fn check_isosceles(p: u64, q: i64, r: i64) -> bool {
    let nq = padic_norm(p, q);
    let nr = padic_norm(p, r);
    if (nq - nr).abs() < 1e-12 {
        return true; // precondition not met
    }
    let nsum = padic_norm(p, q + r);
    (nsum - nq.max(nr)).abs() < 1e-12
}

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

    #[test]
    fn ball_membership() {
        assert!(in_causal_ball(2, 0, 1.0, 1));
        assert!(in_causal_ball(2, 0, 0.5, 2)); // |2|_2 = 0.5
    }

    #[test]
    fn convexity() {
        assert!(check_ball_convexity(2, 0, 1.0, 1, 3));
    }

    #[test]
    fn isosceles() {
        // |2|_2 = 0.5, |3|_2 = 1.0 — different norms
        assert!(check_isosceles(2, 2, 3));
    }
}