PYTHON · NUMPY

What a Certificate Cannot Claim

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, and find a green verdict that means nothing. Pass = you produce all three verdicts, explain which control caused each, and identify a vacuous certificate from the readout.

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 honest 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.

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. Three things in that sentence can fail independently, and this lesson is about all three. 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. That flip is real: 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. 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 a constraint honestly and can never certify one, however much room appears to be left. This is not pedantry. Sampling refutes, proof certifies, and a system that returns Certified on sampled evidence is lying to you in the most expensive possible way. Third: this constraint. Shorten the horizon and watch the verdict go green. Look at why. The mass needs about two hundred and eighty milliseconds to reach its apex; with a sixty-millisecond horizon the ceiling is simply never approached. The certificate is true. It is also worthless, and nothing in the word CERTIFIED tells you so. The only defence is to check how close the nominal path came to the constraint compared with how wide the envelope is, which is the vacuity ratio in the readout. We shipped that exact mistake before adding it.

03Guided practice

Step A (worked, fully shown): leave everything at its default. Stiffness 1e6, ceiling 0.46 m, horizon 340 steps, evidence SAMPLED. 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. The verdict is now CERTIFIED with a margin near 0.026 m. Write down what changed. It was not the system. 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 at around step 208. 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.

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, and found a CERTIFIED result whose vacuity warning is showing. 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.

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.

06Mastery & project

You read a verification result as a sentence with three failure points: the set it quantifies over, the evidence it rests on, and the constraint it names. You never accept Certified without checking whether the constraint was reachable. You never accept a bound without asking whether it was sampled or proved. And you know which way the asymmetry runs: a counterexample settles things, a wide margin on weak evidence settles nothing.

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 ↗ — Two modes at spectral radius 0.9500 compose to a per-step gain of 8.1113, so 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 No Machinery Back to course →

PYTHON · NUMPY

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 arrays and values already in scope

You change

the code you write in each cell

Fixed

the dataset and the checks that grade you