// Lean 4 → LambdaIR → MiniC → C → Rust
// Module: HeytingLean.PadicDecoupling.Hamiltonian.Tripartite
// Theorem preserved: interaction_cancellation

/// Three-body energy decomposition: worker, signal, interaction.
#[derive(Clone, Copy, Debug, PartialEq)]
pub struct TripartiteHamiltonian {
    pub e_worker: f64,
    pub e_signal: f64,
    pub e_interaction: f64,
}

impl TripartiteHamiltonian {
    pub fn total(self) -> f64 {
        self.e_worker + self.e_signal + self.e_interaction
    }
}

/// Theorem preserved: interaction_cancellation
/// worker_loss + signal_gain + int_gain = 0 when they sum from a transfer δ
pub fn check_interaction_cancellation(
    worker_loss: f64,
    signal_gain: f64,
    int_gain: f64,
) -> bool {
    (worker_loss + signal_gain + int_gain).abs() < 1e-12
}

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

    #[test]
    fn total_adds_components() {
        let h = TripartiteHamiltonian {
            e_worker: 1.25,
            e_signal: 0.5,
            e_interaction: 0.25,
        };
        assert_eq!(h.total(), 2.0);
    }

    #[test]
    fn cancellation() {
        let delta = 5.0;
        let frac = 0.3;
        assert!(check_interaction_cancellation(
            -delta,
            delta * frac,
            delta * (1.0 - frac),
        ));
    }
}