//! Soft transition gate for PM-bounded control.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → Rust
//! Source: HeytingLean.Analysis.PMBoundedControl.SoftTransition

/// Clamp to [0,1]
///
/// Theorem preserved: clamp01_mem_unit_interval
pub fn clamp01(x: f64) -> f64 {
    x.clamp(0.0, 1.0)
}

/// Gate weight: monotone ω ∈ [0,1], 0 when safe, 1 when critical
///
/// Theorem preserved: gate_in_unit_interval
pub fn gate_weight(q: f64, q_pm: f64, eps: f64) -> f64 {
    clamp01((q - (q_pm - eps)) / eps)
}

/// Convex blend: (1-ω)*classical + ω*completed
///
/// Theorem preserved: blended_bounded
/// Theorem preserved: blended_classical_when_safe
/// Theorem preserved: blended_completed_when_critical
pub fn blended_update(omega: f64, classical: f64, completed: f64) -> f64 {
    (1.0 - omega) * classical + omega * completed
}

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

    #[test]
    fn test_gate_in_unit_interval() {
        for &q in &[0.0, 5.0, 9.5, 10.0, 15.0] {
            let w = gate_weight(q, 10.0, 1.0);
            assert!(w >= 0.0 && w <= 1.0);
        }
    }

    #[test]
    fn test_blended_classical_when_safe() {
        let w = gate_weight(5.0, 10.0, 1.0);
        assert!((w - 0.0).abs() < 1e-12);
        let b = blended_update(w, 42.0, 99.0);
        assert!((b - 42.0).abs() < 1e-12);
    }

    #[test]
    fn test_blended_completed_when_critical() {
        let w = gate_weight(10.0, 10.0, 1.0);
        assert!((w - 1.0).abs() < 1e-12);
        let b = blended_update(w, 42.0, 7.0);
        assert!((b - 7.0).abs() < 1e-12);
    }
}