# Reproduction — Bounded sine oscillator (|output| ≤ amplitude)

Source `examples/sine_oscillator.eml` (sha256 `73837d61bea80a15`). 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 | `sine_oscillator_amplitude_bound` — ✓ clean (`proof/sine_oscillator_amplitude_bound.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/sine.png` — max|A·sin(ωt)| = 0.8 ≤ 0.8 | LOCAL |
| hardware | — (numeric kernel; no dedicated hardware capture) | NONE |

**The same claim, two ways.** The Lean theorem `sine_oscillator_amplitude_bound` proves |A·sin(ωt)| ≤ A for A ∈ [0,1], ω ∈ [0, 1e4], t ≥ 0; the simulation shows `max|A·sin(ωt)| = 0.8 ≤ 0.8` (amplitude bound |·| ≤ 0.8); Proved, simulated.