actuation_bound

The bounded-actuation-noise ultimate bound — obligation C1 (bounded case)

Seal

Rung rung-1 (thin corollary of the engine) · Status interfaced — both theorems axiom-clean (#print axioms verbatim in The machine seal), no sorryAx, with the same trajectory-regularity hypotheses the engine carries applier-side BY DESIGN (hvc, hv, hbound — see interfaces).
Links: module index · interface ledger · engine time_varying_comparison (comparison_bounded) · state reading via rayleigh_sandwich (quadSandwich_matrix) · map proof_obligations_risk_phases.md row C1, §7 item 3 · pin (~/Code/tasks/streams/ctrllib/scratch/pin_actuation_bound.py) · sources panteley2001growth, giordano2019coordinated, khalil1996nonlinear (no wiki page yet)

What this seals, in one paragraph

The risk-aware program (map row C1) needs one quantitative fact for the bounded/truncated actuation-noise model: an actuation disturbance held under a constant ceiling $\epsilon (t)\le \bar{\epsilon }$ keeps the closed-loop Lyapunov value inside an explicit ultimate ball, and cannot cause a finite escape. The engine time_varying_comparison comparison_bounded already proves $v(t)\le v(0)+M/a$ from $\dot{v}\le -av+\epsilon$ and $\epsilon \le M$; this module specializes it to the actuation ceiling $\bar{\epsilon }$ (the headline seal, actuation_ultimate_bound) and reads the bound back onto the state through the quadratic Lyapunov sandwich (actuation_state_ball). It is a thin wiring corollary — near-zero new proof, high defense value — exactly as the map’s §7 item 3 predicted. No new analysis: the engine and the sandwich are both sealed elsewhere; nothing in the content of the ultimate bound is re-derived here.

The precise statements

Both declarations live in ActuationBound.lean beside this page, namespace Ctrllib.

Corollary (bounded-actuation-noise ultimate bound), actuation_ultimate_bound. Let $a>0$ and $\bar{\epsilon }\ge 0$. If the closed-loop Lyapunov value $v$ is continuous on $[0,\infty )$, right-differentiable with derivative $v^{\prime }$, obeys the decrease $v^{\prime }(t)\le -av(t)+\epsilon (t)$, the actuation disturbance sits under the constant ceiling $\epsilon (t)\le \bar{\epsilon }$, and $v(0)\ge 0$, then for every $t\ge 0$

$v(t)\le v(0)+\frac{\bar{\epsilon }}{a}$

The proof term is one line: comparison_bounded with disturbance ceiling $M:=\bar{\epsilon }$. The constant $\bar{\epsilon }/a$ is the noise-floor / ultimate-bound level (Khalil, Nonlinear Systems, ultimate bound), and the whole ball $v(0)+\bar{\epsilon }/a$ is the finite-escape guard — a uniform-in-$t$ ceiling, no limit taken.

Corollary (state-level residual ball), actuation_state_ball. Let $a>0$, $\bar{\epsilon }\ge 0$, and let $V$ satisfy the quadratic sandwich QuadSandwich V c₁ c₂, i.e. $c_1\Vert y{\Vert }^2\le V(y)\le c_2\Vert y{\Vert }^2$. If the Lyapunov value along the trajectory, $t\mapsto V(x(t))$, obeys the same comparison hypotheses under the ceiling $\bar{\epsilon }$, then for every $t\ge 0$

$c_1\Vert x(t){\Vert }^2\le c_2\Vert x(0){\Vert }^2+\frac{\bar{\epsilon }}{a}$

Dividing by $c_1>0$ gives the familiar residual-set radius $\Vert x(t){\Vert }^2\le (c_2\Vert x(0){\Vert }^2+\bar{\epsilon }/a)/c_1$; it is stated division-free. The proof is a one-line linarith composition of actuation_ultimate_bound with the two ends of the sandwich ($c_1\Vert x(t){\Vert }^2\le V(x(t))$ and $V(x(0))\le c_2\Vert x(0){\Vert }^2$).

What the corollary says for the robot

Read $v=V\circ x$ as the tracking energy (the Giordano eq-37 quadratic Lyapunov function along the closed-loop trajectory). The two statements say:

• Energy stays in a ball. If the actuation noise contributes no more than $\bar{\epsilon }$ to the energy rate at any instant, the tracking energy never leaves the ball of radius $v(0)+\bar{\epsilon }/a$. A bounded actuator disturbance buys a bounded energy — no finite escape, ever.
• The tracking error stays in a ball. Through the eigenvalue sandwich of the stiffness/inertia matrix, the same fact becomes a ceiling on the squared state norm: the tracking error sits inside an explicit residual set whose size is set by the actuator ceiling $\bar{\epsilon }$, the decay rate $a$, and the conditioning $c_2/c_1$ of the Lyapunov metric. Shrink the actuator noise floor $\bar{\epsilon }$ and the residual ball shrinks with it (linearly, $\propto \bar{\epsilon }/(a{c}_1)$).

This is the safety complement to the vanishing-disturbance convergence comparison_tendsto_zero (map row C2): even a persistent bounded actuation disturbance — one that never dies out — cannot blow the tracker up; it only inflates the residual ball by $\bar{\epsilon }/a$.

What stays applier-side (named, never faked)

Per the library’s interface discipline (interfaces), the corollary re-uses — and does not re-prove — the engine’s trajectory-regularity hypotheses, and it takes the noise ceiling as a modelling input. Named honestly:

• The regularity trio hvc, hv, hbound. Continuity of $v=V\circ x$ on the half-line, its pointwise right-derivative witness, and the differential inequality $\dot{v}\le -av+\epsilon$ — the field-level Lyapunov decrease pulled back along the solution. These are applier-side by design (the same status the engine gives them); here $V\circ x$ inherits its regularity from the chain rule on a differentiable $V$ and a solution $x$, upstream scaffolding, not this theorem’s content. The explicit HasDerivWithinAt witness also disarms Mathlib’s total-fderiv junk-value trap, exactly as the engine does.
• Nonnegativity at the start, hv0. The corollary needs only $v(0)\ge 0$ (a pointwise-at-zero slice of the engine’s hnn), trivially true for a Lyapunov function $V\ge 0$; it is strictly weaker than the full nonnegativity comparison_tendsto_zero consumes.
• Realizing $\bar{\epsilon }$ from the actuator model. That the actuation disturbance’s contribution to $\dot{v}$ is pointwise $\le \bar{\epsilon }$ is the bounded/truncated-noise model. This is the honest boundary the map flags at row C1: a Gaussian actuation noise is almost-surely unbounded, so the deterministic ultimate bound does not apply to an unbounded Gaussian model directly — one must first adopt a bounded or truncated noise model (then this corollary applies verbatim), or move to an ISS-in-probability statement (not sealed, not in Mathlib). The corollary earns the ball only for a genuinely bounded $\bar{\epsilon }$; it does not manufacture that bound.
• The sandwich QuadSandwich V c₁ c₂ (state reading only). Consumed as a hypothesis by actuation_state_ball; it is discharged for the concrete symmetric-positive-definite matrix model by rayleigh_sandwich quadSandwich_matrix, with $c_1={\lambda }_{\min }(K)>0$, $c_2={\lambda }_{\max }(K)$ the extreme eigenvalues of the Lyapunov matrix. The applier supplies those eigenvalue bounds; the corollary supplies the composition.

Numeric sanity pin

(~/Code/tasks/streams/ctrllib/scratch/pin_actuation_bound.py) — optional (the engine is already sealed), a sanity check not a proof. It (1) forward-integrates $v^{\prime }=-av+\epsilon (t)$ over a spread of disturbances each capped at $\bar{\epsilon }$ (constant-at-ceiling, oscillatory, decaying, riding-under) and confirms $v(t)\le v(0)+\bar{\epsilon }/a$ on every one, with the constant-ceiling trajectory relaxing to the floor $\bar{\epsilon }/a$; and (2) certifies the state-ball chain as an exact sum of the three hypothesis slacks (the linarith certificate). All asserts pass.

The machine seal

Elaborated against the built dependencies (lake env lean on the module; not a full lake build — the orchestrator integrates the import serially). #print axioms for both public theorems, verbatim:

'Ctrllib.actuation_ultimate_bound' depends on axioms: [propext, Classical.choice, Quot.sound]
'Ctrllib.actuation_state_ball' depends on axioms: [propext, Classical.choice, Quot.sound]

No sorryAx, nothing beyond the three permitted axioms. The tracked source of truth is (~/Code/vault/lean/ActuationBound.lean); the build copy lives at ~/lean/ctrllib/Ctrllib/ActuationBound.lean, to be imported into Ctrllib.lean by the serial integrator (not touched here).