/// Lean 4 → Safe Rust transpilation
/// Source: HeytingLean.HossenfelderNoGo.Spacetime
/// Provenance: Apoth3osis verified transpilation pipeline

/// A spacetime displacement in 1+1-dimensional Minkowski space.
#[derive(Debug, Clone, Copy, PartialEq)]
pub struct SpacetimeDisplacement {
    pub delta_t: f64,
    pub delta_x: f64,
}

/// The Minkowski interval (proper length squared) with spacelike-positive sign convention.
pub fn minkowski_interval(d: &SpacetimeDisplacement) -> f64 {
    -d.delta_t * d.delta_t + d.delta_x * d.delta_x
}

/// Check if a displacement lies on hyperbolaAt(alpha).
pub fn in_hyperbola_at(alpha: f64, d: &SpacetimeDisplacement) -> bool {
    (minkowski_interval(d) - alpha).abs() < 1e-12
}

/// A Lorentz boost parameterized by rapidity.
#[derive(Debug, Clone, Copy)]
pub struct LorentzBoost {
    pub rapidity: f64,
}

impl LorentzBoost {
    /// Apply a Lorentz boost to a spacetime displacement.
    pub fn apply(&self, d: &SpacetimeDisplacement) -> SpacetimeDisplacement {
        SpacetimeDisplacement {
            delta_t: d.delta_t * self.rapidity.cosh() + d.delta_x * self.rapidity.sinh(),
            delta_x: d.delta_t * self.rapidity.sinh() + d.delta_x * self.rapidity.cosh(),
        }
    }
}

/// Product norm on R x R: max(|a|, |b|).
pub fn product_norm(a: f64, b: f64) -> f64 {
    a.abs().max(b.abs())
}

/// Theorem preserved: hyperbola_infinite_length
/// For any alpha != 0 and any bound L, construct a point on hyperbolaAt(alpha) with norm > L.
pub fn hyperbola_witness_norm(alpha: f64, bound: f64) -> f64 {
    if alpha == 0.0 {
        return 0.0;
    }
    let big_b = bound.max(0.0) + 1.0;
    if alpha > 0.0 {
        let r = alpha.sqrt();
        let eta = (2.0 * big_b / r).ln();
        let dt = r * eta.sinh();
        let dx = r * eta.cosh();
        product_norm(dt, dx)
    } else {
        let r = (-alpha).sqrt();
        let eta = (2.0 * big_b / r).ln();
        let dt = r * eta.cosh();
        let dx = r * eta.sinh();
        product_norm(dt, dx)
    }
}

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

    #[test]
    fn test_minkowski_interval_spacelike() {
        let d = SpacetimeDisplacement { delta_t: 0.0, delta_x: 1.0 };
        assert!((minkowski_interval(&d) - 1.0).abs() < 1e-12);
    }

    #[test]
    fn test_minkowski_interval_timelike() {
        let d = SpacetimeDisplacement { delta_t: 1.0, delta_x: 0.0 };
        assert!((minkowski_interval(&d) - (-1.0)).abs() < 1e-12);
    }

    #[test]
    fn test_boost_preserves_interval() {
        let d = SpacetimeDisplacement { delta_t: 3.0, delta_x: 5.0 };
        let boost = LorentzBoost { rapidity: 1.5 };
        let boosted = boost.apply(&d);
        let orig = minkowski_interval(&d);
        let after = minkowski_interval(&boosted);
        assert!((orig - after).abs() < 1e-10);
    }

    #[test]
    fn test_hyperbola_witness_exceeds_bound() {
        for alpha in [1.0, -1.0, 0.5, -3.0] {
            for bound in [10.0, 100.0, 1000.0] {
                let norm = hyperbola_witness_norm(alpha, bound);
                assert!(norm > bound, "alpha={alpha}, bound={bound}, norm={norm}");
            }
        }
    }

    #[test]
    fn test_product_norm() {
        assert!((product_norm(3.0, -5.0) - 5.0).abs() < 1e-12);
        assert!((product_norm(-7.0, 2.0) - 7.0).abs() < 1e-12);
    }
}