num-valid 0.3.3

//! Property-based tests using proptest for num-valid.
//!
//! These tests verify mathematical properties that should hold for all valid inputs,
//! not just specific example values. proptest generates hundreds of random inputs
//! and automatically shrinks failing cases to minimal reproducible examples.

use num::{One, Zero};
use num_valid::{
    RealScalar,
    backends::native64::validated::{ComplexNative64StrictFinite, RealNative64StrictFinite},
    functions::{
        ACos, ASin, ATan, Abs, ComplexScalarConstructors, ComplexScalarGetParts, Conjugate, Cos,
        CosH, Exp, Ln, Pow, Reciprocal, Sin, SinH, Sqrt, Tan, TanH,
    },
};
use proptest::prelude::*;

// =============================================================================
// STRATEGY DEFINITIONS
// =============================================================================
// Strategies define how to generate random values for testing.
// We exclude edge cases that would fail validation (NaN, Inf, subnormal).

/// Strategy for generating valid f64 values (finite, non-subnormal).
/// Excludes the "danger zone" near zero where subnormals live.
fn valid_f64() -> impl Strategy<Value = f64> {
    prop_oneof![
        // Normal positive range (avoiding subnormals)
        (f64::MIN_POSITIVE..1e100_f64),
        // Normal negative range
        (-1e100_f64..(-f64::MIN_POSITIVE)),
        // Zero is valid
        Just(0.0),
    ]
}

/// Strategy for positive f64 values (for sqrt, ln, etc.)
fn positive_f64() -> impl Strategy<Value = f64> {
    f64::MIN_POSITIVE..1e100_f64
}

/// Strategy for values in [-1, 1] (for asin, acos)
fn unit_interval() -> impl Strategy<Value = f64> {
    -1.0..=1.0_f64
}

/// Strategy for small positive values (for testing precision)
fn small_positive_f64() -> impl Strategy<Value = f64> {
    1e-10_f64..1e10_f64
}

/// Strategy for angles in a reasonable range (avoiding precision loss at extremes)
fn angle_radians() -> impl Strategy<Value = f64> {
    -100.0..100.0_f64
}

/// Strategy for angles in [-π/2 + ε, π/2 - ε] (for tan domain)
fn tan_safe_angle() -> impl Strategy<Value = f64> {
    let half_pi = std::f64::consts::FRAC_PI_2;
    let epsilon = 0.01; // Stay away from asymptotes
    (-half_pi + epsilon)..(half_pi - epsilon)
}

/// Strategy for generating validated RealNative64StrictFinite
fn validated_real() -> impl Strategy<Value = RealNative64StrictFinite> {
    valid_f64().prop_filter_map("must be valid", |x| {
        RealNative64StrictFinite::try_from_f64(x).ok()
    })
}

/// Strategy for positive validated reals
fn positive_validated_real() -> impl Strategy<Value = RealNative64StrictFinite> {
    positive_f64().prop_filter_map("must be positive valid", |x| {
        RealNative64StrictFinite::try_from_f64(x).ok()
    })
}

// =============================================================================
// ARITHMETIC PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// Addition is commutative: a + b = b + a
    #[test]
    fn prop_add_commutative(a in validated_real(), b in validated_real()) {
        let sum1 = a + b;
        let sum2 = b + a;
        prop_assert_eq!(sum1, sum2);
    }

    /// Multiplication is commutative: a * b = b * a
    #[test]
    fn prop_mul_commutative(a in validated_real(), b in validated_real()) {
        let prod1 = a * b;
        let prod2 = b * a;
        prop_assert_eq!(prod1, prod2);
    }

    /// Addition identity: a + 0 = a
    #[test]
    fn prop_add_identity(a in validated_real()) {
        let zero = RealNative64StrictFinite::zero();
        let result = a + zero;
        prop_assert_eq!(result, a);
    }

    /// Multiplication identity: a * 1 = a
    #[test]
    fn prop_mul_identity(a in validated_real()) {
        let one = RealNative64StrictFinite::one();
        let result = a * one;
        prop_assert_eq!(result, a);
    }

    /// Multiplication by zero: a * 0 = 0
    #[test]
    fn prop_mul_zero(a in validated_real()) {
        let zero = RealNative64StrictFinite::zero();
        let result = a * zero;
        prop_assert_eq!(result, zero);
    }

    /// Subtraction is inverse of addition: (a + b) - b ≈ a
    #[test]
    fn prop_sub_inverse_of_add(
        a in small_positive_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        b in small_positive_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let sum = a + b;
        let result = sum - b;
        let diff = (result - a).abs();
        // Allow for floating-point tolerance
        let tolerance = a.abs() * RealNative64StrictFinite::from_f64(1e-10);
        prop_assert!(diff <= tolerance, "Expected {} ≈ {}, diff = {}", result, a, diff);
    }

    /// Division is inverse of multiplication: (a * b) / b ≈ a (for b ≠ 0)
    #[test]
    fn prop_div_inverse_of_mul(
        a in small_positive_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        b in (1e-5_f64..1e5_f64).prop_filter_map("valid nonzero", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let prod = a * b;
        let result = prod / b;
        let diff = (result - a).abs();
        let tolerance = a.abs() * RealNative64StrictFinite::from_f64(1e-10);
        prop_assert!(diff <= tolerance, "Expected {} ≈ {}, diff = {}", result, a, diff);
    }

    /// Negation is self-inverse: -(-a) = a
    #[test]
    fn prop_neg_self_inverse(a in validated_real()) {
        let double_neg = -(-a);
        prop_assert_eq!(double_neg, a);
    }
}

// =============================================================================
// SQUARE ROOT PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// sqrt(x)² ≈ x for positive x
    #[test]
    fn prop_sqrt_squared(x in positive_validated_real()) {
        let sqrt_x = x.sqrt();
        let squared = sqrt_x * sqrt_x;
        let diff = (squared - x).abs();
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance, "sqrt({})² = {}, expected {}", x, squared, x);
    }

    /// sqrt(a * b) = sqrt(a) * sqrt(b) for positive a, b
    #[test]
    fn prop_sqrt_product(
        a in positive_validated_real(),
        b in positive_validated_real()
    ) {
        // Guard against overflow
        let product_raw = *a.as_ref() * *b.as_ref();
        prop_assume!(product_raw.is_finite() && product_raw > f64::MIN_POSITIVE);

        let product = a * b;
        let sqrt_product = product.sqrt();
        let sqrt_a = a.sqrt();
        let sqrt_b = b.sqrt();
        let product_of_sqrts = sqrt_a * sqrt_b;

        let diff = (sqrt_product - product_of_sqrts).abs();
        let tolerance = product_of_sqrts.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// sqrt(1) = 1
    #[test]
    fn prop_sqrt_one(_dummy in Just(())) {
        let one = RealNative64StrictFinite::one();
        let sqrt_one = one.sqrt();
        prop_assert_eq!(sqrt_one, one);
    }

    /// sqrt(0) = 0
    #[test]
    fn prop_sqrt_zero(_dummy in Just(())) {
        let zero = RealNative64StrictFinite::zero();
        let sqrt_zero = zero.sqrt();
        prop_assert_eq!(sqrt_zero, zero);
    }
}

// =============================================================================
// EXPONENTIAL AND LOGARITHM PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// ln(exp(x)) ≈ x for reasonable x values
    #[test]
    fn prop_ln_exp_inverse(x in (-50.0..50.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let exp_x = x.exp();
        let ln_exp_x = exp_x.ln();
        let diff = (ln_exp_x - x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-12);
        prop_assert!(diff <= tolerance, "ln(exp({})) = {}, expected {}", x, ln_exp_x, x);
    }

    /// exp(ln(x)) ≈ x for positive x
    #[test]
    fn prop_exp_ln_inverse(x in positive_validated_real()) {
        let ln_x = x.ln();
        let exp_ln_x = ln_x.exp();
        let diff = (exp_ln_x - x).abs();
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-12);
        prop_assert!(diff <= tolerance, "exp(ln({})) = {}, expected {}", x, exp_ln_x, x);
    }

    /// exp(a + b) = exp(a) * exp(b)
    #[test]
    fn prop_exp_sum(
        a in (-20.0..20.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        b in (-20.0..20.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let sum = a + b;
        let exp_sum = sum.exp();
        let exp_a = a.exp();
        let exp_b = b.exp();
        let product = exp_a * exp_b;

        let diff = (exp_sum - product).abs();
        let tolerance = product.abs() * RealNative64StrictFinite::from_f64(1e-12);
        prop_assert!(diff <= tolerance);
    }

    /// ln(a * b) = ln(a) + ln(b) for positive a, b
    #[test]
    fn prop_ln_product(
        a in (1e-10_f64..1e10_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        b in (1e-10_f64..1e10_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let product = a * b;
        // Guard against overflow/underflow
        let raw_product = *product.as_ref();
        prop_assume!(raw_product > f64::MIN_POSITIVE && raw_product < 1e100);

        let ln_product = product.ln();
        let ln_a = a.ln();
        let ln_b = b.ln();
        let sum_of_lns = ln_a + ln_b;

        let diff = (ln_product - sum_of_lns).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-12);
        prop_assert!(diff <= tolerance);
    }

    /// exp(0) = 1
    #[test]
    fn prop_exp_zero(_dummy in Just(())) {
        let zero = RealNative64StrictFinite::zero();
        let one = RealNative64StrictFinite::one();
        let exp_zero = zero.exp();
        prop_assert_eq!(exp_zero, one);
    }

    /// ln(1) = 0
    #[test]
    fn prop_ln_one(_dummy in Just(())) {
        let zero = RealNative64StrictFinite::zero();
        let one = RealNative64StrictFinite::one();
        let ln_one = one.ln();
        prop_assert_eq!(ln_one, zero);
    }
}

// =============================================================================
// TRIGONOMETRIC PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// sin²(x) + cos²(x) = 1 (Pythagorean identity)
    #[test]
    fn prop_pythagorean_identity(x in angle_radians().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let sin_x = x.sin();
        let cos_x = x.cos();
        let sin_sq = sin_x * sin_x;
        let cos_sq = cos_x * cos_x;
        let sum = sin_sq + cos_sq;

        let one = RealNative64StrictFinite::one();
        let diff = (sum - one).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance, "sin²({}) + cos²({}) = {}, expected 1", x, x, sum);
    }

    /// sin(-x) = -sin(x) (odd function)
    #[test]
    fn prop_sin_odd(x in angle_radians().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let sin_x = x.sin();
        let sin_neg_x = (-x).sin();
        let neg_sin_x = -sin_x;

        let diff = (sin_neg_x - neg_sin_x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// cos(-x) = cos(x) (even function)
    #[test]
    fn prop_cos_even(x in angle_radians().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let cos_x = x.cos();
        let cos_neg_x = (-x).cos();

        let diff = (cos_x - cos_neg_x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// tan(x) = sin(x) / cos(x)
    #[test]
    fn prop_tan_definition(x in tan_safe_angle().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let tan_x = x.tan();
        let sin_x = x.sin();
        let cos_x = x.cos();
        let ratio = sin_x / cos_x;

        let diff = (tan_x - ratio).abs();
        let tolerance = ratio.abs() * RealNative64StrictFinite::from_f64(1e-12)
            + RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// sin(0) = 0
    #[test]
    fn prop_sin_zero(_dummy in Just(())) {
        let zero = RealNative64StrictFinite::zero();
        let sin_zero = zero.sin();
        prop_assert_eq!(sin_zero, zero);
    }

    /// cos(0) = 1
    #[test]
    fn prop_cos_zero(_dummy in Just(())) {
        let zero = RealNative64StrictFinite::zero();
        let one = RealNative64StrictFinite::one();
        let cos_zero = zero.cos();
        prop_assert_eq!(cos_zero, one);
    }
}

// =============================================================================
// INVERSE TRIGONOMETRIC PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// sin(asin(x)) = x for x ∈ [-1, 1]
    #[test]
    fn prop_sin_asin_inverse(x in unit_interval().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let asin_x = x.asin();
        let sin_asin_x = asin_x.sin();
        let diff = (sin_asin_x - x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// cos(acos(x)) = x for x ∈ [-1, 1]
    #[test]
    fn prop_cos_acos_inverse(x in unit_interval().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let acos_x = x.acos();
        let cos_acos_x = acos_x.cos();
        let diff = (cos_acos_x - x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// tan(atan(x)) = x
    /// Note: For very large x, atan(x) approaches ±π/2, making tan precision-limited
    #[test]
    fn prop_tan_atan_inverse(x in (-1e3_f64..1e3_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let atan_x = x.atan();
        let tan_atan_x = atan_x.tan();
        let diff = (tan_atan_x - x).abs();
        // Relative tolerance with absolute floor for near-zero values
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-12)
            + RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }
}

// =============================================================================
// RECIPROCAL PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// 1 / (1 / x) = x for x ≠ 0
    #[test]
    fn prop_reciprocal_self_inverse(
        x in (1e-100_f64..1e100_f64).prop_filter_map("valid nonzero", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let recip = x.reciprocal();
        let double_recip = recip.reciprocal();
        let diff = (double_recip - x).abs();
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// x * (1/x) = 1 for x ≠ 0
    #[test]
    fn prop_reciprocal_product_one(
        x in (1e-50_f64..1e50_f64).prop_filter_map("valid nonzero", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let recip = x.reciprocal();
        let product = x * recip;
        let one = RealNative64StrictFinite::one();
        let diff = (product - one).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }
}

// =============================================================================
// POWER PROPERTIES (using integer exponents)
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// x^1 = x (using Pow<i32>)
    #[test]
    fn prop_pow_one(x in positive_validated_real()) {
        let x_pow_1: RealNative64StrictFinite = Pow::pow(x, 1_i32);
        let diff = (x_pow_1 - x).abs();
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// x^0 = 1 for x > 0
    #[test]
    fn prop_pow_zero(x in positive_validated_real()) {
        let one = RealNative64StrictFinite::one();
        let x_pow_0: RealNative64StrictFinite = Pow::pow(x, 0_i32);
        prop_assert_eq!(x_pow_0, one);
    }

    /// x^2 = x * x
    #[test]
    fn prop_pow_two_equals_square(x in small_positive_f64().prop_filter_map("valid", |v| RealNative64StrictFinite::try_from_f64(v).ok())) {
        let x_squared: RealNative64StrictFinite = Pow::pow(x, 2_i32);
        let x_times_x = x * x;
        let diff = (x_squared - x_times_x).abs();
        let tolerance = x_times_x.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// x^(-1) = 1/x
    #[test]
    fn prop_pow_neg_one_equals_reciprocal(
        x in (1e-50_f64..1e50_f64).prop_filter_map("valid nonzero", |v| RealNative64StrictFinite::try_from_f64(v).ok())
    ) {
        let x_pow_neg1: RealNative64StrictFinite = Pow::pow(x, -1_i32);
        let x_recip = x.reciprocal();
        let diff = (x_pow_neg1 - x_recip).abs();
        let tolerance = x_recip.abs() * RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// (x^a)^b = x^(a*b) for small integer exponents
    #[test]
    fn prop_pow_of_pow(
        x in (1e-2_f64..1e2_f64).prop_filter_map("valid", |v| RealNative64StrictFinite::try_from_f64(v).ok()),
        a in -2_i32..=2_i32,
        b in -2_i32..=2_i32
    ) {
        // Guard against 0^negative
        prop_assume!(*x.as_ref() > 0.0 || (a >= 0 && b >= 0));

        let x_pow_a: RealNative64StrictFinite = Pow::pow(x, a);
        // Guard against intermediate overflow/underflow
        let raw_pow_a = *x_pow_a.as_ref();
        prop_assume!(raw_pow_a.is_finite() && raw_pow_a.abs() > f64::MIN_POSITIVE);

        let left: RealNative64StrictFinite = Pow::pow(x_pow_a, b);
        let ab = a * b;
        let right: RealNative64StrictFinite = Pow::pow(x, ab);

        // Guard against result overflow/underflow
        let raw_left = *left.as_ref();
        let raw_right = *right.as_ref();
        prop_assume!(raw_left.is_finite() && raw_right.is_finite());
        prop_assume!(raw_left.abs() > f64::MIN_POSITIVE && raw_right.abs() > f64::MIN_POSITIVE);

        let diff = (left - right).abs();
        let tolerance = right.abs() * RealNative64StrictFinite::from_f64(1e-10);
        prop_assert!(diff <= tolerance);
    }
}

// =============================================================================
// COMPLEX NUMBER PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// |z * conj(z)| = |z|² (magnitude property)
    #[test]
    fn prop_complex_magnitude_squared(
        re in (-100.0..100.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        im in (-100.0..100.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let z = ComplexNative64StrictFinite::new_complex(re, im);
        let conj_z = z.conjugate();
        let product = z * conj_z;

        // z * conj(z) should be a positive real number = |z|²
        let magnitude = z.abs();
        let mag_squared = magnitude * magnitude;

        // The real part of z * conj(z) should equal |z|²
        let product_re = product.real_part();
        let diff = (product_re - mag_squared).abs();
        let tolerance = mag_squared.abs() * RealNative64StrictFinite::from_f64(1e-12)
            + RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// conj(conj(z)) = z
    #[test]
    fn prop_conjugate_self_inverse(
        re in valid_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        im in valid_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let z = ComplexNative64StrictFinite::new_complex(re, im);
        let double_conj = z.conjugate().conjugate();
        prop_assert_eq!(double_conj, z);
    }

    /// |z| >= 0 (magnitude is non-negative)
    #[test]
    fn prop_magnitude_non_negative(
        re in valid_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        im in valid_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let z = ComplexNative64StrictFinite::new_complex(re, im);
        let magnitude = z.abs();
        let zero = RealNative64StrictFinite::zero();
        prop_assert!(magnitude >= zero);
    }
}

// =============================================================================
// SERIALIZATION ROUNDTRIP
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// JSON serialization roundtrip: deserialize(serialize(x)) ≈ x
    /// Note: JSON number formatting can have tiny rounding effects at extreme magnitudes
    #[test]
    fn prop_json_roundtrip(x in validated_real()) {
        let json = serde_json::to_string(&x).unwrap();
        let deserialized: RealNative64StrictFinite = serde_json::from_str(&json).unwrap();
        // Use relative tolerance for very large/small numbers
        let diff = (deserialized - x).abs();
        let tolerance = x.abs() * RealNative64StrictFinite::from_f64(1e-14)
            + RealNative64StrictFinite::from_f64(1e-300); // tiny absolute tolerance for near-zero
        prop_assert!(diff <= tolerance, "JSON roundtrip: {} != {}, diff = {}", deserialized, x, diff);
    }

    /// Conversion roundtrip: try_from_f64(*x.as_ref()) == Ok(x)
    #[test]
    fn prop_f64_conversion_roundtrip(x in validated_real()) {
        let raw = *x.as_ref();
        let back = RealNative64StrictFinite::try_from_f64(raw).unwrap();
        prop_assert_eq!(back, x);
    }
}

// =============================================================================
// ORDERING AND COMPARISON PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// Transitivity: if a < b and b < c, then a < c
    #[test]
    fn prop_ordering_transitive(
        a in small_positive_f64().prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        delta1 in (1e-10_f64..1.0).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok()),
        delta2 in (1e-10_f64..1.0).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())
    ) {
        let b = a + delta1;
        let c = b + delta2;
        prop_assert!(a < b);
        prop_assert!(b < c);
        prop_assert!(a < c); // Transitivity
    }

    /// Antisymmetry: a <= b and b <= a implies a == b
    #[test]
    fn prop_ordering_antisymmetric(a in validated_real()) {
        let b = a;
        prop_assert!(a <= b);
        prop_assert!(b <= a);
        prop_assert_eq!(a, b);
    }

    /// Totality: either a <= b or b <= a (or both)
    #[test]
    fn prop_ordering_total(a in validated_real(), b in validated_real()) {
        prop_assert!(a <= b || b <= a);
    }
}

// =============================================================================
// ABSOLUTE VALUE PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// |x| >= 0
    #[test]
    fn prop_abs_non_negative(x in validated_real()) {
        let abs_x = x.abs();
        let zero = RealNative64StrictFinite::zero();
        prop_assert!(abs_x >= zero);
    }

    /// |x| = |-x|
    #[test]
    fn prop_abs_symmetric(x in validated_real()) {
        let abs_x = x.abs();
        let abs_neg_x = (-x).abs();
        prop_assert_eq!(abs_x, abs_neg_x);
    }

    /// |x * y| = |x| * |y|
    #[test]
    fn prop_abs_multiplicative(
        x in small_positive_f64().prop_filter_map("valid", |v| RealNative64StrictFinite::try_from_f64(v).ok()),
        y in small_positive_f64().prop_filter_map("valid", |v| RealNative64StrictFinite::try_from_f64(v).ok())
    ) {
        // Use both positive and negative variants
        let x_neg = -x;
        let y_neg = -y;

        // Test all combinations
        for (a, b) in [(x, y), (x, y_neg), (x_neg, y), (x_neg, y_neg)] {
            let product = a * b;
            let abs_product = product.abs();
            let abs_a = a.abs();
            let abs_b = b.abs();
            let product_of_abs = abs_a * abs_b;

            let diff = (abs_product - product_of_abs).abs();
            let tolerance = product_of_abs.abs() * RealNative64StrictFinite::from_f64(1e-14);
            prop_assert!(diff <= tolerance);
        }
    }
}

// =============================================================================
// HYPERBOLIC FUNCTION PROPERTIES
// =============================================================================

proptest! {
    #![proptest_config(ProptestConfig::with_cases(500))]

    /// cosh²(x) - sinh²(x) = 1 (hyperbolic identity)
    /// Note: For larger |x|, cosh and sinh grow exponentially, so relative error accumulates
    #[test]
    fn prop_hyperbolic_identity(x in (-4.0..4.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let sinh_x = x.sinh();
        let cosh_x = x.cosh();
        let sinh_sq = sinh_x * sinh_x;
        let cosh_sq = cosh_x * cosh_x;
        let diff_sq = cosh_sq - sinh_sq;

        let one = RealNative64StrictFinite::one();
        let diff = (diff_sq - one).abs();
        // At x=4, cosh(4)≈27.3, cosh²≈745, typical f64 epsilon is ~2e-16, so error ~1e-13
        let tolerance = RealNative64StrictFinite::from_f64(1e-12);
        prop_assert!(diff <= tolerance, "cosh²({}) - sinh²({}) = {}, expected 1", x, x, diff_sq);
    }

    /// sinh(-x) = -sinh(x) (odd function)
    #[test]
    fn prop_sinh_odd(x in (-10.0..10.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let sinh_x = x.sinh();
        let sinh_neg_x = (-x).sinh();
        let neg_sinh_x = -sinh_x;

        let diff = (sinh_neg_x - neg_sinh_x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// cosh(-x) = cosh(x) (even function)
    #[test]
    fn prop_cosh_even(x in (-10.0..10.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let cosh_x = x.cosh();
        let cosh_neg_x = (-x).cosh();

        let diff = (cosh_x - cosh_neg_x).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }

    /// tanh(x) = sinh(x) / cosh(x)
    #[test]
    fn prop_tanh_definition(x in (-10.0..10.0_f64).prop_filter_map("valid", |x| RealNative64StrictFinite::try_from_f64(x).ok())) {
        let tanh_x = x.tanh();
        let sinh_x = x.sinh();
        let cosh_x = x.cosh();
        let ratio = sinh_x / cosh_x;

        let diff = (tanh_x - ratio).abs();
        let tolerance = RealNative64StrictFinite::from_f64(1e-14);
        prop_assert!(diff <= tolerance);
    }
}