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.

The Euler-angle pole: a degenerate parametrization of SO(3) while the physical orientation remains regular

Physical scope

A worked example about the Euler-angle description of the orientation of the rigid-material model branch of Adoption of the rigid-material model branch: reference mass distribution, rigid placements, orientation and scope: at the pole β=0 the parametrization is non-injective and its derivative has rank at most two, so it is not a chart there, and the map from Euler-angle rates to the body angular velocity loses injectivity; meanwhile the orientation path R(t)=Ry(κt) passes through the pole orientation with constant angular velocity κe2 for a positive rate κ in radians per second, and is perfectly regular. The item asserts no dynamics, no measurement and no claim that the orientation of a concrete body has been recorded.

Example

Let Rz,Ry be the coordinate rotation matrices of The coordinate rotation matrices Rz(a) and Ry(a): values in SO(3), composition law, and derivatives and consider the formula of the Euler-angle parametrization of The Euler-angle parametrization and the heavy symmetric top system, Φ:R3⟶M3(R),Φ(α,β,γ):=Rz(α)Ry(β)Rz(γ), here read on the whole parameter space R3 (the definition restricts its parameter domain to β∈(0,π) and asserts no chart property). Angles are dimensionless radians; time t is read in seconds. Fix a positive rate κ>0 of dimension τ−1, read in radians per second (Dimensions and SI unit conventions of the non-relativistic classical mechanics framework). Angle-curve rates have the same dimension. Then:

  1. Φ(α,0,γ)=Rz(α+γ): at the pole β=0 the value depends only on the sum α+γ, and for every real s Φ(α+s,0,γ−s)=Φ(α,0,γ); hence Φ is not injective on any neighbourhood of a pole point.
  2. the partial derivatives at a pole point satisfy ∂αΦ(α,0,γ)=∂γΦ(α,0,γ)=[e3]×Rz(α+γ), so the Jacobian matrix has two identical columns, its rank is at most 2, and DΦ:R3→M3(R) is not injective; consequently Φ has no differentiable local inverse at any pole point;
  3. along a smooth curve t↦(α(t),β(t),γ(t)) through a pole point (β(0)=0) the body angular velocity of the resulting rotation path is ω(0)=(α′(0)+γ′(0)) e3+β′(0) Rz(−γ(0))e2, so the individual rates α′ and γ′ enter only through their sum: the triples of rates (α′,β′,γ′) and (α′+h,β′,γ′−h) produce the same angular velocity, and the rate map of the parametrization is not injective at the pole, where h is any rate of dimension τ−1;
  4. nevertheless the orientation path R:R⟶SO(3),R(t):=Ry(κt), with c(t)=0 and time window I0=R, of a rigid-material model passes through the pole orientation R(0)=I3=Φ(0,0,0), is of class C∞, and has the constant body angular velocity κe2; the singularity of clause 2 is a property of the parametrization, not of the orientation or of the angular velocity.

Facts & Assumptions

Given: The map Φ, the coordinate rotation matrices of The coordinate rotation matrices Rz(a) and Ry(a): values in SO(3), composition law, and derivatives, a pole point (α,0,γ)∈R3, a real s, the positive rate κ with units specified above, and a C2 curve (α,β,γ) on an open time interval with 0 an interior point and β(0)=0 (Intervals of R: the nine order-convex forms, nondegeneracy, and length, The derivative f′(c)=lim⁡x→cf(x)−f(c)x−c of f:A→R at a point c∈A that is a limit point of A, and differentiability on a set).

[L1]

Coordinate rotations (The coordinate rotation matrices Rz(a) and Ry(a): values in SO(3), composition law, and derivatives): Rz(a),Ry(a)∈SO(3) for every real a, Rz(0)=Ry(0)=I3, Rz(a)Rz(b)=Rz(a+b), and for a differentiable a the curves Rz∘a, Ry∘a are differentiable with (Rz∘a)′=a′Rz(a)[e3]×=a′[e3]×Rz(a) and (Ry∘a)′=a′Ry(a)[e2]×=a′[e2]×Ry(a).

[L2]

Skew-matrix correspondence and conjugation (The skew-matrix/cross-product correspondence [ω]×z=ω×z and its conjugation law R[ω]×RT=[Rω]× clauses 1-3, The orthogonal group O(3) and the rotation group SO(3)): [ω]×z=ω×z; the map ω↦[ω]× is injective; for R∈SO(3) one has R[ω]×RT=[Rω]×; SO(3) is a group (SO(3) is a subgroup of the general linear group, with R−1=RT).

[L4]

The model's kinematic notions (Configuration, configuration space and orientation of a rigid-material model in an inertial frame, Body and spatial angular velocity of a rigid-material motion, and the material velocity field): a configuration path (c,R) with R of class C2 assigns to each time a placement; the body angular velocity is the unique ω with RTR′=[ω]×.

Verification

technique · direct; use the composition law of the coordinate rotations, differentiate the parametrization with the product rule, and read the angular velocity through the skew-matrix correspondence
1.1givenL1algebra

Pole values: by the composition law and Ry(0)=I3 of [L1], Φ(α,0,γ)=Rz(α)Rz(γ)=Rz(α+γ), so the value depends only on α+γ. For every real s, Φ(α+s,0,γ−s)=Rz(α+s+γ−s)=Rz(α+γ)=Φ(α,0,γ), and the points (α+s,0,γ−s) approach (α,0,γ) as s→0 while remaining distinct for s≠0. Hence Φ is not injective on any neighbourhood of the pole point; this is clause 1.

1.2givenL1L3algebra

Partial derivatives at the pole: differentiating with respect to α with β,γ fixed and using the product rule and [L1], ∂αΦ(α,β,γ)=[e3]×Rz(α)Ry(β)Rz(γ), and at β=0 this is [e3]×Rz(α+γ) by clause 1. Differentiating with respect to γ gives ∂γΦ(α,β,γ)=Rz(α)Ry(β)Rz(γ)[e3]×; at β=0 the middle factor is I3 and the factors Rz(γ) and [e3]× commute by the identity Rz(a)[e3]×=[e3]×Rz(a) of [L1], so ∂γΦ(α,0,γ)=Rz(α)[e3]×Rz(γ)=[e3]×Rz(α)Rz(γ)=[e3]×Rz(α+γ), the same value as ∂αΦ.

2.1step 1.1step 1.2L3algebra

Rank and absence of a local inverse: the Jacobian matrix JΦ(α,0,γ) has columns ∂αΦ, ∂βΦ, ∂γΦ [L3], and the first and third columns coincide by step 1.2. Thus the linear map DΦ:R3→M3(R)≅R9 annihilates the nonzero vector (1,0,−1) and has rank at most 2, so it is not injective. Moreover, step 1.1 gives distinct points with equal images in every neighbourhood of the pole point, ruling out any local inverse, including a differentiable inverse onto a neighbourhood in SO(3). This proves clause 2.

2.2step 1.2L1L2L4algebra

Angular velocity along a curve through the pole: let Φt:=Φ(α(t),β(t),γ(t)); by the product rule and [L1] at t=0, where β(0)=0 and Ry(0)=I3, Φ0′=(α′(0)+γ′(0))[e3]×Rz(α(0)+γ(0))+β′(0) Rz(α(0))[e2]×Rz(γ(0)), using the two computations of step 1.2 for the α- and γ-directions and the middle derivative ∂βΦ=Rz(α)[e2]×Rz(γ) at the pole. Multiplying on the left by Φ0T=Rz(−γ(0))Rz(−α(0))=Φ0−1 (the matrix is orthogonal [L1]) and using the conjugation law R[ω]×RT=[Rω]× of [L2] together with Rz(−γ(0))e2 for the second term gives Φ0TΦ0′=[(α′(0)+γ′(0)) e3+β′(0) Rz(−γ(0))e2]×, so by the injectivity clause of [L2] and the characterisation of the body angular velocity [L4], ω(0)=(α′(0)+γ′(0))e3+β′(0)Rz(−γ(0))e2. The rates α′ and γ′ enter only through the sum, so (α′+h,β′,γ′−h) and (α′,β′,γ′) give the same angular velocity: the rate map is not injective at the pole. This is clause 3.

3.1step 2.1L1L2L4algebra

The regular physical path: R(t)=Ry(κt) has R(0)=I3 and is the composition of the smooth coordinate-rotation curve with the smooth map t↦κt, hence of class C∞ [L1]; by the derivative clause of [L1], R′(t)=κRy(κt)[e2]×, so R(t)TR′(t)=[κe2]× for every t and the body angular velocity is the constant vector κe2 by [L2] and [L4]; in particular the orientation path passes through the pole orientation R(0)=I3=Φ(0,0,0) with a well-defined, constant angular velocity. The failure of clause 2 is thus a failure of the parameter triple to be a chart at the pole, not a singularity of the orientation path or of its angular velocity. This proves clause 4.

4.1step 1.1step 2.1step 2.2step 3.1∎

Summary: the parametrization Φ is smooth as a map, but at every pole point it is non-injective (clause 1), its derivative has rank at most 2 and it admits no differentiable local inverse (clause 2), and the angular velocity does not uniquely determine the Euler-angle rates at a fixed pole triple (clause 3), while a physical orientation path through the same pole orientation is regular with a perfectly well-defined angular velocity (clause 4).

Remarks

Depends on

Dependency tree · 2 levels

Sources