# Reproduction — Closed-loop safety envelope under an injected fault

Machine-checked result `MachLib.Real.first_order_clamp_envelope` in `MachLib.ClosedLoopSafety` — a proof, not a codegen kernel. Regenerate with `make all`.

> The envelope is a conservative worst-case SAFETY bound — real trajectories sit well inside it (here the fault peak is ~40% of the envelope). That margin IS the safety, not a defect: the bound rests on the actuator clamp, not on good control. Measured on real hardware (ESP32 RC + a nonlinear diode-RC plant) it held under an injected fault while the breadboard limit-cycled.

| stage | artifact | tier |
|---|---|---|
| proof | `MachLib.Real.first_order_clamp_envelope` — ✓ clean (`proof/first_order_clamp_envelope.axioms.txt`) | REPLAY (re-derive: TOOLCHAIN — Lean) |
| simulate | `sim/trace.csv`, `sim/safety_envelope.png` — max|x| over the run (fault injected at midpoint) = 0.8 ≤ 2.0 | LOCAL |
| hardware | the same clamp-guarded envelope was measured on real silicon under an INJECTED fault: ESP32 DAC→R→C plant (nominal 0.806≤1.0, +1.0 fault 1.546≤2.0) and a genuinely nonlinear diode-RC plant (785/806 sample reversals = real noise) — the loop limit-cycled, nothing like the sim, yet the envelope held. Replayed from capture. | REPLAY |

**The same claim, three ways.** The Lean theorem `MachLib.Real.first_order_clamp_envelope` proves for a first-order plant with a saturating actuator clamp (|u|≤U) and bounded disturbance (|w|≤W), the state stays within the envelope X=(U+W)/(1−a) for ALL time and ANY controller; the simulation shows `max|x| over the run (fault injected at midpoint) = 0.8 ≤ 2.0` (state stays inside the proved envelope X*=(U+W)/(1−|a|) even after the injected fault — safety rides on the clamp, not on good control); the hardware evidence shows the same behavior measured on real hardware; Proved, simulated, measured.