========================================================================
Guard <-> .bio conformance proof (Z3, IEEE-754 float64, all inputs incl. NaN/inf)
========================================================================
guard : backend/modules/fdir_guard.py  sha256 29202a03448c613c
spec  : satellite_fdir.bio             sha256 ddb0b8ec06ca6f8c
thresholds parsed from .bio: {'gps_ins_dist_m': 50.0, 'power_residual_w': 500.0, 'imu_star_diff_deg': 0.5, 'wheel_torque_resid_nm': 0.05, 'batt_voltage_drop_v': 0.5}

  PASS  [S1] |gps_ins_dist_m| >= 50.0 => fault_detected 
  PASS  [S2] |power_residual_w| >= 500.0 => fault_detected 
  PASS  [S3] |imu_star_diff_deg| >= 0.5 => fault_detected 
  PASS  [S4] |wheel_torque_resid_nm| >= 0.05 => fault_detected 
  PASS  [S5] |batt_voltage_drop_v| >= 0.5 => fault_detected 
  PASS  [S6] all channels below threshold => no fault (no false alarm) 
  PASS  [S7] fault_detected => safe_mode 
  PASS  [S8] any NaN input => fault_detected (fail-safe) 
  PASS  [S9] fault_code in 0..5 and (fault_code != 0 <=> fault_detected) 
  PASS  [S10] only gps_ins_dist_m breached => fault_code == 1 
  PASS  [S11] only power_residual_w breached => fault_code == 2 
  PASS  [S12] only imu_star_diff_deg breached => fault_code == 3 
  PASS  [S13] only wheel_torque_resid_nm breached => fault_code == 4 
  PASS  [S14] only batt_voltage_drop_v breached => fault_code == 5 
  PASS  [S15] a nominal vector is accepted (satisfiable) 

  PASS  [DIFF] translator vs real Python function: 1565 vectors, 0 mismatches

  Mutation controls (each broken guard must be REJECTED):
  PASS  [MUT] boundary < -> <=  (gps): rejected by S1,S10
  PASS  [MUT] threshold GPS_M 50 -> 51: rejected by S1,S10
  PASS  [MUT] threshold IMU 0.5 -> 0.4: rejected by S6,S13,S14
  PASS  [MUT] drop abs() on power residual: rejected by S2,S11
  PASS  [MUT] NaN-unsafe form (>=): rejected by S8
  PASS  [MUT] safe_mode never set: rejected by S7
  PASS  [MUT] battery channel dropped: rejected by S5,S8,S14
  PASS  [MUT] fault codes swapped: rejected by S12

========================================================================
RESULT: 15 proofs + differential + 8 mutation controls: ALL PASS
fdir_guard.py (used by MetaSpaceSimulator) conforms to satellite_fdir.bio for every float64 input.
========================================================================