LemmaStatement: AI-adaptedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Sphere-contact guards, normals and binary resets have explicit tube bounds

Statement

Use the Euclidean norm on the full state $z = (q_{1}, \dots, q_{P}, v_{1}, \dots, v_{P})$ of $P \geq 2$ spheres in $R^{d}$ . Fix a pair $i < j$ , positive masses $m_{i}, m_{j}$ , positive radii $r_{i}, r_{j}$ , and a fixed restitution coefficient $e \in [0, 1]$ . Put $d_{i j} = q_{i} - q_{j}, n (z) = \frac{d_{i j}}{∥ d_{i j} ∥_{2}}, γ (z) = ∥ d_{i j} ∥_{2} - r_{i} - r_{j},$ $α = m_{i}^{- 1} + m_{j}^{- 1}, κ = \frac{1 + e}{α}, β = \sqrt{m_{i}^{- 2} + m_{j}^{- 2}} .$ Extend the binary reset formula of Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact to every state with $d_{i j} \neq 0$ by setting $J (z) = - κ ⟨ v_{i} - v_{j}, n (z) ⟩$ , replacing $v_{i}$ by $v_{i} + J (z) n (z) / m_{i}$ and $v_{j}$ by $v_{j} - J (z) n (z) / m_{j}$ , and leaving all other coordinates unchanged. Denote this time-independent reset extension by $R (z)$ .

The functions $γ, n, R$ are $C^{1}$ on the open set $d_{i j} \neq 0$ . For two states $z, z^{'}$ with both pair distances at least $σ > 0$ and both relative velocity norms at most $V \geq 0$ , $∣ γ (z) - γ (z^{'}) ∣ \leq \sqrt{2} ∥ z - z^{'} ∥_{2}, ∥ n (z) - n (z^{'}) ∥_{2} \leq \frac{2 \sqrt{2}}{σ} ∥ z - z^{'} ∥_{2},$ $∥ R (z) - R (z^{'}) ∥_{2} \leq L_{R} ∥ z - z^{'} ∥_{2}, L_{R} : = 1 + \sqrt{2} β κ (1 + \frac{4 V}{σ}) .$ These pairwise bounds do not require a convex collision-free state set. Along a differentiable smooth segment with $q_{k}^{'} = v_{k}$ , $\frac{d}{d t} γ (z (t)) = ⟨ n (z (t)), v_{i} (t) - v_{j} (t) ⟩ .$ The normal bound $2 / σ$ applies to differences of the relative vectors $d_{i j}$ ; its full-state version includes the factor $\sqrt{2}$ . This extension does not assert that an approximate state is exactly at contact or that an event exists.

Facts & Assumptions

Given: The stated pair, fixed masses/radii/restitution, two states with separated pair centers and bounded relative velocities, and the Euclidean full-state norm.

[F1]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ fixes the bilinear inner product and squared Euclidean norm.

[F2]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation gives Cauchy–Schwarz, the Euclidean triangle inequality and norm homogeneity.

[F3]

Impulse, momentum, and kinetic-energy laws for an isolated frictionless sphere impact supplies the impulse and equal/opposite binary velocity updates at an exact incoming contact.

[F4]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ give the chain rule and the scalar coordinate sum, product and quotient rules with nonzero denominators.

[F5]

If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: continuous first partial derivatives on an open set give total differentiability, with its derivative given by those partials.

Proof

1.1givenF1F2algebra

Write $a = ∥ d_{i j} ∥_{2}$ and $a^{'} = ∥ d_{i j}^{'} ∥_{2}$ . By [F2], $∣ a - a^{'} ∣ \leq ∥ d_{i j} - d_{i j}^{'} ∥_{2}$ . Also $∥ d_{i j} - d_{i j}^{'} ∥_{2} \leq ∥ q_{i} - q_{i}^{'} ∥_{2} + ∥ q_{j} - q_{j}^{'} ∥_{2} \leq \sqrt{2} ∥ q - q^{'} ∥_{2} \leq \sqrt{2} ∥ z - z^{'} ∥_{2}$ . Subtracting the fixed radii gives the guard bound.

2.1givenF2step 1.1algebra

The identity $n - n^{'} = (d_{i j} - d_{i j}^{'}) / a + d_{i j}^{'} (1 / a - 1 / a^{'})$ and step 1.1 give $∥ n - n^{'} ∥_{2} \leq ∥ d_{i j} - d_{i j}^{'} ∥_{2} / a + ∣ a - a^{'} ∣ / a \leq 2 ∥ d_{i j} - d_{i j}^{'} ∥_{2} / σ$ . Applying the full-state estimate from step 1.1 gives the asserted normal bound.

3.1givenF2F3step 1.1step 2.1algebra

Put $w = v_{i} - v_{j}$ and $w^{'} = v_{i}^{'} - v_{j}^{'}$ . The impulse formula in [F3], used as the stated extension, gives $∣ J - J^{'} ∣ \leq κ (∥ w - w^{'} ∥_{2} + ∥ w^{'} ∥_{2} ∥ n - n^{'} ∥_{2}) \leq κ (\sqrt{2} ∥ v - v^{'} ∥_{2} + \frac{2 \sqrt{2} V}{σ} ∥ q - q^{'} ∥_{2}),$ and $∣ J^{'} ∣ \leq κ V$ . The two changed velocity increments have joint norm difference $β ∥ J n - J^{'} n^{'} ∥_{2}$ , which is at most $β (∣ J - J^{'} ∣ + ∣ J^{'} ∣ ∥ n - n^{'} ∥_{2})$ .

4.1givenF2step 2.1step 3.1algebra

Combining steps 2.1–3.1 bounds the reset-increment difference by $\sqrt{2} β κ (∥ v - v^{'} ∥_{2} + 4 V ∥ q - q^{'} ∥_{2} / σ)$ . Each coordinate-block norm is at most $∥ z - z^{'} ∥_{2}$ . The identity part of the reset contributes at most $∥ z - z^{'} ∥_{2}$ by [F2], giving exactly the stated $L_{R}$ . This argument compares the two endpoints directly and uses no connecting line segment.

5.1givenF1F2F4F5algebra∎

For a nonzero vector $d$ and increment $h$ , rationalization gives $∥ d + h ∥_{2} - ∥ d ∥_{2} = \frac{2 ⟨ d, h ⟩ + ∥ h ∥_{2}^{2}}{∥ d + h ∥_{2} + ∥ d ∥_{2}} .$ The denominator tends to $2 ∥ d ∥_{2} > 0$ , so the total derivative is $h \mapsto ⟨ d / ∥ d ∥_{2}, h ⟩$ , continuously dependent on $d \neq 0$ . The coordinate rules in [F4] give continuous partial derivatives for the quotient defining $n$ and the products defining $R$ on this open set; [F5] makes them $C^{1}$ . Applying [F4] along $d_{i j}^{'} = v_{i} - v_{j}$ proves the guard derivative formula.

Depends on

Used by

Event-driven integration for isolated frictionless spherical impacts Algorithm

Dependency tree · two levels

42 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

David E. Stewart, Dynamics with Inequalities: Impacts and Hard Constraints (standard reference, not scraped)