//! PM-bounded scalar saturation operators.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → Rust
//! Source: HeytingLean.Analysis.PMBoundedControl.CompletionOperator

/// Rational saturation: x / (1 + |x| / Q_PM)
///
/// Theorem preserved: sat_rational_bounded — |sat_rational(Q, x)| ≤ Q
/// Theorem preserved: sat_rational_monotone — Monotone(sat_rational Q)
/// Theorem preserved: sat_rational_odd — sat_rational(Q, -x) = -sat_rational(Q, x)
pub fn sat_rational(q_pm: f64, x: f64) -> f64 {
    x / (1.0 + x.abs() / q_pm)
}

/// Tanh saturation: Q_PM * tanh(x / Q_PM)
///
/// Theorem preserved: sat_tanh_bounded — |sat_tanh(Q, x)| ≤ Q
pub fn sat_tanh(q_pm: f64, x: f64) -> f64 {
    q_pm * (x / q_pm).tanh()
}

/// Hard boundary clamp: min(x, Q_PM)
pub fn pm_boundary_clamp(q_pm: f64, x: f64) -> f64 {
    x.min(q_pm)
}

/// PM safe set membership: x ∈ [0, Q_PM]
pub fn in_pm_safe_set(q_pm: f64, x: f64) -> bool {
    x >= 0.0 && x <= q_pm
}

/// Bundled completion operator
pub struct PmCompletion {
    pub q_pm: f64,
    pub sat: fn(f64, f64) -> f64,
}

pub fn rational_completion(q_pm: f64) -> PmCompletion {
    PmCompletion {
        q_pm,
        sat: sat_rational,
    }
}

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

    #[test]
    fn test_sat_rational_bounded() {
        let q = 10.0;
        for &x in &[-100.0, -1.0, 0.0, 1.0, 50.0, 1e6] {
            assert!(sat_rational(q, x).abs() <= q + 1e-12);
        }
    }

    #[test]
    fn test_sat_rational_odd() {
        let q = 5.0;
        for &x in &[0.5, 3.0, 100.0] {
            let diff = (sat_rational(q, -x) + sat_rational(q, x)).abs();
            assert!(diff < 1e-12);
        }
    }

    #[test]
    fn test_sat_rational_monotone() {
        let q = 10.0;
        let xs: Vec<f64> = (-50..=50).map(|i| i as f64 * 0.5).collect();
        for w in xs.windows(2) {
            assert!(sat_rational(q, w[0]) <= sat_rational(q, w[1]) + 1e-12);
        }
    }

    #[test]
    fn test_sat_rational_safe_set() {
        let q = 10.0;
        for &x in &[0.0, 1.0, 5.0, 10.0, 100.0] {
            assert!(in_pm_safe_set(q, sat_rational(q, x)));
        }
    }
}