One source, every artifact — proved, simulated, and (where it exists) measured.
Each card below was produced by one command (make all) from an EML
source: the emitted C / Rust / Python / Lean, a contract proof whose axiom footprint is clean
of sorryAx, a simulation whose measured quantity satisfies the proved bound, and a
link to the raw evidence. This page is a generated view of that evidence — nothing here
is hand-authored; a proof that were not clean, or a sim check that did not hold, would show in
red on its card.
Reproduction tiers: LOCAL one command, no heavy toolchain · TOOLCHAIN re-derive with Lean / Vivado · REPLAY captured on real hardware, replayed from evidence. 4 controllers · 2 with real-hardware evidence.
clamp_in_unit_interval proves clamp_unit(x) is always within [-1, 1] for every input x; the sim shows 1.0 ≤ 1.0 (clamp band [-1.0, 1.0]).
pid_output_clamped proves the control output is always within the actuator band [OUT_MIN, OUT_MAX] = [-1, 1]; the sim shows 1.0 ≤ 1.0 (actuator band [-1.0, 1.0]); and the same behavior was measured on real hardware.
rc_time_constant_def proves the filter time constant is exactly τ = R·C; the sim shows 0.0068 ≤ 0.01 (settles to Vin within 5τ); and the same behavior was measured on real hardware.
sine_oscillator_amplitude_bound proves |A·sin(ωt)| ≤ A for A ∈ [0,1], ω ∈ [0, 1e4], t ≥ 0; the sim shows 0.8 ≤ 0.8 (amplitude bound |·| ≤ 0.8).