//! τ-Progression and effective step control.
//!
//! Provenance: Lean 4 → LambdaIR → MiniC → Rust
//! Source: HeytingLean.Analysis.PMBoundedControl.TauProgression

/// Progression density: 1 + (Q/Q_PM) / max(ε, 1 - Q/Q_PM)
///
/// Theorem preserved: progression_density_ge_one
pub fn progression_density(q: f64, q_pm: f64, eps: f64) -> f64 {
    let ratio = q / q_pm;
    let denom = eps.max(1.0 - ratio);
    1.0 + ratio / denom
}

/// Effective step size after τ-dilation: Δσ / ρ
///
/// Theorem preserved: effective_step_le_external
/// Theorem preserved: effective_step_vanishes_of_large_density
pub fn effective_step(delta_sigma: f64, rho: f64) -> f64 {
    delta_sigma / rho
}

/// One-step completed update: u + Δσ_eff * (L(u) + N_PM(u))
pub fn completed_update(u: f64, l_u: f64, n_pm_u: f64, delta_sigma_eff: f64) -> f64 {
    u + delta_sigma_eff * (l_u + n_pm_u)
}

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

    #[test]
    fn test_progression_density_ge_one() {
        for &q in &[0.0, 1.0, 5.0, 9.0] {
            assert!(progression_density(q, 10.0, 0.01) >= 1.0);
        }
    }

    #[test]
    fn test_effective_step_le_external() {
        let ds = 0.1;
        let rho = progression_density(8.0, 10.0, 0.01);
        assert!(effective_step(ds, rho) <= ds + 1e-12);
    }
}