-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : soft_actuator_within_band
-- source  : examples/soft_actuator.eml  ->  eml-compile --target lean   (the artifact the zoo ships; NOT a probe)
-- tool    : forge 173c30c . machlib e36c002a . lean via lake
-- when    : 2026-07-10T08:02:45Z
-- verdict : CLEAN -- footprint free of sorry- and classical-citation axioms
-- (re-derive: make verify-proof)
--
/tmp/claude-1000/-home-monogate-monogate/69bd851b-b35c-4a08-ae27-43248ef8ea21/scratchpad/sa_probe.lean:25:5: warning: unused variable `h_error`
note: this linter can be disabled with `set_option linter.unusedVariables false`
/tmp/claude-1000/-home-monogate-monogate/69bd851b-b35c-4a08-ae27-43248ef8ea21/scratchpad/sa_probe.lean:26:5: warning: unused variable `h_gain`
note: this linter can be disabled with `set_option linter.unusedVariables false`
'soft_actuator_within_band' depends on axioms: [propext,
 Classical.choice,
 MachLib.Real,
 Quot.sound,
 MachLib.Real.leR,
 MachLib.Real.le_iff_lt_or_eq,
 MachLib.Real.ltR,
 MachLib.Real.lt_total,
 MachLib.Real.mulR,
 MachLib.Real.negR,
 MachLib.Real.oneR,
 MachLib.Real.realOfScientific,
 MachLib.Real.tanh]