LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The derivative of a guard along an ODE mode is its Lie derivative

Statement

Let $y$ be a differentiable solution in mode $m$ on an interval $J$ , with $y^{'} (t) = f_{m} (t, y (t))$ . Let $g (t, x)$ be $C^{1}$ on an open neighborhood of the graph of $y$ , and define $h (t) = g (t, y (t))$ . Then $h$ is differentiable on $J$ and $h^{'} (t) = \partial_{t} g (t, y (t)) + D_{x} g (t, y (t)) f_{m} (t, y (t)) .$

Facts & Assumptions

Given: A mode solution $y^{'} = f_{m} (t, y)$ and a $C^{1}$ guard $g$ on a neighborhood of its graph.

[F1]

Smooth hybrid ODE modes, guards, resets, and deterministic event priority: a solution in mode $m$ satisfies the first-order ODE $y^{'} = f_{m} (t, y)$ .

[F2]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : for differentiable maps $z$ and $g$ , the derivative of $g \circ z$ is $D g (z (t)) z^{'} (t)$ .

[F3]

Continuously differentiable maps, local inverses, and local diffeomorphisms: a $C^{1}$ map on an open set is totally differentiable at every point of its domain.

Proof

1.1givenF1construct

Set $z (t) = (t, y (t))$ . Domain-relative differentiability of $y$ gives $z^{'} (t) = (1, y^{'} (t)) = (1, f_{m} (t, y (t)))$ and $z (t + h) = z (t) + h z^{'} (t) + o (∣ h ∣)$ for admissible $h$ with $t + h \in J$ .

2.1F2F3step 1.1algebra∎

At interior points of $J$ , [F2] gives $(g \circ z)^{'} (t) = D g (z (t)) z^{'} (t)$ . At an endpoint, use admissible increments in step 1.1 and the total differentiability of $g$ from [F3]: with $k = z (t + h) - z (t) = h z^{'} (t) + o (∣ h ∣)$ , its first-order expansion gives $g (z (t + h)) - g (z (t)) = D g (z (t)) k + o (∥ k ∥) = h D g (z (t)) z^{'} (t) + o (∣ h ∣)$ , proving the same one-sided derivative formula. Splitting the derivative into its time and state blocks gives the displayed identity.

Depends on

Used by

Dependency tree · two levels

10 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Nathan J. Kong, J. Joe Payne, James Zhu, and Aaron M. Johnson, Saltation Matrices: The Essential Tool for Linearizing Hybrid Dynamical Systems (standard reference, not scraped)