# Reproduction — Saturating clamp (output bounded to [-1, 1])

Source `examples/clamp_bounded.eml` (sha256 `602c87f60a2a9b9b`). 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 total** | **29 targets from one source** | LOCAL |
| proof | `clamp_in_unit_interval` — ✓ clean (`proof/clamp_in_unit_interval.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/clamp.png` — max|clamp_unit(x)| = 1.0 ≤ 1.0 | LOCAL |
| hardware | — (pure clamp primitive; the same saturation backs the PID / aerospace guards that were run on silicon) | NONE |

**The same claim, two ways.** The Lean theorem `clamp_in_unit_interval` proves clamp_unit(x) is always within [-1, 1] for every input x; the simulation shows `max|clamp_unit(x)| = 1.0 ≤ 1.0` (clamp band [-1.0, 1.0]); Proved, simulated.