-- Generated by the EML-lang Lean backend
-- Source module: aerospace_actuator_guard_band
-- Source file:   /home/monogate/monogate/forge/examples/actuator_guard.eml
-- Verified fns:  actuator_command_within_band

import MachLib.EML
import MachLib.Trig
import MachLib.Forge
import MachLib.Linarith
import MachLib.FixedPoint
import MachLib.SignTactic

open MachLib
open MachLib.Real

-- ── actuator_command_within_band ──

noncomputable def actuator_command_within_band_def (error : Real) (integral : Real) (deriv : Real) (kp : Real) (ki : Real) (kd : Real) (u_min : Real) (u_max : Real) : Real :=
  (min (max (((kp * error) + (ki * integral)) + (kd * deriv)) u_min) u_max)

theorem actuator_command_within_band (error : Real) (integral : Real) (deriv : Real) (kp : Real) (ki : Real) (kd : Real) (u_min : Real) (u_max : Real)
    (h1 : (u_min <= u_max))
    (h_clamp1 : u_min ≤ u_max) :
    ((u_min <= (actuator_command_within_band_def error integral deriv kp ki kd u_min u_max))) ∧ (((actuator_command_within_band_def error integral deriv kp ki kd u_min u_max) <= u_max)) := by
  unfold actuator_command_within_band_def
  refine ⟨?_, ?_⟩ <;>
    first
    | (apply lo_le_clamp <;> (first | assumption | mach_positivity))
    | apply clamp_le_hi
    | mach_positivity
    | mach_sign
    | rfl
    | sorry  -- out of reach; left for the prover