Automatic Dynamic Parallelotope Bundles for Reachability Analysis of Nonlinear Systems

Lemma 1 claims TransformBundle returns a sound overapproximation Q′ of f(Q) for x^+ = f(x). The paper’s argument uses: (i) bundle semantics Q = ⋂ P_i and the generator/half-space representations (Equations (3) and (5)), (ii) reduction of max/min over a parallelotope to an optBox over α ∈ [0,1]^n (Equations (7)–(8)), and (iii) Algorithm 1’s updates c′u[i] ← min_P optBox(T_i·f) and c′l[i] ← max_P(−optBox(−T_i·f)), followed by constructing Q′ from T, c′l, c′u. This yields min-over-upper-bounds and max-over-lower-bounds across all P ∈ Q, establishing f(Q) ⊆ Q′ (statement of Lemma 1) . The candidate solution formalizes the same reasoning: it fixes x ∈ Q, reparameterizes P via x = a + Σ α_j g_j, applies optBox to h_i^P(α) = T_i f(a + Σ α_j g_j) to obtain U_i(P) and L_i(P), then shows L_i(P) ≤ T_i f(x) ≤ U_i(P) for each P and concludes c′l[i] ≤ T_i f(x) ≤ c′u[i] for all i, hence f(x) ∈ Q′. This matches the paper’s proof sketch step-for-step, adding a clear quantifier structure and the consistency note c′l ≤ c′u. Therefore, both are correct and substantially the same proof.