Alphabeta Math
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.

All four inertial terms checked on explicit data, and the exact return to an inertial chart

Physical scope

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 N=1, mass m=1 kg, time window I0=R, configuration domain Q=R3 and the zero force map F:I0×Q×R3⟶R3,F(t,x,v)≡0 (admissible: constant, hence of the standing regularity), in a fixed inertial frame F with adapted coordinates (t,x) (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 ω0,β,γ, vectors a0,vc∈R3 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 [ω0]=τ−1, [β]=τ−2, [γ]=ℓτ−2, [a0,j]=ℓ and [vc,j]=ℓτ−1 for each spatial component j: θ(t):=ω0t+12βt2,R(t):=(cos⁡θ(t)−sin⁡θ(t)0sin⁡θ(t)cos⁡θ(t)0001),c(t):=a0+vct+12γt2e1, consider the motion x(t):=x0+v t of the zero-force model with x0=(1,0,0) m, v=(0,1,0) m s−1, its moving-chart coordinate curve y(t)=R(t)T(x(t)−c(t)), and the inertial-terms field τ(t,y,y˙)=−(2ω(t)×y˙+ω′(t)×y+ω(t)×(ω(t)×y)+R(t)Tc′′(t)).

Then, for the parameter values ω0=2 s−1, β=1 s−2, γ=3 m s−2 and a0=vc=0:

  1. R(t)∈SO(3) is C∞ and Ω=RTR′ has the angular velocity ω(t)=θ′(t)e3=(2+t)e3 and ω′(t)=e3, while c′′(t)=(3,0,0);
  2. y(0)=e1, y˙(0)=−e2, and the moving-chart coordinate acceleration is y¨(0)=−3e1−e2 (in units m s−2); the inertial-chart acceleration is x¨(t)=0 for every t;
  3. the four inertial terms at t=0 are −2ω×y˙=−4e1, −ω′×y=−e2, −ω×(ω×y)=+4e1 and −RTc′′=−3e1, and their sum is τ(0,y(0),y˙(0))=−3e1−e2=y¨(0); 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 t=0 for these data, with my¨=RTF+mτ=mτ;
  4. because ω≢0, clause 3 of that theorem identifies the chart as not inertial; and with the alternative parameters ω0=β=γ=0, a0=(1,0,0), vc=(0,1,0), the chart has constant rotation R≡I3 and affine reference curve, hence vanishing inertial terms, and the same motion has y¨≡0 in the chart, which is the inertial-frame description with y(t)=x(t)−a0−vct.

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 (I,c,R) with I=R, the motion x(t)=x0+vt, and the curve y(t)=R(t)T(x(t)−c(t)).

[F1]

The chart (Moving spatial charts of an inertial frame: rotating and translating coordinates, angular velocity and inertial terms): R(t)∈SO(3) with Ω=RTR′ skew and unique representing vector ω, Ωz=ω×z; y is the moving-chart coordinate curve; τ is the inertial-terms field of clause (d).

[F2]

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): my¨i=RTFi+mτ along a motion; the inertial terms vanish identically exactly when R is constant and c is affine, in which case the chart is an inertial frame's chart and the equation reduces to the covariance law.

[F5]

The kinematic identity of the chart (Angular velocity of a moving frame and the rotating-frame acceleration identity clause 3): RTx′′=y′′+2ω×y′+ω′×y+ω×(ω×y)+RTc′′ for the curves of the chart; and ∥Rz∥2=∥z∥2.

[F6]

Intervals and constants (Intervals of R: the nine order-convex forms, nondegeneracy, and length); the chart's data are defined for all t∈R.

Verification

technique · direct; compute the chart quantities, evaluate the two sides of the moving-chart equation on explicit data at one time, and check the inertial and non-inertial cases against the criterion
1.1F1F4F6givenalgebra

Chart quantities: R(t) is the rotation about e3 by the angle θ(t), so R(t)TR(t)=I3 and det⁡R(t)=cos⁡2θ+sin⁡2θ=1 by [F4], and R is C∞ because sine, cosine and the polynomial θ are on the interval I=R ([F6]); differentiating Ω=RTR′ gives Ω(t)=θ′(t)(0−10100000),soω(t)=θ′(t)e3=(2+t)e3,ω′(t)=e3 for the parameter values of the Example, and c′′(t)=γe1=3e1.

1.2F3F4givenalgebra

The motion and its chart acceleration at t=0: the curve x(t)=x0+vt has x′′=0, so it is a motion of the zero-force model by [F3]. At t=0 one has θ(0)=0, R(0)=I3, c(0)=0 and c′(0)=0, so y(0)=x0=e1 and, differentiating y=RT(x−c) at t=0 with Ω(0)=2 [e3]×, y˙(0)=−Ω(0)y(0)+x′(0)−c′(0)=−2e3×e1+e2=−2e2+e2=−e2. Differentiating once more at t=0, y¨(0)=−(Ω(0)2+Ω′(0))y(0)−2Ω(0)y˙(0)+x′′(0)−c′′(0), using Ω′(0)=θ′′(0)[e3]×=[e3]× and Ω(0)2=4[e3]×2 with [e3]×e1=e2, [e3]×e2=−e1: −(Ω2+Ω′)y(0)=4e1−e2, −2Ω(0)y˙(0)=−4[e3]×(−e2)=−4e1 and −c′′(0)=−3e1, so y¨(0)=−3e1−e2.

2.1F2F4step 1.1step 1.2algebra

The four inertial terms at t=0 and the identity: with ω(0)=2e3, ω′(0)=e3, R(0)=I3, y(0)=e1, y˙(0)=−e2 and c′′(0)=3e1 from steps 1.1 and 1.2, the four terms of τ are −2ω×y˙=−4(e3×(−e2))=−4e1, −ω′×y=−(e3×e1)=−e2, −ω×(ω×y)=−2e3×(2e3×e1)=−4(e3×e2)=4e1 and −RTc′′=−3e1; their sum is τ(0,e1,−e2)=−4e1−e2+4e1−3e1=−3e1−e2, which equals y¨(0) of step 1.2, so my¨(0)=mτ(0,e1,−e2) and clause 1 of [F2] holds at t=0 for these data (with F=0).

2.2F2F3F5step 1.1algebra

The inertial case checked: with ω0=β=γ=0, a0=(1,0,0) and vc=(0,1,0) one has θ≡0, R≡I3 and c(t)=a0+vct affine, so ω≡0, ω′≡0 and c′′≡0; the inertial terms vanish identically by [F2] clause 3, and the chart is the adapted chart of the inertial frame related to F by the Galilean transformation y=Qx+v∗t+a0∗ with Q=I3, v∗=−vc=(0,−1,0) and a0∗=−a0=(−1,0,0). For the same motion x(t)=x0+vt one gets y(t)=x0−a0+(v−vc)t=(0,0,0) and y¨≡0, consistent with my¨=RTF+mτ=0.

2.3F1F2step 1.1

The chart is not inertial: since ω(t)=(2+t)e3 is not identically zero on I=R, R 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 t=0.

3.1step 1.1step 1.2step 2.1step 2.2step 2.3∎

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 (−4e1+4e1=0) 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 y˙ 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

Dependency tree · 2 levels

Sources