clinlat 0.3.0

//! SOFA-3 respiratory component (PaO₂/FiO₂ ratio) deduction operator.
//!
//! Implements diagnostic scoring for respiratory distress severity in sepsis.
//! Based on Sepsis-3 definitions (Singer et al. 2016, JAMA).
//!
//! Reference: Vincent et al. (1996) on SOFA scoring; Singer et al. (2016) on Sepsis-3.

use crate::{AbstainReason, Hyp, Operator, Outcome};

// SOFA respiratory score thresholds (PaO₂/FiO₂ ratio in mmHg).
//
// Implements task 2.1: Encode SOFA respiratory thresholds per Sepsis-3.
const SOFA_SCORE_0_MIN: f64 = 400.0; // ≥400: score 0 (no respiratory dysfunction)
const SOFA_SCORE_1_MIN: f64 = 300.0; // 300–399: score 1
const SOFA_SCORE_2_MIN: f64 = 200.0; // 200–299: score 2
const SOFA_SCORE_3_MIN: f64 = 100.0; // 100–199: score 3 (requires mechanical ventilation)
// <100: score 4 (requires mechanical ventilation)

/// Evidence for SOFA respiratory scoring.
///
/// Implements task 2.2: Evidence type for SOFA respiratory component.
/// Carries:
/// - `pao2`: Arterial oxygen partial pressure (mmHg)
/// - `fio2`: Fraction of inspired oxygen (0.0–1.0)
/// - `on_mech_vent`: Whether patient is on mechanical ventilation
///
/// Note: The mechanical ventilation flag is required because Sepsis-3 defines
/// scores 3 and 4 only for intubated patients.
#[derive(Clone, Copy, Debug, PartialEq)]
pub struct SofaRespEvidence {
    pub pao2: f64,
    pub fio2: f64,
    pub on_mech_vent: bool,
}

impl SofaRespEvidence {
    /// Creates a new SOFA respiratory evidence entry.
    pub fn new(pao2: f64, fio2: f64, on_mech_vent: bool) -> Self {
        SofaRespEvidence {
            pao2,
            fio2,
            on_mech_vent,
        }
    }

    /// Computes the PaO₂/FiO₂ ratio.
    ///
    /// Returns `None` if FiO₂ is zero or negative (invalid).
    pub fn pao2_fio2_ratio(&self) -> Option<f64> {
        if self.fio2 > 0.0 {
            Some(self.pao2 / self.fio2)
        } else {
            None
        }
    }
}

/// SOFA respiratory hypothesis variants.
///
/// Implements task 2.3: Hypothesis space for SOFA respiratory.
/// Variants represent different severity levels:
/// - `Unknown`: No diagnosis yet (top element in refinement order).
/// - `Score{N}`: SOFA score 0–4, from mild to severe respiratory dysfunction.
///
/// Refinement order: `Unknown` ⊐ each `Score{N}` (Unknown is least specific).
/// Compatibility: each `Score{N}` is compatible only with itself and `Unknown`.
#[derive(Clone, Copy, Debug, Eq, PartialEq)]
pub enum SofaRespHypothesis {
    Unknown,
    Score0,
    Score1,
    Score2,
    Score3,
    Score4,
}

impl SofaRespHypothesis {
    /// Returns the SOFA score as an integer (0–4), or `None` for `Unknown`.
    pub fn score(&self) -> Option<u8> {
        match self {
            SofaRespHypothesis::Unknown => None,
            SofaRespHypothesis::Score0 => Some(0),
            SofaRespHypothesis::Score1 => Some(1),
            SofaRespHypothesis::Score2 => Some(2),
            SofaRespHypothesis::Score3 => Some(3),
            SofaRespHypothesis::Score4 => Some(4),
        }
    }
}

/// The SOFA-3 respiratory deduction operator.
///
/// Implements task 2.3: Operator that maps PaO₂/FiO₂ evidence to SOFA respiratory score.
/// Enforces version-respecting derivation chains (INV-PS-05) by validating that input
/// evidence provenance version matches the operator version before refining.
///
/// Logic:
/// 1. Extract PaO₂/FiO₂ observations from Evidence.
/// 2. Validate input provenance version matches operator version; abstain if mismatch.
/// 3. Compute PaO₂/FiO₂ ratio; abstain if FiO₂ ≤ 0 (insufficient evidence).
/// 4. Map ratio to SOFA score (0–4).
/// 5. If score ≥ 3 but patient is not on mechanical ventilation, abstain (precondition unmet).
/// 6. Create refined Hyp with SOFA-score atoms and updated provenance.
pub struct SofaRespOperator {
    /// The version of this operator (e.g., "0.2.0", "0.3.0").
    /// Per INV-PS-05, output provenance.version must equal this value.
    pub version: String,
}

impl SofaRespOperator {
    /// Create a new SOFA respiratory operator with a given version.
    pub fn new(version: impl Into<String>) -> Self {
        SofaRespOperator {
            version: version.into(),
        }
    }

    /// Creates a SOFA respiratory operator with default version "0.2.0".
    pub fn default_v0_2() -> Self {
        Self::new("0.2.0")
    }

    /// Extract PaO₂ and FiO₂ values from observations.
    ///
    /// Looks for observations with codes matching LOINC PaO₂ (2703-7) and FiO₂ (3150-0).
    /// Returns `(Option<pao2>, Option<fio2>, on_mech_vent)`.
    fn extract_pao2_fio2(evidence: &crate::operator::Evidence) -> (Option<f64>, Option<f64>, bool) {
        let mut pao2 = None;
        let mut fio2 = None;
        let mut on_mech_vent = false;

        for obs in &evidence.observations {
            match obs.code.as_str() {
                "LOINC:2703-7" => {
                    // PaO₂ (partial pressure of oxygen, arterial)
                    if let Some(val) = obs.value.as_f64() {
                        pao2 = Some(val);
                    }
                }
                "LOINC:3150-0" => {
                    // FiO₂ (fraction of inspired oxygen)
                    if let Some(val) = obs.value.as_f64() {
                        fio2 = Some(val);
                    }
                }
                "SNOMED:243144002" => {
                    // Patient on mechanical ventilation (SNOMED code)
                    on_mech_vent = obs.value.as_bool().unwrap_or(false);
                }
                _ => {}
            }
        }

        (pao2, fio2, on_mech_vent)
    }

    /// Compute SOFA respiratory score from PaO₂/FiO₂ ratio and ventilation status.
    ///
    /// Returns a SNOMED-like atom representing the SOFA score, tagged with this operator's version.
    /// Per INV-PS-05, the atom version must match self.version to maintain provenance closure.
    fn score_to_atom(&self, score: u8) -> crate::Atom {
        let (code, preferred_term) = match score {
            0 => ("SNOMED:clinlat-sofa-resp-0", "SOFA respiratory score 0"),
            1 => ("SNOMED:clinlat-sofa-resp-1", "SOFA respiratory score 1"),
            2 => ("SNOMED:clinlat-sofa-resp-2", "SOFA respiratory score 2"),
            3 => ("SNOMED:clinlat-sofa-resp-3", "SOFA respiratory score 3"),
            4 => ("SNOMED:clinlat-sofa-resp-4", "SOFA respiratory score 4"),
            _ => unreachable!(),
        };

        crate::Atom {
            system: crate::OntologySystem::SNOMED,
            code: code.to_string(),
            preferred_term: preferred_term.to_string(),
            version: self.version.clone(),
        }
    }
}

impl Operator for SofaRespOperator {
    fn apply(&self, h: &Hyp, e: &crate::operator::Evidence) -> Outcome<Hyp, AbstainReason> {
        use crate::Ver;

        // Check version invariant: input provenance version must match operator version.
        // Per INV-PS-05, we don't silently change versions; we abstain instead.
        let expected_ver = Ver::new("clinlat", "sofa_resp", &self.version);
        if e.provenance.version != expected_ver {
            return Outcome::Abstain(AbstainReason::OperatorPreconditionUnmet(
                "SOFA respiratory operator version mismatch; operator version does not match evidence provenance version",
            ));
        }

        // Extract PaO₂, FiO₂, and mechanical ventilation status from observations.
        let (pao2_opt, fio2_opt, on_mech_vent) = Self::extract_pao2_fio2(e);

        let pao2 = match pao2_opt {
            Some(val) => val,
            None => {
                return Outcome::Abstain(AbstainReason::InsufficientEvidence(
                    "PaO₂ (LOINC:2703-7) not found in observations",
                ));
            }
        };

        let fio2 = match fio2_opt {
            Some(val) => val,
            None => {
                return Outcome::Abstain(AbstainReason::InsufficientEvidence(
                    "FiO₂ (LOINC:3150-0) not found in observations",
                ));
            }
        };

        // Compute PaO₂/FiO₂ ratio; abstain if FiO₂ ≤ 0.
        if fio2 <= 0.0 {
            return Outcome::Abstain(AbstainReason::InsufficientEvidence("FiO₂ must be > 0"));
        }

        let ratio = pao2 / fio2;

        // Map ratio to SOFA score.
        let score = if ratio >= SOFA_SCORE_0_MIN {
            0
        } else if ratio >= SOFA_SCORE_1_MIN {
            1
        } else if ratio >= SOFA_SCORE_2_MIN {
            2
        } else if ratio >= SOFA_SCORE_3_MIN {
            3
        } else {
            4
        };

        // Sepsis-3: Scores 3 and 4 require mechanical ventilation.
        // This is a precondition requirement, not insufficient evidence.
        if score >= 3 && !on_mech_vent {
            return Outcome::Abstain(AbstainReason::OperatorPreconditionUnmet(
                "SOFA respiratory score ≥3 requires mechanical ventilation; patient not on ventilation",
            ));
        }

        // Create refined hypothesis by appending SOFA score atom to input atoms.
        // Per INV-PS-03 (operator monotonicity), output must refine input: δ(h,e) ⊑ h.
        // This is achieved by including all input atoms plus the new SOFA atom.
        let sofa_atom = self.score_to_atom(score);
        let mut refined_atoms = h.atoms().to_vec();
        refined_atoms.push(sofa_atom);
        let refined_hyp = Hyp::new(refined_atoms);

        // Verify monotonicity: refined_hyp should have strictly more atoms (unless h was Unknown),
        // ensuring refined_hyp ⊑ h per the refinement order.
        debug_assert!(
            refined_hyp <= *h,
            "operator output must refine input: {:?} ⊑ {:?}",
            refined_hyp.atoms(),
            h.atoms()
        );

        Outcome::Refined(refined_hyp)
    }
}

/// Standalone helper that maps a PaO₂/FiO₂ ratio to a SOFA respiratory score.
///
/// This is a thin numeric helper exposed for callers that only need the scoring
/// rule in isolation (e.g., bench tooling, exploratory analysis). The full
/// substrate API path is [`SofaRespOperator::apply`], which validates evidence
/// provenance, enforces the version invariant (INV-PS-05), and returns a typed
/// [`crate::Outcome`].
///
/// # Arguments
///
/// - `ratio`: PaO₂/FiO₂ ratio in mmHg.
/// - `on_mech_vent`: Whether the patient is on mechanical ventilation.
///
/// # Returns
///
/// - `Some(score)`: The computed SOFA respiratory score (0–4).
/// - `None`: If preconditions are unmet (score ≥3 requires mechanical ventilation
///   per Sepsis-3).
pub fn score_from_ratio(ratio: f64, on_mech_vent: bool) -> Option<u8> {
    let score = if ratio >= SOFA_SCORE_0_MIN {
        0
    } else if ratio >= SOFA_SCORE_1_MIN {
        1
    } else if ratio >= SOFA_SCORE_2_MIN {
        2
    } else if ratio >= SOFA_SCORE_3_MIN {
        3
    } else {
        4
    };

    // Sepsis-3: Scores 3 and 4 require mechanical ventilation.
    if score >= 3 && !on_mech_vent {
        return None;
    }

    Some(score)
}

#[cfg(test)]
mod tests {
    use super::*;
    use chrono::Utc;
    use std::collections::BTreeMap;

    // Helper functions for tests
    fn test_provenance_v0_2() -> crate::Provenance {
        let origin = crate::ProvenanceOrigin::new("external_lab_api", "LOINC", "2703-7");
        let metadata = BTreeMap::new();
        crate::Provenance::new(
            origin,
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            metadata,
        )
    }

    fn test_evidence_pao2_fio2(pao2: f64, fio2: f64, on_vent: bool) -> crate::Evidence {
        let mut observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(pao2)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(fio2)),
        ];
        if on_vent {
            observations.push(crate::Observation::new(
                "SNOMED:243144002",
                serde_json::json!(true),
            ));
        }
        crate::Evidence::new(observations, test_provenance_v0_2())
    }

    // Original helper tests
    #[test]
    fn test_pao2_fio2_ratio_valid() {
        let evidence = SofaRespEvidence::new(350.0, 1.0, false);
        assert_eq!(evidence.pao2_fio2_ratio(), Some(350.0));
    }

    #[test]
    fn test_pao2_fio2_ratio_zero_fio2() {
        let evidence = SofaRespEvidence::new(350.0, 0.0, false);
        assert_eq!(evidence.pao2_fio2_ratio(), None);
    }

    #[test]
    fn test_pao2_fio2_ratio_negative_fio2() {
        let evidence = SofaRespEvidence::new(350.0, -0.5, false);
        assert_eq!(evidence.pao2_fio2_ratio(), None);
    }

    #[test]
    fn test_score_from_ratio_score0() {
        let ratio = 400.0;
        assert_eq!(score_from_ratio(ratio, false), Some(0));
    }

    #[test]
    fn test_score_from_ratio_score1() {
        let ratio = 350.0;
        assert_eq!(score_from_ratio(ratio, false), Some(1));
    }

    #[test]
    fn test_score_from_ratio_score2() {
        let ratio = 250.0;
        assert_eq!(score_from_ratio(ratio, false), Some(2));
    }

    #[test]
    fn test_score_from_ratio_score3_with_vent() {
        let ratio = 150.0;
        assert_eq!(score_from_ratio(ratio, true), Some(3));
    }

    #[test]
    fn test_score_from_ratio_score3_without_vent() {
        let ratio = 150.0;
        // Score 3 requires mechanical ventilation; abstain if not ventilated.
        assert_eq!(score_from_ratio(ratio, false), None);
    }

    #[test]
    fn test_score_from_ratio_score4_with_vent() {
        let ratio = 80.0;
        assert_eq!(score_from_ratio(ratio, true), Some(4));
    }

    #[test]
    fn test_score_from_ratio_score4_without_vent() {
        let ratio = 80.0;
        // Score 4 requires mechanical ventilation.
        assert_eq!(score_from_ratio(ratio, false), None);
    }

    #[test]
    fn test_sofa_resp_hypothesis_score() {
        assert_eq!(SofaRespHypothesis::Unknown.score(), None);
        assert_eq!(SofaRespHypothesis::Score0.score(), Some(0));
        assert_eq!(SofaRespHypothesis::Score1.score(), Some(1));
        assert_eq!(SofaRespHypothesis::Score2.score(), Some(2));
        assert_eq!(SofaRespHypothesis::Score3.score(), Some(3));
        assert_eq!(SofaRespHypothesis::Score4.score(), Some(4));
    }

    // New tests for SofaRespOperator with Evidence and Provenance (task 2.3)

    #[test]
    fn test_sofa_operator_creation() {
        let op = SofaRespOperator::new("0.2.0");
        assert_eq!(op.version, "0.2.0");

        let op_default = SofaRespOperator::default_v0_2();
        assert_eq!(op_default.version, "0.2.0");
    }

    #[test]
    fn test_sofa_operator_score0() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(450.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));

        if let Outcome::Refined(h) = result {
            assert!(!h.atoms().is_empty());
        }
    }

    #[test]
    fn test_sofa_operator_score1() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(350.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));
    }

    #[test]
    fn test_sofa_operator_score2() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(250.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));
    }

    #[test]
    fn test_sofa_operator_score3_with_ventilation() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(150.0, 1.0, true);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));
    }

    #[test]
    fn test_sofa_operator_score3_without_ventilation_abstains() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(150.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Abstain(_)));
    }

    #[test]
    fn test_sofa_operator_missing_pao2_abstains() {
        let op = SofaRespOperator::default_v0_2();
        let observations = vec![crate::Observation::new(
            "LOINC:3150-0",
            serde_json::json!(1.0),
        )];
        let evidence = crate::Evidence::new(observations, test_provenance_v0_2());
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Abstain(_)));
    }

    #[test]
    fn test_sofa_operator_missing_fio2_abstains() {
        let op = SofaRespOperator::default_v0_2();
        let observations = vec![crate::Observation::new(
            "LOINC:2703-7",
            serde_json::json!(350.0),
        )];
        let evidence = crate::Evidence::new(observations, test_provenance_v0_2());
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Abstain(_)));
    }

    #[test]
    fn test_sofa_operator_zero_fio2_abstains() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(350.0, 0.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Abstain(_)));
    }

    #[test]
    fn test_sofa_operator_version_mismatch_abstains() {
        let op = SofaRespOperator::new("0.3.0"); // Different version
        let evidence = test_evidence_pao2_fio2(350.0, 1.0, false); // Has v0.2.0 provenance
        let hyp = Hyp::unknown();

        // Version mismatch: operator v0.3.0 but evidence is from v0.2.0
        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Abstain(_)));

        if let Outcome::Abstain(reason) = result {
            assert!(reason.message().contains("version mismatch"));
        }
    }

    #[test]
    fn test_sofa_operator_version_invariant() {
        // Property test: if operator succeeds, output provenance has correct version
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(350.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        if let Outcome::Refined(refined_hyp) = result {
            // The atoms in the refined hypothesis should have atoms from the SOFA score
            assert!(!refined_hyp.atoms().is_empty());
            // Verify the atoms have the expected version
            for atom in refined_hyp.atoms() {
                assert_eq!(atom.system, crate::OntologySystem::SNOMED);
                assert!(atom.code.contains("clinlat-sofa-resp"));
            }
        }
    }

    #[test]
    fn test_sofa_operator_score_boundary_400_is_score0() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(400.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));
    }

    #[test]
    fn test_sofa_operator_score_boundary_399_is_score1() {
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(399.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(matches!(result, Outcome::Refined(_)));
    }

    #[test]
    fn test_sofa_operator_score_boundary_300_exactly() {
        // Test the exact boundary at 300.0 (transition from score 1 to score 2)
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(300.0, 1.0, false);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(
            matches!(result, Outcome::Refined(_)),
            "ratio=300.0 should produce a score (either 1 or 2)"
        );
    }

    #[test]
    fn test_sofa_operator_score_boundary_200_exactly() {
        // Test the exact boundary at 200.0 (transition from score 2 to score 3)
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(200.0, 1.0, true); // score 3 requires ventilation
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(
            matches!(result, Outcome::Refined(_)),
            "ratio=200.0 should produce a score (either 2 or 3)"
        );
    }

    #[test]
    fn test_sofa_operator_score_boundary_100_exactly() {
        // Test the exact boundary at 100.0 (transition from score 3 to score 4)
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(100.0, 1.0, true); // score 3/4 require ventilation
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        assert!(
            matches!(result, Outcome::Refined(_)),
            "ratio=100.0 should produce a score (either 3 or 4)"
        );
    }

    #[test]
    fn test_sofa_operator_monotonicity_preserved() {
        // Property: δ(h, e) ⊑ h (operator output refines input per INV-PS-03)
        let op = SofaRespOperator::default_v0_2();
        let evidence = test_evidence_pao2_fio2(350.0, 1.0, false);

        // Test 1: apply to Unknown should produce a more specific hypothesis
        let h_unknown = Hyp::unknown();
        let result_unknown = op.apply(&h_unknown, &evidence);
        if let Outcome::Refined(refined) = result_unknown {
            // refined ⊑ unknown (refined is more specific)
            assert_eq!(
                refined.partial_cmp(&h_unknown),
                Some(std::cmp::Ordering::Less)
            );
        }

        // Test 2: apply to a concrete hypothesis should preserve input atoms
        let atom_a = crate::Atom {
            system: crate::OntologySystem::SNOMED,
            code: "67822003".to_string(),
            preferred_term: "Hypoxemia".to_string(),
            version: "0.2.0".to_string(),
        };
        let h_concrete = Hyp::new(vec![atom_a.clone()]);
        let result_concrete = op.apply(&h_concrete, &evidence);
        if let Outcome::Refined(refined) = result_concrete {
            // refined should contain all atoms from h_concrete plus the SOFA atom
            let refined_atoms: std::collections::HashSet<_> =
                refined.atoms().iter().cloned().collect();
            assert!(
                refined_atoms.contains(&atom_a),
                "refined hypothesis should preserve input atoms"
            );
            // refined ⊑ h_concrete (refined is more specific or equal)
            assert!(
                refined <= h_concrete,
                "operator must preserve refinement order"
            );
        }
    }

    #[test]
    fn test_sofa_operator_version_consistency() {
        // Property: atoms emitted by operator carry operator version (INV-PS-05)
        let version = "0.3.0";
        let op = SofaRespOperator::new(version);

        // Create evidence with matching version
        let origin = crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7");
        let metadata = BTreeMap::new();
        let prov = crate::Provenance::new(
            origin,
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", version),
            metadata,
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(350.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        let hyp = Hyp::unknown();

        let result = op.apply(&hyp, &evidence);
        if let Outcome::Refined(refined) = result {
            // All atoms should have the operator's version string
            for atom in refined.atoms() {
                assert_eq!(
                    atom.version, version,
                    "operator atoms should use operator version, not hardcoded string"
                );
            }
        }
    }

    // Property test suite (≥21 cases via iteration over ranges)
    // Instead of proptest! macro, we use simple loops to test multiple values

    #[test]
    fn prop_score_boundaries_all_bands() {
        // Test that each ratio falls into the correct SOFA band
        let test_cases = vec![
            (500.0, Some(0)), // ≥400
            (400.0, Some(0)), // boundary
            (399.0, Some(1)), // just below boundary
            (350.0, Some(1)), // 300-399
            (300.0, Some(1)), // boundary
            (299.0, Some(2)), // just below
            (250.0, Some(2)), // 200-299
            (200.0, Some(2)), // boundary
            (199.0, Some(3)), // just below (with vent)
            (150.0, Some(3)), // 100-199 (with vent)
            (100.0, Some(3)), // boundary (with vent)
            (99.0, Some(4)),  // just below (with vent)
            (50.0, Some(4)),  // 0-100 (with vent)
        ];
        for (ratio, expected) in test_cases {
            assert_eq!(
                score_from_ratio(ratio, true),
                expected,
                "ratio {} failed",
                ratio
            );
        }
    }

    #[test]
    fn prop_monotonicity_decreasing_ratios() {
        // Lower ratios should produce higher (worse) scores
        let ratios = vec![500.0, 350.0, 250.0, 150.0, 50.0];
        let mut prev_score: Option<u8> = None;
        for ratio in ratios {
            let score = score_from_ratio(ratio, true);
            if let (Some(prev), Some(curr)) = (prev_score, score) {
                assert!(
                    curr >= prev,
                    "monotonicity violated: {} should have >= score than {}",
                    ratio,
                    50.0
                );
            }
            prev_score = score;
        }
    }

    #[test]
    fn prop_no_vent_high_scores_abstain() {
        // Scores 3-4 require ventilation
        let no_vent_ratios = vec![150.0, 100.0, 99.0, 50.0, 25.0];
        for ratio in no_vent_ratios {
            let score = score_from_ratio(ratio, false);
            assert!(
                score.is_none() || score == Some(0) || score == Some(1) || score == Some(2),
                "ratio {} without vent should not give 3 or 4",
                ratio
            );
        }
    }

    #[test]
    fn prop_no_vent_low_scores_exist() {
        // Scores 0-2 should work without ventilation
        let low_vent_ratios = vec![500.0, 400.0, 350.0, 300.0, 250.0, 200.0];
        for ratio in low_vent_ratios {
            let score = score_from_ratio(ratio, false);
            assert!(
                score.is_some(),
                "ratio {} without vent should give some score",
                ratio
            );
        }
    }

    #[test]
    fn prop_with_vent_all_ratios_covered() {
        // Any positive ratio with vent should return Some score
        let vent_ratios = vec![
            0.1, 10.0, 50.0, 100.0, 150.0, 200.0, 250.0, 300.0, 350.0, 400.0, 500.0,
        ];
        for ratio in vent_ratios {
            let score = score_from_ratio(ratio, true);
            assert!(
                score.is_some(),
                "ratio {} with vent should always return Some",
                ratio
            );
        }
    }

    #[test]
    fn prop_operator_version_mismatch() {
        // Operator should abstain if evidence version doesn't match operator version
        let op = SofaRespOperator::new("0.2.0");
        let origin = crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7");
        let prov = crate::Provenance::new(
            origin,
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.3.0"), // wrong version
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        let result = op.apply(&Hyp::unknown(), &evidence);
        match result {
            Outcome::Abstain(AbstainReason::OperatorPreconditionUnmet(_)) => {}
            other => panic!("expected version mismatch abstention, got {:?}", other),
        }
    }

    #[test]
    fn prop_operator_zero_fio2() {
        // Operator should abstain if FiO2 is zero
        let op = SofaRespOperator::new("0.2.0");
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "3150-0"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(0.0)), // zero FiO2
        ];
        let evidence = crate::Evidence::new(observations, prov);
        let result = op.apply(&Hyp::unknown(), &evidence);
        match result {
            Outcome::Abstain(AbstainReason::InsufficientEvidence(_)) => {}
            other => panic!(
                "expected InsufficientEvidence for zero FiO2, got {:?}",
                other
            ),
        }
    }

    #[test]
    fn prop_operator_missing_pao2() {
        // Operator should abstain if PaO2 observation is missing
        let op = SofaRespOperator::new("0.2.0");
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "3150-0"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            // Missing LOINC:2703-7
        ];
        let evidence = crate::Evidence::new(observations, prov);
        let result = op.apply(&Hyp::unknown(), &evidence);
        match result {
            Outcome::Abstain(AbstainReason::InsufficientEvidence(_)) => {}
            other => panic!(
                "expected InsufficientEvidence for missing PaO2, got {:?}",
                other
            ),
        }
    }

    #[test]
    fn prop_operator_missing_fio2() {
        // Operator should abstain if FiO2 observation is missing
        let op = SofaRespOperator::new("0.2.0");
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            // Missing LOINC:3150-0
        ];
        let evidence = crate::Evidence::new(observations, prov);
        let result = op.apply(&Hyp::unknown(), &evidence);
        match result {
            Outcome::Abstain(AbstainReason::InsufficientEvidence(_)) => {}
            other => panic!(
                "expected InsufficientEvidence for missing FiO2, got {:?}",
                other
            ),
        }
    }

    #[test]
    fn prop_operator_score3_no_vent_abstains_all() {
        // Score 3-4 (low ratios) without vent should abstain
        let low_ratios = vec![150.0, 125.0, 100.0, 99.0, 50.0, 25.0, 10.0, 1.0];
        for ratio in low_ratios {
            let op = SofaRespOperator::new("0.2.0");
            let prov = crate::Provenance::new(
                crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
                Utc::now(),
                crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
                BTreeMap::new(),
            );
            let observations = vec![
                crate::Observation::new("LOINC:2703-7", serde_json::json!(ratio)),
                crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
                // No vent flag
            ];
            let evidence = crate::Evidence::new(observations, prov);
            let result = op.apply(&Hyp::unknown(), &evidence);
            match result {
                Outcome::Abstain(AbstainReason::OperatorPreconditionUnmet(_)) => {}
                other => panic!(
                    "ratio {} without vent should abstain (score 3-4), got {:?}",
                    ratio, other
                ),
            }
        }
    }

    #[test]
    fn prop_operator_valid_vent_input_refines() {
        // Valid input with vent should always refine
        let valid_ratios = vec![500.0, 250.0, 150.0, 100.0, 50.0, 10.0];
        for ratio in valid_ratios {
            let op = SofaRespOperator::new("0.2.0");
            let prov = crate::Provenance::new(
                crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
                Utc::now(),
                crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
                BTreeMap::new(),
            );
            let observations = vec![
                crate::Observation::new("LOINC:2703-7", serde_json::json!(ratio)),
                crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
                crate::Observation::new("SNOMED:243144002", serde_json::json!(true)), // vent
            ];
            let evidence = crate::Evidence::new(observations, prov);
            let result = op.apply(&Hyp::unknown(), &evidence);
            match result {
                Outcome::Refined(_) => {}
                other => panic!("ratio {} with vent should refine, got {:?}", ratio, other),
            }
        }
    }

    #[test]
    fn prop_refined_atom_version_matches() {
        // Refined atoms should have operator version
        let version = "0.2.1";
        let op = SofaRespOperator::new(version);
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", version),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        if let Outcome::Refined(h_prime) = op.apply(&Hyp::unknown(), &evidence) {
            for atom in h_prime.atoms() {
                if atom.code.contains("sofa-resp") {
                    assert_eq!(atom.version, version);
                }
            }
        }
    }

    #[test]
    fn prop_refined_atom_system_snomed() {
        // Refined atoms should use SNOMED system
        let op = SofaRespOperator::new("0.2.0");
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        if let Outcome::Refined(h_prime) = op.apply(&Hyp::unknown(), &evidence) {
            for atom in h_prime.atoms() {
                if atom.code.contains("sofa-resp") {
                    assert_eq!(atom.system, crate::OntologySystem::SNOMED);
                }
            }
        }
    }

    #[test]
    fn prop_refinement_monotonicity_inv_ps03() {
        // Refined hypothesis should refine input (h' ⊑ h)
        let op = SofaRespOperator::new("0.2.0");
        let h_input = Hyp::unknown();
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        if let Outcome::Refined(h_prime) = op.apply(&h_input, &evidence) {
            assert!(h_prime <= h_input, "INV-PS-03: refined must refine input");
        }
    }

    #[test]
    fn prop_refined_adds_one_atom() {
        // Refining should add exactly one atom
        let op = SofaRespOperator::new("0.2.0");
        let h_input = Hyp::unknown();
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        if let Outcome::Refined(h_prime) = op.apply(&h_input, &evidence) {
            let atoms_added = h_prime.atoms().len() - h_input.atoms().len();
            assert_eq!(atoms_added, 1, "exactly one atom should be added");
        }
    }

    #[test]
    fn prop_refined_code_contains_sofa_resp() {
        // Refined atoms should have correct SOFA code
        let op = SofaRespOperator::new("0.2.0");
        let prov = crate::Provenance::new(
            crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
            Utc::now(),
            crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
            BTreeMap::new(),
        );
        let observations = vec![
            crate::Observation::new("LOINC:2703-7", serde_json::json!(250.0)),
            crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
            crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
        ];
        let evidence = crate::Evidence::new(observations, prov);
        if let Outcome::Refined(h_prime) = op.apply(&Hyp::unknown(), &evidence) {
            let has_sofa = h_prime
                .atoms()
                .iter()
                .any(|a| a.code.contains("clinlat-sofa-resp"));
            assert!(has_sofa, "refined should contain sofa-resp atom");
        }
    }

    #[test]
    fn prop_refined_code_score_matches() {
        // Refined code should contain the expected score
        let test_cases = vec![(500.0, 0), (350.0, 1), (250.0, 2), (150.0, 3)];
        for (ratio, expected_score) in test_cases {
            let op = SofaRespOperator::new("0.2.0");
            let prov = crate::Provenance::new(
                crate::ProvenanceOrigin::new("lab", "LOINC", "2703-7"),
                Utc::now(),
                crate::Ver::new("clinlat", "sofa_resp", "0.2.0"),
                BTreeMap::new(),
            );
            let observations = vec![
                crate::Observation::new("LOINC:2703-7", serde_json::json!(ratio)),
                crate::Observation::new("LOINC:3150-0", serde_json::json!(1.0)),
                crate::Observation::new("SNOMED:243144002", serde_json::json!(true)),
            ];
            let evidence = crate::Evidence::new(observations, prov);
            if let Outcome::Refined(h_prime) = op.apply(&Hyp::unknown(), &evidence) {
                let score_str = expected_score.to_string();
                let has_score = h_prime
                    .atoms()
                    .iter()
                    .any(|a| a.code.contains(&format!("-{}", score_str)));
                assert!(
                    has_score,
                    "ratio {} should produce score {} in atom code",
                    ratio, expected_score
                );
            }
        }
    }
}