ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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.

Projectile motion in the constant-field model: planar parabolic trajectory, flight time and level range for stated model data

Physical scope

A worked computation inside the constant-field model of The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance: for a stated initial position, speed and launch angle and a declared constant field parameter, the trajectory is planar and parabolic, the return-to-launch-height time and the level range are computed from the model, and the motion is the unique maximal motion through the datum. The item asserts no measured value of any field strength or launch parameter, models no medium and no drag, and records that the constant-field description of a realistic field is an approximation.

Example

Fix an inertial frame $(o, u, (b_{1}, b_{2}, b_{3}))$ and its adapted coordinates as in Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors. Write $e_{1} = (1, 0, 0)$ , $e_{2} = (0, 1, 0)$ and $e_{3} = (0, 0, 1)$ for the standard coordinate basis of $R^{3}$ . Throughout, $x : R \to R^{3}$ is the coordinate position curve, with coordinate velocity $\dot{x}$ and coordinate acceleration $\ddot{x}$ ; its associated worldline is $γ (t) = o + t u + \sum_{j = 1}^{3} x_{j} (t) b_{j}$ , and its spatial displacement from the frame origin at time $t$ is $\sum_{j} x_{j} (t) b_{j} \in K$ , where $K$ is the spatial displacement space of that definition.

Work in the constant-field model of The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance with one label of mass $m > 0$ , time window $R$ , configuration domain $Q = R^{3}$ , and declared field parameter

$g = - g e_{3}, g > 0, [g] = ℓ τ^{- 2}$

(Dimensions and SI unit conventions of the non-relativistic classical mechanics framework), so that the force map is $F (t, x, v) = m g$ and the equation of motion is $\ddot{x} (t) = - g e_{3}$ . Fix the initial datum

$x (0) = 0, \dot{x} (0) = v_{0} (\cos α e_{1} + \sin α e_{3}), v_{0} > 0, 0 < α < π / 2.$

Verify: the unique maximal motion through the datum is

$x (t) = (v_{0} \cos α) t e_{1} + (v_{0} \sin α t - \frac{1}{2} g t^{2}) e_{3},$

its trajectory lies in the plane $span (e_{1}, e_{3})$ , and for this model the return-to-launch-height time and the level range are

$T_{f} = \frac{2 v_{0} \sin α}{g}, R_{r a n g e} = \frac{v_{0}^{2} \sin (2 α)}{g} .$

The level range and flight time are model quantities computed from the declared parameters: no measured value of $g$ , $v_{0}$ or $α$ is asserted, no medium and no drag are included, and the constant-field description of a realistic field is an approximation recorded with the model.

Facts & Assumptions

Given: The constant-field model with its parameters and the initial datum above.

[L1]

The constant-field model is a force model of the branch Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, with the explicit solution formula $x (t) = x_{0} + v_{0} t + \frac{1}{2} g t^{2}$ for the datum $(x_{0}, v_{0})$ , its uniqueness as the maximal motion, and its frame covariance: The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance claims 1-4, whose proofs use The associated first-order system, motions, maximal motions and the Newtonian flow of a force model and Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder.

[L2]

Componentwise differentiation of $R^{3}$ -valued curves (The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set): sums and scalar multiples are differentiated termwise (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$ ), $(t^{2})^{'} = 2 t$ and $(t)^{'} = 1$ (For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term).

[L3]

The double-angle identity $\sin (2 α) = 2 \sin α \cos α$ (Double-angle and quadratic power-reduction identities).

[L4]

Dimensions and units (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework): $[g] = ℓ τ^{- 2}$ , $[T_{f}] = τ$ and $[R_{r a n g e}] = ℓ$ , read through the dimension rules for quotients and products.

Verification

technique · direct; specialize the uniform-field solution to the projectile datum, then compute the trajectory geometry, the return time and the range, and record the model scope

1.1givenL1algebra

The datum's coordinate triples are $x_{0} = 0 \in R^{3}$ and $v_{0}^{♭} = v_{0} \cos α e_{1} + v_{0} \sin α e_{3} \in R^{3}$ ; the constant-field model with $N = 1$ , $m_{1} = m$ and $g = - g e_{3} \in R^{3}$ is a force model of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance by The uniform-force model: explicit global motion of a label under a constant declared field, with uniqueness, dimensions and frame covariance claim 1, and by its claim 2 the unique maximal motion through $(x_{0}, v_{0}^{♭})$ is $x (t) = v_{0}^{♭} t - \frac{1}{2} g t^{2} e_{3}$ , which is the displayed formula; its maximal interval is all of $R$ .

1.2givenL1L2algebra

Direct verification of the formula, independently of [L1]: differentiating componentwise by [L2] gives $\dot{x} (t) = v_{0} \cos α e_{1} + (v_{0} \sin α - g t) e_{3}$ and $\ddot{x} (t) = - g e_{3} = F (t, x (t), \dot{x} (t)) / m$ ; the initial values are $x (0) = 0$ and $\dot{x} (0) = v_{0} (\cos α e_{1} + \sin α e_{3})$ , so the curve is a motion of the model by The associated first-order system, motions, maximal motions and the Newtonian flow of a force model clause (c), and by Local existence and uniqueness for the Newtonian initial-value problem, with the quantitative Picard-Lindelöf cylinder clause 2 it is the only motion through the datum on any interval containing $0$ .

2.1step 1.1givenalgebra

Planarity: the coefficient of $e_{2}$ in $x (t)$ is $0$ for every $t$ , so the coordinate trajectory lies in the plane spanned by $e_{1}$ and $e_{3}$ ; equivalently $⟨ x (t), e_{2} ⟩ = 0$ for all $t$ for the standard Euclidean inner product on $R^{3}$ . Its spatial displacement therefore lies in $span (b_{1}, b_{3}) \subseteq K$ under the declared coordinate map. Since $v_{0} \cos α > 0$ , eliminating $t = x_{1} / (v_{0} \cos α)$ from the $e_{3}$ -component gives $x_{3} = \tan α x_{1} - \frac{g}{2 v_{0}^{2} \cos^{2} α} x_{1}^{2}$ ; its quadratic coefficient is nonzero because $g > 0$ , so this is a parabola in the stated plane.

3.1step 2.1L3algebra

Return time and range: the height above the launch level is $h (t) : = v_{0} \sin α t - \frac{1}{2} g t^{2}$ ; for $g > 0$ and $v_{0} \sin α > 0$ one has $h (t) = 0$ exactly when $t = 0$ or $t = \frac{2 v_{0} \sin α}{g} = : T_{f}$ , so $T_{f}$ is the positive return-to-launch-height time; the first coordinate at that time is $v_{0} \cos α T_{f} = \frac{2 v_{0}^{2} \sin α \cos α}{g} = \frac{v_{0}^{2} \sin (2 α)}{g}$ by [L3], the displayed range $R_{r a n g e}$ .

4.1step 3.1givenL4algebra∎

Dimensions and scope: $[g] = ℓ τ^{- 2}$ so $[T_{f}] = ℓ τ^{- 1} / (ℓ τ^{- 2}) = τ$ and $[R_{r a n g e}] = ℓ^{2} τ^{- 2} / (ℓ τ^{- 2}) = ℓ$ , consistent with Dimensions and SI unit conventions of the non-relativistic classical mechanics framework; the computation uses no drag term, so it does not describe motion through a medium (compare the drag model The linear drag model: a phenomenological velocity-proportional resistance with a declared coefficient), and a realistic gravitational field is constant only as an approximation, so treating a measured local field strength as the parameter $g$ is an empirical premise with its own conditions and uncertainty.

Remarks

What is and is not model output. The parabola, the flight time and the range are conditional consequences of the adopted constant-field model and the stated datum; they are not measurements, and agreement with a reported observation would test the combined model, apparatus and calibration assumptions rather than prove the model.
The trajectory is planar but the model is three-dimensional. The motion is the restriction to a two-dimensional plane of the three-dimensional model motion; the third direction plays no role for this datum but is part of the model's state space.

Projectile motion in the constant-field model: planar parabolic trajectory, flight time and level range for stated model data

Example

Facts & Assumptions

Verification

Remarks

Depends on

Dependency tree · 2 levels

Sources