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.
All four inertial terms checked on explicit data, and the exact return to an inertial chart
A worked finite check of the moving-chart equation of the framework: a zero-force one-label model observed in a chart with a uniformly accelerated rotation angle and a uniformly accelerated reference curve; the four inertial terms are evaluated term by term at one time and compared with the moving-chart coordinate acceleration of the motion, a chart with nonzero angular velocity is identified as non-inertial by the criterion, and an explicit chart with affine reference curve and constant rotation is checked to reproduce the inertial-frame description. All values are model values; the example reports no measurement.
Example
Declare a one-label model of the force branch of Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance with , mass , time window , configuration domain and the zero force map (admissible: constant, hence of the standing regularity), in a fixed inertial frame with adapted coordinates (Inertial frames, stationary observers and the adopted Galilean transformations between frames, Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). For real parameters , vectors and Moving spatial charts of an inertial frame: rotating and translating coordinates, angular velocity and inertial terms data, take to be a dimensionless angle in radians, with , , , and for each spatial component : consider the motion of the zero-force model with , , its moving-chart coordinate curve , and the inertial-terms field .
Then, for the parameter values , , and :
- is and has the angular velocity and , while ;
- , , and the moving-chart coordinate acceleration is (in units ); the inertial-chart acceleration is for every ;
- the four inertial terms at are , , and , and their sum is ; clause 1 of The equation of motion in a moving chart: inertial terms, inertial forces, and when it restricts to an inertial chart therefore holds at for these data, with ;
- because , clause 3 of that theorem identifies the chart as not inertial; and with the alternative parameters , , , the chart has constant rotation and affine reference curve, hence vanishing inertial terms, and the same motion has in the chart, which is the inertial-frame description with .
All values are model values in the declared coordinates; the example reports no measurement and asserts nothing about any apparatus.
Facts & Assumptions
Given: The constants and parameters of the Example, the zero-force model, the moving chart with , the motion , and the curve .
The chart (Moving spatial charts of an inertial frame: rotating and translating coordinates, angular velocity and inertial terms): with skew and unique representing vector , ; is the moving-chart coordinate curve; is the inertial-terms field of clause (d).
The moving-chart equation (The equation of motion in a moving chart: inertial terms, inertial forces, and when it restricts to an inertial chart clauses 1,2,3): along a motion; the inertial terms vanish identically exactly when is constant and is affine, in which case the chart is an inertial frame's chart and the equation reduces to the covariance law.
The zero-force model and its motions: is of class with the standing regularity; is a motion of the model in the sense of The associated first-order system, motions, maximal motions and the Newtonian flow of a force model clause (c), because (Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance, Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors).
Rotation and trigonometry: as displayed lies in with ; the derivatives of sine and cosine, the identity , the chain rule and the componentwise algebra of derivatives; the cross product of the standard basis (The orthogonal group and the rotation group , is a subgroup of the general linear group, with , Sine and cosine defined by their real power series, The derivatives of sine and cosine are cosine and minus sine, Parity and the Pythagorean identity for sine and cosine, The chain rule for total derivatives: , Sums, scalar multiples, products and quotients: , , , and when , The cross product in , The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral, The Euclidean inner product on ).
The kinematic identity of the chart (Angular velocity of a moving frame and the rotating-frame acceleration identity clause 3): for the curves of the chart; and .
Intervals and constants (Intervals of : the nine order-convex forms, nondegeneracy, and length); the chart's data are defined for all .
Verification
Chart quantities: is the rotation about by the angle , so and by [F4], and is because sine, cosine and the polynomial are on the interval ([F6]); differentiating gives for the parameter values of the Example, and .
The motion and its chart acceleration at : the curve has , so it is a motion of the zero-force model by [F3]. At one has , , and , so and, differentiating at with , . Differentiating once more at , , using and with , : , and , so .
The four inertial terms at and the identity: with , , , , and from steps 1.1 and 1.2, the four terms of are , , and ; their sum is , which equals of step 1.2, so and clause 1 of [F2] holds at for these data (with ).
The inertial case checked: with , and one has , and affine, so , and ; the inertial terms vanish identically by [F2] clause 3, and the chart is the adapted chart of the inertial frame related to by the Galilean transformation with , and . For the same motion one gets and , consistent with .
The chart is not inertial: since is not identically zero on , is not constant, so by clause 3 of [F2] the inertial terms do not vanish identically and the chart is not the adapted chart of an inertial frame; the four-term computation of the preceding check exhibits the nonvanishing explicitly at .
The Example's clauses are proved: clause 1 is step 1.1, clauses 2 and 3 are steps 1.2 and 2.1, the non-inertial verdict is step 2.3, and the exact return to an inertial chart is step 2.2.
Remarks
-
Reading the terms. On this data the Coriolis term and the centrifugal term cancel () and the Euler and translational terms add, so the example is a check of the individual terms rather than of any one of them. A motion with not aligned as here separates the Coriolis contribution; the companion pendulum and bead examples do not use a moving chart at all.
-
No equivalence principle. The non-inertial chart's terms are computed from its own motion data; nothing in the example compares them with a gravitational field, and the zero-force model remains force-free in every chart.
Depends on
Moving spatial charts of an inertial frame: rotating and translating coordinates, angular velocity and inertial terms
The equation of motion in a moving chart: inertial terms, inertial forces, and when it restricts to an inertial chart
Adopted force model: force maps, the equation of motion, additive composition of force contributions and frame covariance
The associated first-order system, motions, maximal motions and the Newtonian flow of a force model
Inertial frames, stationary observers and the adopted Galilean transformations between frames
Coordinate velocity and acceleration of a worldline in an inertial frame, and the spatial velocity and acceleration vectors
Dimensions and SI unit conventions of the non-relativistic classical mechanics framework
Angular velocity of a moving frame and the rotating-frame acceleration identity
The orthogonal group and the rotation group
is a subgroup of the general linear group, with
The cross product in
The Euclidean inner product on
Sine and cosine defined by their real power series
The derivatives of sine and cosine are cosine and minus sine
Parity and the Pythagorean identity for sine and cosine
The chain rule for total derivatives:
Sums, scalar multiples, products and quotients: , , , and when
The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral
Intervals of : the nine order-convex forms, nondegeneracy, and length
Dependency tree · 2 levels
Sources
- D. Tong, Dynamics and Relativity (Cambridge lecture notes, Lent 2013), Sections 6.1-6.2, Eqs. (6.4)-(6.5), printed pages 94-95 (PDF pages 100-101): the acceleration transfer to a rotating frame and the Coriolis, centrifugal and Euler terms
- K. K. Likharev, Essential Graduate Physics, Part CM: Classical Mechanics (title page last edited September 1, 2026), Section 4.6, Eqs. (4.88)-(4.92), chapter pages 21-23 (PDF pages 76-78): velocity and acceleration transfer and the four inertial-force terms, with the frame-motion terms a0 and omega-dot
- D. Tong, Classical Dynamics (Cambridge lecture notes, January 2015 printing), Section 3.1.1, printed pages 47-49 (PDF pages 53-55): the angular velocity of a rotating basis in the convention R^T Rdot