FERROMOTION · RUST → WASM

What a Certificate Cannot Claim

A verification returns UNDECIDED. What does that tell you?

Learn to read a verification result as a claim with preconditions rather than a number. You will make the same system return Certified, Refuted and Undecided; discover that one of those transitions involves no change to the geometry at all; find a green verdict that means nothing; and find a fourth failure the lab uncovered in itself, a bound that was only valid in a region nobody checked. Pass = you produce all three verdicts, explain which control caused each, and say what the precondition check found.

01Challenge

You have spent two lessons getting a derivative right. Now suppose you succeeded, optimised a policy on it, and someone asks whether the robot is safe. the answer is not a percentage. The Bench gives you a mass bouncing under a ceiling it must not hit, with the gap between your smooth contact model and the real one drawn as an envelope around the trajectory. Three controls: contact stiffness, ceiling height, horizon length. Produce each of the three verdicts. Then find the setting where the verdict is CERTIFIED and the certificate is worth nothing, and work out how you would have caught that if the lab had not told you.

Predict firstA verification returns UNDECIDED. What does that tell you?

02Model

A certificate is not a score. It is a sentence of the form: every state this system can reach, under these assumptions, satisfies this constraint. Four things in that sentence can fail independently. First: reachable. The claim is about a SET, not a trajectory. That is why the Bench draws an envelope rather than a line, and why the envelope is the thing tested against the ceiling. Widen the gap between your smooth model and the real one and the envelope swells until it touches the ceiling, and the verdict flips to REFUTED. A refutation is a counterexample, and a counterexample survives any amount of argument. Second: under these assumptions. Press the evidence button. Nothing about the geometry changes - not the envelope, not the trajectory, not the slack - and the verdict changes anyway, from UNDECIDED to CERTIFIED, because measuring the model gap at twenty-five sampled states tells you the gap is AT LEAST that big. It is a lower bound. A tube built on a lower bound can refute soundly and can never certify, however much room appears to be left. Sampling refutes, proof certifies. Third: this constraint. Shorten the horizon and watch the verdict go green. The mass needs about two hundred and eighty milliseconds to reach its apex; with a sixty-millisecond horizon the ceiling is never approached. The certificate is true. It is also worthless, and nothing in the word CERTIFIED tells you so. Fourth: where each bound is valid. Every step of the tube carries bounds, and some are only valid somewhere. The free-flight steps are given a gap of exactly zero, justified by a real argument - above the plane both models integrate the same quadratic, so they cannot differ. Above the plane. The precondition check tests that, and it is on by default. It passes here, and the story of how it came to pass is the reason it exists. When the check was first switched on it FAILED, and the failure was real: the tube's envelope dipped below the plane for the first three steps after the bounce, where free flight is the motion of neither model. The cause was not the certificate. It was a scoping error in how the model gap was fed to the tube. The disturbance set in a reachable-tube recursion is a PER-STEP quantity, and the measured gap is the mismatch accumulated over the whole contact - about three control steps' worth. Injecting all of it at one step over-stated the one-step disturbance threefold and pushed the envelope through the floor. Divide it across the steps the contact actually spans and the envelope stays above the plane, the precondition holds, and the certificate closes. So the fourth control is not a demonstration that certificates fail. It is a demonstration that a check you build into the tool finds your own errors, including the ones that look like the tool being too strict. Without it the scoping error would have shipped as a valid certificate.

03Guided practice

Step A (worked, fully shown): leave everything at its default. Stiffness 1e6, ceiling 0.46 m, horizon 340 steps, evidence SAMPLED, precondition checking ON. The verdict reads UNDECIDED with reason GapOnlySampled. Note the tube half-width (about 1.3e-2 m) and the nominal slack (about 3.9e-2 m). The constraint is not violated. It is also not certified. Step B (worked): press the evidence button once. Confirm from the readout that the tube half-width and the nominal slack are UNCHANGED to every digit shown, and that the verdict is now CERTIFIED with a margin near 0.026 m. Write down what changed. It was not the system, and it was not the geometry. Step C (you do it): with evidence still PROVED, drag stiffness down to 1e4. The smoothing gap rises from about 9.5e-3 to about 3.2e-1, and the verdict flips to REFUTED. You have now produced all three. Step D (you do it): return stiffness to 1e6 and drag the horizon down to 60 steps. The verdict goes green. Read the vacuity ratio and the apex step count, and say in one sentence why this certificate is worthless. Step E (you do it): turn precondition checking OFF and back ON, and confirm the verdict does not move. It passes. Then answer the question that matters: if a check never fires, why keep it? The answer is in the narration - this one fired once, on a scoping error in the fixture, and the error looked exactly like the check being too strict.

04Feedback

PASS WHEN PASS when you have produced all three verdicts on the live lab, confirmed that the evidence button changes the verdict without changing any number in the readout, found a CERTIFIED result whose vacuity warning is showing, and can say what the precondition check is for even though it currently passes. There is no code to submit.

If your run fails, check:

You are reading UNDECIDED as a failure. It is not a failure and it is not a pass. It says the tube did not cross the ceiling and the evidence cannot support a claim either way. The useful response is to go and get better evidence, not to shrug and ship.
You pressed the evidence button and the verdict improved, so you concluded the system got safer. Check the readout again: the tube half-width and the nominal slack did not move. Nothing about the system changed. You changed what you were willing to assert.
You are treating PROVED as a free upgrade. Read the button label: it says assumed. Deriving a real Lipschitz bound on the smoothing gap of a stiff penalty contact is an open problem, and the lab lets you assume it only so you can see what a proof would buy. That is a reason to go and prove it, not to skip it.
The verdict went green when you shortened the horizon and you moved on. Look at the apex marker: it is off the right-hand edge of the plot. The mass never gets near the ceiling within your horizon, so the constraint could not have been violated. The certificate is true and says nothing.
You found the refutation at low stiffness and read it as the soft contact being unsafe. Closer: the soft contact makes the model gap large enough that safety cannot be established. And now connect it to the previous lesson - high stiffness is where the tube gets tight enough to certify, and it is also exactly where a fixed-step gradient reports the wrong sign. The regime you must certify in is the regime you cannot differentiate naively.
The vacuity ratio is the number to watch, not the margin. A margin of 0.4 m with a ratio of 300 is a certificate about a constraint that was never in play. A margin of 0.02 m with a ratio of 3 is a real one.
You are wondering why a check that always passes is worth having. Because it did not always pass. Switched on for the first time it failed at step 2, and the cause was a scoping error in how the gap was handed to the tube: a reachable-tube disturbance set is PER STEP, and the measured gap accumulates over a contact spanning about three steps. All of it injected at one step over-stated the disturbance threefold and pushed the envelope below the plane. The check found that. Without it the error would have shipped as a valid certificate.
If you ever do see PreconditionViolated, do not reach for the ceiling. The ceiling governs whether the constraint is SATISFIED; this failure is about whether a step's bound is APPLICABLE at all. Different questions, and only one of them has a slider. Look instead at what each step's bound assumes and whether the reachable set stayed where that assumption holds.

05Retrieve & space

The three values (short answer): name the three verdicts and say which of them a counterexample produces -> Certified, Refuted, Undecided. Refuted comes from a counterexample, which is why it is sound even on sampled evidence.
The asymmetry (typed): sampling can ____ a constraint and can never ____ one -> refute / certify. A sampled gap is a lower bound on the true gap, so a tube built from it under-states the risk.
The unchanged geometry (multiple choice): pressing the evidence button changed the verdict from Undecided to Certified. What else changed? -> Nothing. Not the tube width, not the nominal slack, not the trajectory. The verdict tracks the evidence, not the geometry.
The vacuous certificate (short answer): a run reports CERTIFIED with margin 0.26 m and a vacuity ratio of 300. What is wrong? -> The constraint was never approached, so the certificate is true and worth nothing. The horizon is too short for the ceiling to be reachable.
The regime trap (short answer): why is the stiffness that makes a certificate possible the same stiffness that makes a naive gradient useless? -> The tube is only tight enough to certify once the model gap is small, which needs a stiff contact; and a stiff contact is exactly where fixed-step autodiff reports the wrong sign. You need the exact or tolerance-driven Jacobian to work in the only regime where you can certify.
A saturated controller (multiple choice): a QP controller that has hit its actuator limits behaves like which system? -> The open loop. A saturated mode is the plant with no feedback, so whether a QP loop can be certified at all is a property of the plant, not of the gains.
The right metric (typed): a plastic impact is exactly non-expansive under a metric built from ____ -> the kinetic energy (the mass matrix). Measured residual 0.000e0 with the mass-matrix metric against 1.1478 for an LQR cost, so the choice of metric decides whether the impact looks stabilising or destabilising.
The fourth failure (short answer): a certificate's step bounds can be valid only in a region. What did checking that region find here? -> A scoping error in the fixture, not a flaw in the certificate. The reachable-tube disturbance set is per step, and the measured gap accumulates over a contact spanning about three control steps; injecting all of it at one step over-stated the one-step disturbance and pushed the tube below the plane, where the flight steps' zero-gap justification does not hold. Scoped correctly, the precondition holds and the certificate closes.
Satisfied versus applicable (multiple choice): PreconditionViolated persists no matter how high you raise the ceiling. Why? -> Because the ceiling governs whether the constraint is satisfied, and this failure is about whether a step's bound is applicable at all. They are different questions and only one of them has a slider.

06Mastery & project

You read a verification result as a sentence with four failure points: the set it quantifies over, the evidence it rests on, the constraint it names, and the region each of its bounds is valid in. You never accept Certified without checking whether the constraint was reachable, nor without asking where each bound applies. You know which way the evidence asymmetry runs. And you keep a check that passes, because this one fired exactly once, on an error of your own that looked like the check being too strict.

Not a capstone lesson. It is the standard the rest of the course is held to: every safety or performance claim you make from here gets the same three questions.

GO FURTHER · THE LIVE PLAYGROUND

The tube, and the type that refuses to overclaim ↗ · The evidence enum is carried through every function and enforced in certify() rather than left to the caller. Includes the test that a sampled bound cannot certify at a margin of 1e6, and the activity check added after a vacuous certificate shipped.
Measured: stiffness decides whether the certificate exists ↗ · Gap 3.2e-1 at 1e4 against 9.5e-3 at 1e6, turning a refuted ceiling into a certifiable one. Also records a mis-specified experiment that was deleted rather than tuned into looking sensible.
A saturated QP mode is the open loop ↗ · The classical switched-stability fixture - two individually stable modes at spectral radius 0.9500 - composes to a per-step gain of 8.1113 over eight steps, which is what validates the certificate. Read it as a fixture, not as a measurement of the shipped QP stack: real QP active-set modes in the same run reach a worst switching gain of 1.1732, and no QP mode sits at 0.9500, because a saturated mode equals the open-loop radius exactly. That last fact is the module's actual finding - certifiability is a property of the plant rather than of the gains.
The metric that makes an impact non-expansive ↗ · A plastic impact is exactly non-expansive in the kinetic-energy metric (residual 0.000e0) and looks expansive under an LQR cost. The metric is a modelling choice with a verdict attached.
Chaining skills without the reliabilities multiplying away ↗ · Funnel composition with detection, where an early claim that the escape rate cancels exactly turned out to be a spurious factor in the algebra and was caught by Monte Carlo.

← The Reference That Shares Its Machinery Back to course →

FERROMOTION · RUST → WASM

What a Certificate Cannot Claim

Live ferromotion-control: the reachable tube is propagated by the real zonotope algebra over the exact saltation-composed impact map, and the smoothing gap is measured against the rigid model rather than assumed. The verdict comes from the same certify() the library exposes, including its refusal to certify on sampled evidence. Certified, Refuted and Undecided are drawn in three unrelated colours on purpose: they are not a spectrum, and Undecided is not a dimmer green.

You read

the readout: what the Rust crate computes, recomputed as you change things

You change

the bench controls, and with them the assumption the measurement rests on

Fixed

the ferromotion crate doing the computing, and the check that decides pass