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.

A steady precession of the heavy symmetric top checked on explicit data: the pivot balance, the two conserved momenta and the reduced energy

Physical scope

A worked steady precession of the heavy symmetric top branch of Adoption of the heavy symmetric top branch: axisymmetric rigid material, a fixed pivot material point, a uniform gravitational field and the balance of angular momentum about the pivot on declared parameters Ac=2, Cc=1, m=1, d=1, g=1 (so the pivot transverse moment is A=3) and the explicit angles φ(t)=t, θ=π/3, ψ(t)=2t: the pivot balance is verified identically in time, the two conserved momenta are a=7/2 and b=5/2, the reduced energy is 19/4, and the heavy-top system holds, so the reduction conclusions apply. All formulas use numerical SI values with dimensionless dimensionless t = T / (one second) as defined in the Example; no measurement, no concrete top and no experiment is asserted.

Example

Numerical SI convention. Let T denote physical elapsed time and fix T∗=1 s, M∗=1 kg and D∗=1 m. All formulas below use numerical SI values: t:=T/T∗ is dimensionless, angles are in radians, positions and d are divided by D∗, masses by M∗, inertia entries by M∗D∗2, and g by D∗/T∗2. Primes denote differentiation with respect to t. Restore physical angular velocity as ωphys(T)=ω(T/T∗)/T∗, angular momentum as Jphys(T)=(M∗D∗2/T∗)J(T/T∗), energy as (M∗D∗2/T∗2)E, and torque as (M∗D∗2/T∗2)τ(T/T∗). Thus the displayed rates φ′=1 and ψ′=2 mean physical rates 1 s−1 and 2 s−1, and every trigonometric argument is dimensionless. The physical placement is xphys(T,ρphys)=D∗x(T/T∗,ρphys/D∗); its derivatives restore the pivot balance and heavy-top equations with the same SI data. These are unit conventions of Dimensions and SI unit conventions of the non-relativistic classical mechanics framework, not measured inputs.

Adopt the heavy symmetric top branch Adoption of the heavy symmetric top branch: axisymmetric rigid material, a fixed pivot material point, a uniform gravitational field and the balance of angular momentum about the pivot with declared parameters Ac=2,Cc=1,m=1,d=1,g=1 in the framework's units (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework), so that the body inertia matrix is I=diag(2,2,1) in the declared basis and the pivot transverse moment is A=Ac+md2=2+1=3,C=Cc=1. Let θ0:=π/3 and consider the angles φ(t)=t,θ(t)=θ0,ψ(t)=2t(t∈R), the orientation path R(t):=Θ(φ(t),θ(t),ψ(t)) of The Euler-angle parametrization and the heavy symmetric top system, the centre of mass c(t):=d R(t)e3, and the motion x(t,ρ):=c(t)+R(t)ρ. Verify:

  1. It is a motion of the branch satisfying the pivot balance. The pivot constraint c(t)+R(t)(−de3)=0 holds, and with ω(t)=(−32cos⁡(2t), 32sin⁡(2t), 52) and γ(t)=R(t)Te3, I~ ω′+ω×I~ ω=−mgd (e3×γ)(t∈R), where I~=diag(3,3,1); hence the motion satisfies the adopted balance of Adoption of the heavy symmetric top branch: axisymmetric rigid material, a fixed pivot material point, a uniform gravitational field and the balance of angular momentum about the pivot clause (v) and the conclusions of Reduction of the heavy symmetric top branch: pivotal angular momentum, Euler-angle equations, the two conserved momenta and the one-dimensional θ equation clauses 1-2 hold along it.
  2. The conserved momenta and the reduced energy. With φ′=1, θ′=0, ψ′=2, a=Aφ′sin⁡2θ0+bcos⁡θ0=72,b=C(ψ′+φ′cos⁡θ0)=52,E=U(θ0)=194.
  3. The heavy-top system holds, and θ is constant. The three equations of The Euler-angle parametrization and the heavy symmetric top system hold for the triple, and Aθ′′=−U′(θ0)=0, so the motion is a steady precession: φ′=1 and ψ′=2 are constant and the nutation angle is constantly π/3.

Facts & Assumptions

Given: The branch parameters Ac=2, Cc=1, m=1, d=1, g=1, the derived constants A=3, C=1, the angle data θ0=π/3, φ(t)=t, ψ(t)=2t, and the path R=Θ(φ,θ0,ψ) with c=dRe3.

[L1]

Branch kinematics and dynamics: the motions of the branch satisfy the pivot constraint c=dRe3 and the balance Jp′=τp with Jp=RI~ω, τp=−mgd(Re3)×e3, so the reduction conclusions of Reduction of the heavy symmetric top branch: pivotal angular momentum, Euler-angle equations, the two conserved momenta and the one-dimensional θ equation clauses 1-4 hold on any interval carrying an Euler-angle description (Adoption of the heavy symmetric top branch: axisymmetric rigid material, a fixed pivot material point, a uniform gravitational field and the balance of angular momentum about the pivot clauses (ii)-(v), Reduction of the heavy symmetric top branch: pivotal angular momentum, Euler-angle equations, the two conserved momenta and the one-dimensional θ equation clauses 1-4).

[L2]

Euler-angle kinematics: for R=Θ(φ,θ,ψ) one has ω=(−φ′sin⁡θcos⁡ψ+θ′sin⁡ψ, φ′sin⁡θsin⁡ψ+θ′cos⁡ψ, ψ′+φ′cos⁡θ) and γ=RTe3=(−sin⁡θcos⁡ψ, sin⁡θsin⁡ψ, cos⁡θ) (Angular velocity in Euler angles: ω3=ψ′+φ′cos⁡θ and ω12+ω22=θ′2+φ′2sin⁡2θ, Reduction of the heavy symmetric top branch: pivotal angular momentum, Euler-angle equations, the two conserved momenta and the one-dimensional θ equation clause 2, The coordinate rotation matrices Rz(a) and Ry(a): values in SO(3), composition law, and derivatives).

[L3]

The heavy-top system and its reduction: the three displayed equations of The Euler-angle parametrization and the heavy symmetric top system, and the conclusions Aθ′′=−U′(θ), φ′=(a−bcos⁡θ)/(Asin⁡2θ), ψ′=b/C−(a−bcos⁡θ)cos⁡θ/(Asin⁡2θ) of Reduction of the heavy symmetric top system: conserved momenta, one-dimensional θ equation and conserved reduced energy clauses 2-4.

[L5]

The constant π=2γ, where γ is the smallest positive zero of cosine; cos⁡π=−1, cos⁡0=1, cos⁡(π/2)=0, sin⁡0=0; cosine is strictly decreasing on [0,π] and sine strictly increasing on [0,π/2]; sine and cosine obey their addition formulas; and every nonnegative real has a unique nonnegative square root (Pi as twice the smallest positive zero of cosine, Cosine has a smallest positive zero, lying strictly between zero and two, Quarter-turn values and shifts by pi/2 and pi, Signs, monotonicity intervals, and ranges of sine and cosine, The addition formulas for sine and cosine, Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}).

Verification

technique · direct; compute the body angular velocity, the vertical direction in body coordinates and the two sides of the pivot balance on the declared data, then read off the conserved momenta and the reduced energy
1.1L4L5algebra

Put θ=π/3, c=cos⁡θ and s=sin⁡θ. Since 0<θ<π/2, [L5] gives 0<c<1 and s>0. The addition formulas [L5] and Pythagorean identity [L4] give cos⁡π=cos⁡(3θ)=4c3−3c; as cos⁡π=−1, (c+1)(2c−1)2=0. Because c>0, c=1/2. Then s2=1−c2=3/4 and s>0, so the uniqueness of the nonnegative square root [L5] gives s=3/2.

2.1givenstep 1.1L2L4algebra

By [L2] with φ′=1, θ′=0, ψ′=2, θ0=π/3 and ψ(t)=2t: ω(t)=(−sin⁡θ0cos⁡(2t), sin⁡θ0sin⁡(2t), 2+cos⁡θ0)=(−32cos⁡(2t), 32sin⁡(2t), 52) and γ(t)=(−32cos⁡(2t), 32sin⁡(2t), 12) by step 1.1 and [L2].

2.2step 1.1givenL1L4algebra

With φ′=1, θ′=0, ψ′=2, sin⁡2θ0=34 and cos⁡θ0=12 by [L4]: b=C(ψ′+φ′cos⁡θ0)=1⋅(2+12)=52 and a=Aφ′sin⁡2θ0+bcos⁡θ0=3⋅34+52⋅12=94+54=72.

3.1step 2.1givenL1L4algebra

Compute both sides of the balance with I~=diag(3,3,1): by [L4], ω′=(3sin⁡(2t), 3cos⁡(2t), 0), so I~ω′=(33sin⁡(2t), 33cos⁡(2t), 0), and with I~ω=(−332cos⁡(2t), 332sin⁡(2t), 52), the coordinate formula for the cross product gives (ω×I~ω)1=534sin⁡(2t)−1534sin⁡(2t)=−532sin⁡(2t), (ω×I~ω)2=−1534cos⁡(2t)+534cos⁡(2t)=−532cos⁡(2t) and (ω×I~ω)3=0. Hence the left side is (32sin⁡(2t), 32cos⁡(2t), 0). On the right, e3×γ=(−γ2,γ1,0)=(−32sin⁡(2t), −32cos⁡(2t), 0) and mgd=1, so the right side is the same vector; the balance holds for every t.

3.2step 2.2givenL3L4algebra

The reduced energy: E=12Aθ′2+(a−bcos⁡θ0)22Asin⁡2θ0+b22C+mgdcos⁡θ0=(9/4)22⋅3⋅(3/4)+25/42+12=98+258+48=388=194, where a−bcos⁡θ0=72−54=94 by step 2.2.

4.1step 2.1step 3.1givenL1

The constraint c(t)+R(t)(−de3)=dR(t)e3−dR(t)e3=0 holds by the definition of c; hence with step 3.1 the data constitute a motion of the branch satisfying the adopted pivot balance, and clauses 1-2 of Reduction of the heavy symmetric top branch: pivotal angular momentum, Euler-angle equations, the two conserved momenta and the one-dimensional θ equation apply.

5.1step 4.1step 2.2step 3.2givenL3L4algebra∎

The three equations of the heavy-top system of [L3] hold for the triple: the first and third are the statements that a and b of step 2.2 are constant, and the second is 0=Aφ′2sin⁡θ0cos⁡θ0−C(ψ′+φ′cos⁡θ0)φ′sin⁡θ0+mgdsin⁡θ0=3⋅34−534+234 with φ′=1, which vanishes by [L4]. Hence (φ,θ,ψ) is a heavy-top trajectory with parameters (A,C,m,d,g)=(3,1,1,1,1), and Aθ′′=−U′(θ0)=0; the conservation of a and b and the formulas φ′=(a−bcos⁡θ0)/(Asin⁡2θ0)=9/49/4=1 and ψ′=b/C−(a−bcos⁡θ0)cos⁡θ0/(Asin⁡2θ0)=52−9/4⋅1/29/4=52−12=2 of [L3] are consistent with the data, so the motion is a steady precession with constant nutation angle π/3.

Remarks

Depends on

Dependency tree · 2 levels

Sources