# Reproduction — Vibration RMS — one-sided sqrt, range-guarded

Source `examples/vibration_rms.eml` (sha256 `a3b7f9cd162f69b6`). Regenerate with `make demo`.

> A sqrt kernel — the one-sided-domain primitive. sqrt is only Lipschitz away from 0, so its forward-error certificate needs a positive lower bound on the argument; here ax²+ay²≥0 plus an additive NOISE_FLOOR supplies it honestly. The @verify contract PROVES the RMS magnitude stays in the sensor range [0,50] via the clamp; the certificate BOUNDS the compiled float64 sqrt's drift (Certcom.pipeline_pos_over_arith — ln/sqrt over an arithmetic core, conditional on the noise-floor lower bound).

| 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 | `vibration_rms_within_range` — ✓ clean (`proof/vibration_rms_within_range.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/vibration_rms.png` — RMS magnitude samples outside the sensor range [0, 50] m/s^2 = 0 = 0 | LOCAL |
| certificate | fwd-error ≤ `6.04e-13` abs (`5443` ulp of result), all inputs in range — `certificate.json` | LOCAL |
| hardware | — | N/A |

**Forward-error certificate.** For every input in the declared ranges (`|ax| ≤ 30`, `|ay| ≤ 30`), the COMPILED kernel's float64 result is within **`6.043e-13`** (absolute, ≈ `5443` ulp of the result) of the exact real value, assuming IEEE-754 binary64 round-to-nearest, unit roundoff u = 2^-53 ≈ 1.110e-16. This is not asserted — it is the `absErr` fold computed over the kernel's AST, and that fold is proved sound (`sorryAx`-free) by machlib's `Certcom.pipeline_pos_over_arith`. Regime: absolute. The soundness is machine-checked (TOOLCHAIN); the per-kernel bound is computed here (LOCAL).

The harness also emits the **instantiated proof** `certificate/vibration_rms_forward_error.lean` — the kernel's arithmetic core as an `EML` term, its generated `IsArith` proof, and the `pipeline_arith` instantiation = a machine-checked per-kernel theorem `vibration_rms_forward_error : AbsEnc (absErr …) (emitted-C value) (exact)`, `sorryAx`-free, holding for any `FPBridge`. Re-check: `lake env lean` it against machlib (TOOLCHAIN).

**The same claim, two ways.** The Lean theorem `vibration_rms_within_range` proves the reported RMS magnitude is always inside the sensor range [0, 50] m/s^2, for any input; the simulation shows `RMS magnitude samples outside the sensor range [0, 50] m/s^2 = 0 = 0` (a swept-frequency 2-axis vibration with a burst peaking at 35.8 m/s^2 stays inside [0,50.0] throughout — the range the theorem proves, the sqrt the forward-error certificate bounds (conditional on the 0.25 noise floor keeping the argument > 0)); Proved, simulated.