# Reproduction — RC low-pass filter (τ = R·C, step response)

Source `examples/rc_filter.eml` (sha256 `ed5acb7a4025d3f1`). Regenerate with `make demo`.

| stage | artifact | tier |
|---|---|---|
| emit — software (14) | `c`, `cpp`, `csharp`, `gdscript`, `go`, `java`, `javascript`, `kotlin`, `luau`, `matlab`, `python`, `rust`, `swift`, `wasm` | LOCAL |
| emit — gpu shader (5) | `glsl`, `glsl-es`, `hlsl`, `metal`, `wgsl` | LOCAL |
| emit — compiler IR (1) | `llvm` | LOCAL |
| emit — proof (3) | `coq`, `isabelle`, `lean` | LOCAL |
| emit — safety-critical (4) | `aadl`, `ada/spark`, `autosar`, `ros2` | LOCAL |
| emit — blockchain (2) | `solidity`, `zkproof` | LOCAL |
| emit — circuit/fab (3) | `jlcpcb`, `kicad`, `spice` | LOCAL |
| **emit total** | **32 targets from one source** | LOCAL |
| proof | `rc_time_constant_def` — ✓ clean (`proof/rc_time_constant_def.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/rc_step.png` — |vout(5τ) − Vin|/Vin = 0.0068 ≤ 0.01 | LOCAL |
| hardware | the same RC (R≈1kΩ, C≈1µF) was driven and measured on a real ESP32 DAC→R→C breadboard — genuinely analog (783 sample-to-sample reversals) — replayed from capture | REPLAY |

**The same claim, three ways.** The Lean theorem `rc_time_constant_def` proves the filter time constant is exactly τ = R·C; the simulation shows `|vout(5τ) − Vin|/Vin = 0.0068 ≤ 0.01` (settles to Vin within 5τ); the hardware evidence shows the same behavior measured on real hardware; Proved, simulated, measured.