-- Reproduction axiom trail -- re-derived from source (TOOLCHAIN tier).
-- theorem : rc_time_constant_def
-- source  : examples/rc_filter.eml  ->  eml-compile --target lean   (the artifact the zoo ships; NOT a probe)
-- tool    : forge 8074510 . machlib 1420f96 . lean via lake
-- when    : 2026-07-02T04:37:24Z
-- verdict : CLEAN -- footprint free of sorry- and classical-citation axioms
-- (re-derive: make verify-proof)
--
MachLib/ReVerify_rc.lean:24:5: warning: unused variable `h1`
note: this linter can be disabled with `set_option linter.unusedVariables false`
MachLib/ReVerify_rc.lean:25:5: warning: unused variable `h2`
note: this linter can be disabled with `set_option linter.unusedVariables false`
MachLib/ReVerify_rc.lean:74:5: warning: unused variable `h1`
note: this linter can be disabled with `set_option linter.unusedVariables false`
MachLib/ReVerify_rc.lean:91:5: warning: unused variable `h1`
note: this linter can be disabled with `set_option linter.unusedVariables false`
'rc_time_constant_def' depends on axioms: [propext,
 MachLib.Real,
 MachLib.Real.ltR,
 MachLib.Real.mulR,
 MachLib.Real.zeroR]