ExampleConstruction: AI-adaptedVerification: AI-adapted

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 declared-data impact check: $m_{1} = 2 k g$ , $m_{2} = 6 k g$ , $v_{1}^{-} = 3 m s^{- 1}$ , $v_{2}^{-} = - 1 m s^{- 1}$ , with elastic, semi-elastic and sticking outcomes

Physical scope

A declared-data check of the adopted collinear impact model: masses $2$ and $6 k g$ with one-dimensional velocities $3$ and $- 1 m s^{- 1}$ along the contact direction, for coefficients of restitution $e = 1, \frac{1}{2}, 0$ ; the example verifies total momentum continuity, the impulse $J = - 9 N s$ at $e = \frac{1}{2}$ , the post-impact velocities, and the kinetic-energy changes $0, - 9, - 12 J$ , all in SI units. Every number is declared model data substituted into the model formulas; the example reports no measurement and no empirical comparison.

Example

Declared model data. Adopt a collinear impact of two labels of the contact model of Adopted impact and open-mass extensions of the force branch: the isolated reciprocal impulse model, the collinear restitution contact law and the open-body material accounting clauses (i)-(ii) along the contact direction $n$ , with masses and incoming velocities $m_{1} = 2 k g, m_{2} = 6 k g, v_{1}^{-} = 3 n m s^{- 1}, v_{2}^{-} = - 1 n m s^{- 1} .$ Thus $M = 8 k g$ , $μ = \frac{2 \cdot 6}{8} = \frac{3}{2} k g$ , $V = \frac{2 \cdot 3 + 6 \cdot (- 1)}{8} = 0$ , and the relative velocity is $d^{-} : = v_{2}^{-} - v_{1}^{-} = - 4 n m s^{- 1}$ .

Assertions to check. For $e = 1$ (elastic): $v_{1}^{+} = - 3 n$ , $v_{2}^{+} = + 1 n$ , $Δ K = 0$ . For $e = \frac{1}{2}$ : $v_{1}^{+} = - \frac{3}{2} n$ , $v_{2}^{+} = + \frac{1}{2} n$ , impulse $J = - 9 n N s$ , $Δ K = - 9 J$ . For $e = 0$ (sticking): $v_{1}^{+} = v_{2}^{+} = 0$ , $Δ K = - 12 J$ . In every case the total momentum $P = 0$ is continuous across the impact, as Consequences of the adopted impact and open-mass models: continuity of total momentum, the smooth-force exclusion, the restitution solution with $Δ K = - \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ , and the open-body and rocket laws clause 1 requires, and the energy changes are those of its clause 4.

Facts & Assumptions

Given: The declared masses, incoming velocities and contact direction; the collinear impact model of Adopted impact and open-mass extensions of the force branch: the isolated reciprocal impulse model, the collinear restitution contact law and the open-body material accounting with coefficients $e \in {0, \frac{1}{2}, 1}$ ; the vocabulary and units of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework and Total mass, total momentum, centre of mass, angular momentum, torque, kinetic energy, power and work of a particle model in an inertial frame.

[L1]

Impact consequences (Consequences of the adopted impact and open-mass models: continuity of total momentum, the smooth-force exclusion, the restitution solution with $Δ K = - \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ , and the open-body and rocket laws clauses 1, 3, 4, Isolated reciprocal impulse with full-vector restitution: momentum jumps $\pm J$ , conservation of total momentum, the restitution solution and the kinetic-energy change $- \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ clauses a-c): in the collinear model, $m_{1} (v_{1}^{+} - v_{1}^{-}) = J = - m_{2} (v_{2}^{+} - v_{2}^{-})$ with total momentum continuous across the impact; $v_{1}^{+} = V + \frac{m_{2}}{M} e d^{-}$ , $v_{2}^{+} = V - \frac{m_{1}}{M} e d^{-}$ ; and $Δ K = - \frac{1 - e^{2}}{2} μ ∥ d^{-} ∥_{2}^{2}$ .

[L2]

Kinetic split (Centre of mass, the identity $\sum_{i} m_{i} ρ_{i} = 0$ , and the splitting of the kinetic sum $\sum_{i} m_{i} ∥ x_{i}^{'} ∥_{2}^{2}$ into centre-of-mass and relative parts (with the two-body reduced-mass case), The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ ): $K^{\pm} = \frac{M}{2} ∥ V ∥_{2}^{2} + \frac{μ}{2} ∥ d^{\pm} ∥_{2}^{2}$ on the respective sides of impact, where $d^{\pm} = v_{2}^{\pm} - v_{1}^{\pm}$ , with $V$ unchanged across the impact.

Verification

technique · direct

1.1givenL1L2algebra

Common data: $M = 8$ , $μ = \frac{3}{2}$ , $V = 0$ and $d^{-} = - 4 n$ , so $∥ d^{-} ∥_{2}^{2} = 16$ and $\frac{μ}{2} ∥ d^{-} ∥_{2}^{2} = 12 J$ ; the initial kinetic energy is $\frac{1}{2} \cdot 2 \cdot 9 + \frac{1}{2} \cdot 6 \cdot 1 = 9 + 3 = 12 J$ ; the incoming relative speed is $4 m s^{- 1}$ .

2.1step 1.1L1L2algebra

Elastic case $e = 1$ : [L1] gives $v_{1}^{+} = V + \frac{m_{2}}{M} d^{-} = \frac{6}{8} (- 4) n = - 3 n$ and $v_{2}^{+} = V - \frac{m_{1}}{M} d^{-} = - \frac{2}{8} (- 4) n = + 1 n$ , so each velocity is reversed and the total momentum is $2 (- 3) + 6 (1) = 0 = P^{-}$ ; $Δ K = - \frac{1 - 1}{2} μ ∥ d^{-} ∥_{2}^{2} = 0$ , and directly $K^{+} = \frac{1}{2} \cdot 2 \cdot 9 + \frac{1}{2} \cdot 6 \cdot 1 = 12 J = K^{-}$ .

2.2step 1.1L1L2algebra

Semi-elastic case $e = \frac{1}{2}$ : $v_{1}^{+} = \frac{6}{8} \cdot \frac{1}{2} \cdot (- 4) n = - \frac{3}{2} n$ , $v_{2}^{+} = - \frac{2}{8} \cdot \frac{1}{2} \cdot (- 4) n = + \frac{1}{2} n$ ; the impulse is $J = m_{1} (v_{1}^{+} - v_{1}^{-}) = 2 (- \frac{3}{2} - 3) n = - 9 n N s$ , and indeed $m_{2} (v_{2}^{+} - v_{2}^{-}) = 6 (\frac{1}{2} + 1) n = 9 n = - J$ ; the total momentum is $2 (- \frac{3}{2}) + 6 (\frac{1}{2}) = 0 = P^{-}$ ; $Δ K = - \frac{1 - \frac{1}{4}}{2} \cdot \frac{3}{2} \cdot 16 = - \frac{3}{4} \cdot 12 = - 9 J$ , and directly $K^{+} = \frac{1}{2} \cdot 2 \cdot \frac{9}{4} + \frac{1}{2} \cdot 6 \cdot \frac{1}{4} = \frac{9}{4} + \frac{3}{4} = 3 J = 12 - 9$ .

2.3step 1.1L1L2algebra

Sticking case $e = 0$ : $v_{1}^{+} = v_{2}^{+} = V = 0$ ; the total momentum is $0 = P^{-}$ ; $Δ K = - \frac{1}{2} \cdot \frac{3}{2} \cdot 16 = - 12 J$ , so $K^{+} = 0$ ; the impulse is $J = 2 (0 - 3) n = - 6 n N s$ , consistent with $m_{2} (0 + 1) n = 6 n = - J$ .

3.1step 2.1step 2.2step 2.3givenL1∎

Reading: all three outcomes satisfy the reciprocal impulse equations with different impulses and different energy changes; the momentum data alone ( $P = 0$ ) are compatible with all of them, illustrating clause 5 of Consequences of the adopted impact and open-mass models: continuity of total momentum, the smooth-force exclusion, the restitution solution with $Δ K = - \frac{1 - e^{2}}{2} μ ∥ v_{2}^{-} - v_{1}^{-} ∥_{2}^{2}$ , and the open-body and rocket laws: the coefficient $e$ is model data and must be supplied by the contact law. Every number above is a declared model datum substituted into the model formulas; no measurement, uncertainty or empirical inference is involved.

Remarks

Units. $[P] = k g m s^{- 1} = μ ℓ τ^{- 1}$ , $[J] = N s = μ ℓ τ^{- 1}$ , $[K] = J = μ ℓ^{2} τ^{- 2}$ (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework); the impulse values displayed are the model's impulse vector components along $n$ .
Frame reading. The one-sided centre-of-mass velocities at the impact are both zero. Thus the centre-of-mass kinetic energy is zero on both sides of that instant: the elastic case reverses the relative velocity, and the inelastic cases decrease its kinetic energy only. The supplied data do not imply rest at other times; external forces can accelerate the centre of mass away from the impact.

A declared-data impact check: $m_{1} = 2 k g$ , $m_{2} = 6 k g$ , $v_{1}^{-} = 3 m s^{- 1}$ , $v_{2}^{-} = - 1 m s^{- 1}$ , with elastic, semi-elastic and sticking outcomes

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

A declared-data impact check: m1=2 kgm1​=2kg, m2=6 kgm2​=6kg, v1−=3 m s−1v1−​=3ms−1, v2−=−1 m s−1v2−​=−1ms−1, with elastic, semi-elastic and sticking outcomes

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources

A declared-data impact check: $m_{1} = 2 k g$ , $m_{2} = 6 k g$ , $v_{1}^{-} = 3 m s^{- 1}$ , $v_{2}^{-} = - 1 m s^{- 1}$ , with elastic, semi-elastic and sticking outcomes