ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-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.

A bouncing-ball impact has a transverse event-time and reset-error bound

Example

Let $q$ be height and $v$ velocity, with mode field $q^{'} = v$ , $v^{'} = - 2$ before and after impacts, initial state $(q (0), v (0)) = (1, 0)$ , downward guard $g (q, v) = q$ of orientation $σ = - 1$ , and time-independent reset $R (q, v) = (0, - v / 2)$ . On the event bracket $[1, 51 / 50]$ , use the approximate incoming reconstruction $U (t) = (1 - t^{2} + 1 / 25, - 2 t) .$ It has uniform state error $η = 1 / 25$ from the exact incoming solution $y (t) = (1 - t^{2}, - 2 t)$ . The reported guard root is $\hat{τ} = \sqrt{26 / 25}$ , and the exact impact time is $τ = 1$ . This example isolates the event-time and reset estimates; it does not claim that $U$ is a residual-certified reconstruction from the exact initial state.

Facts & Assumptions

Given: A smooth hybrid mode and reset, the transverse event-time estimate, and the mistimed-reset estimate.

[F1]

Smooth hybrid ODE modes, guards, resets, and deterministic event priority: a mode follows its ODE until an oriented guard crossing, then applies its reset and changes mode.

[F2]

A transverse hybrid event time is stable under dense-output and root error: if the exact guard has signed derivative at least $ν > 0$ , the dense state error is at most $η$ , and the reported guard residual is at most $ε$ , then $∣ \hat{τ} - τ ∣ \leq (L_{g} η + ε) / ν$ .

[F3]

Reset and smooth-mode flow propagate a transverse event-time error: with incoming error $η$ , event-time error $Δ$ , reset constants $L_{R}, L_{R, t}$ , and incoming/outgoing field bounds $M^{-}, M^{+}$ , the aligned post-reset error is at most $L_{R} η + (L_{R} M^{-} + L_{R, t} + M^{+}) Δ$ .

Verification

1.1givenF1algebra

The exact incoming solution is $y (t) = (1 - t^{2}, - 2 t)$ , so its guard $h (t) = 1 - t^{2}$ has the unique root $τ = 1$ on the bracket. For $t \in [1, 51 / 50]$ , $- h^{'} (t) = 2 t \geq 2$ , so the downward crossing is transverse with margin $ν = 2$ .

2.1givenstep 1.1algebra

The dense guard is $1 - t^{2} + 1 / 25$ , whose root in the bracket is $\hat{τ} = \sqrt{26 / 25}$ and whose residual there is $ε = 0$ . For $x \geq 0$ , both sides are nonnegative and $(1 + x / 2)^{2} - (1 + x) = x^{2} / 4 \geq 0$ , so $\sqrt{1 + x} \leq 1 + x / 2$ . Taking $x = 1 / 25$ gives $0 \leq \hat{τ} - τ \leq 1 / 50$ .

3.1givenF2step 1.1step 2.1algebra

On the bracket, $∥ U (t) - y (t) ∥_{2} = 1 / 25$ . Since $g (q, v) = q$ , $∣ g (q_{1}, v_{1}) - g (q_{2}, v_{2}) ∣ = ∣ q_{1} - q_{2} ∣ \leq ∥ (q_{1}, v_{1}) - (q_{2}, v_{2}) ∥_{2}$ , so $L_{g} = 1$ ; the reported guard residual is zero. Apply [F2] with $ν = 2$ to obtain $∣ \hat{τ} - τ ∣ \leq (1 / 25) / 2 = 1 / 50$ , agreeing with the explicit bound in step 2.1.

4.1givenF3step 1.1step 3.1algebra

The reset is defined on all of $R^{2}$ , is $L_{R} = 1 / 2$ -Lipschitz in state, and has $L_{R, t} = 0$ . On the incoming bracket, $∥ U (t) - y (t) ∥_{2} = 1 / 25$ and $∥ f^{-} (t, y (t)) ∥_{2} = \sqrt{4 t^{2} + 4} < 3$ . Step 3.1 gives $∣ \hat{τ} - τ ∣ \leq 1 / 50$ . The outgoing field $(q, v) \mapsto (v, - 2)$ is globally $1$ -Lipschitz in state. The exact outgoing path through $\hat{τ}$ and the reported reset state lie in $[- 1 / 10, 1 / 10] \times [4 / 5, 6 / 5]$ , where the field norm is less than $3$ ; by local existence and continuity both outgoing solutions remain in the bounded convex rectangle $[- 1 / 5, 1 / 5] \times [3 / 4, 5 / 4]$ for a short common forward interval. Thus the reset and outgoing tube hypotheses of [F3] hold with $M^{-} = M^{+} = 3$ and $L^{+} = 1$ . By [F3], the aligned post-reset error is at most $\frac{1}{2} \cdot \frac{1}{25} + (\frac{1}{2} \cdot 3 + 3) \frac{1}{50} = 11 / 100$ .

5.1givenstep 2.1step 4.1algebra∎

Directly, the exact outgoing state at $\hat{τ} = 1 + Δ$ is $(Δ - Δ^{2}, 1 - 2 Δ)$ and the reported reset state is $(0, 1 + Δ)$ . Their difference has components bounded by $1 / 50$ and $3 / 50$ , so its Euclidean norm is at most $\sqrt{(1 / 50)^{2} + (3 / 50)^{2}} < 11 / 100$ . This verifies the reset estimate for this instance.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Joel M. Esposito, Vijay Kumar, and George J. Pappas, Accurate Event Detection for Simulating Hybrid Systems, HSCC 2001, pp. 204–217 (standard reference, not scraped)
Gerald Teschl, Ordinary Differential Equations and Dynamical Systems, §2.4 (standard reference, not scraped)