/// Penumbra: Completion Operator — Layer 7
/// Provenance: Lean 4 → LambdaIR → MiniC → C → Safe Rust
/// Source: HeytingLean/Analysis/PMBoundedControl/CompletionOperator.lean

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

/// Tanh saturation: Q * tanh(x/Q)
pub fn sat_tanh(q_pm: f64, x: f64) -> f64 {
    q_pm * (x / q_pm).tanh()
}

/// Check if x is in the PM safe set [0, Q_PM]
pub fn in_safe_set(q_pm: f64, x: f64) -> bool {
    x >= 0.0 && x <= q_pm
}

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

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

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

    #[test]
    fn sat_tanh_bounded() {
        let q = 10.0;
        for &x in &[-100.0, -1.0, 0.0, 1.0, 100.0] {
            assert!(sat_tanh(q, x).abs() <= q + 1e-10);
        }
    }
}