CorollaryStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck 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.

Period-one to radian action-angle rescaling: $θ^{r a d} = 2 π θ$ and $I^{r a d} = I / (2 π)$ preserve $ω$

Statement

Let $(I, θ)$ be period-one action-angle coordinates with $ω = \sum_{i = 1}^{n} d θ_{i} \land d I_{i}$ as supplied by Action-angle coordinates on a saturated proper submersion neighbourhood of a compact connected regular fibre, with the two-form primitive supplied locally and Action and angle coordinates. Use the quotient lift charts and global angle differentials specified in Action-angle coordinates on a saturated proper submersion neighbourhood of a compact connected regular fibre, with the two-form primitive supplied locally. Put $T_{r a d} : = R / (2 π Z)$ , with quotient lift charts from intervals of length less than $2 π$ ; their transitions are translations by $2 π k$ , $k \in Z$ . The induced diffeomorphism $s : R / Z \to T_{r a d}$ is $s ([x]) = [2 π x]$ , with inverse $[y] \mapsto [y / (2 π)]$ . Thus the notation $2 π θ_{i}$ below means $s \circ θ_{i}$ , with values in $T_{r a d}$ , and its differential is defined by local real lifts. The action domain rescales from $A$ to $A / (2 π)$ . Define the rescaled coordinates

$θ_{i}^{r a d} : = 2 π θ_{i}, I_{i}^{r a d} : = \frac{I_{i}}{2 π} (i = 1, \dots, n) .$

Then $(θ^{r a d}, I^{r a d})$ are $C^{\infty}$ coordinates on the same chart,

$ω = \sum_{i = 1}^{n} d θ_{i}^{r a d} \land d I_{i}^{r a d},$

the angles $θ^{r a d}$ are $2 π$ -periodic (radian-valued), and if a Hamiltonian is $H = h (I)$ with $h$ of class $C^{2}$ in the period-one coordinates then in the radian coordinates it is $H = \tilde{h} (I^{r a d})$ with $\tilde{h} (I^{r a d}) = h (2 π I^{r a d})$ and ${\dot{θ}}_{i}^{r a d} = \partial \tilde{h} / \partial I_{i}^{r a d}$ .

Facts & Assumptions

Given: Period-one action-angle coordinates $(I, θ)$ on a chart $U$ , with $ω = \sum_{i} d θ_{i} \land d I_{i}$ , and the rescaled functions $θ^{r a d} = 2 π θ$ , $I^{r a d} = I / (2 π)$ .

[F1]

Coordinate calculus ( $C^{k}$ Euclidean maps and diffeomorphisms, Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ ): the rescaling is a linear invertible change of coordinates with constant differential $d θ_{i}^{r a d} = 2 π d θ_{i}$ and $d I_{i}^{r a d} = (2 π)^{- 1} d I_{i}$ .

[F2]

The period-one form (Action and angle coordinates, Action-angle coordinates on a saturated proper submersion neighbourhood of a compact connected regular fibre, with the two-form primitive supplied locally, A phase domain, its canonical one-form and its standard symplectic two-form): on the chart, $ω = \sum_{i} d θ_{i} \land d I_{i}$ and this is the standard two-form in the coordinates $(θ, I)$ .

[F3]

Hamilton's equations in canonical coordinates (The Hamiltonian field of a $C^{2}$ function on a phase domain is $J \nabla H$ , and the Poisson bracket is $\sum_{i} (\partial_{q^{i}} f \partial_{p_{i}} g - \partial_{p_{i}} f \partial_{q^{i}} g)$ ): on a phase domain with coordinates $(q, p)$ and standard two-form $\sum_{i} d q^{i} \land d p_{i}$ , a $C^{2}$ function $K$ has Hamiltonian field $X_{K} = J \nabla K$ , so its integral curves satisfy ${\dot{q}}^{i} = K_{p_{i}}$ and ${\dot{p}}_{i} = - K_{q^{i}}$ .

Proof

technique · direct; substitute the constant rescalings into the coordinate expression of $\omega$

1.1F1F2algebra

By [F1], $d θ_{i}^{r a d} \land d I_{i}^{r a d} = (2 π d θ_{i}) \land ((2 π)^{- 1} d I_{i}) = d θ_{i} \land d I_{i}$ for each $i$ ; summing over $i$ and using [F2] gives $ω = \sum_{i} d θ_{i}^{r a d} \land d I_{i}^{r a d}$ . The angle map is well-defined because changing a lift by an integer changes its scaled lift by an element of $2 π Z$ , and its inverse is the stated quotient map. On each lift chart its differential is the constant scalar $2 π$ . Since this angle diffeomorphism and the action rescaling are bijective and smooth with smooth inverses, $(θ^{r a d}, I^{r a d})$ are coordinates on the same chart.

2.1F1F3step 1.1algebra∎

The relation $H = h (I)$ becomes $H = h (2 π I^{r a d}) = \tilde{h} (I^{r a d})$ ; in the radian chart the two-form is $\sum_{i} d θ_{i}^{r a d} \land d I_{i}^{r a d}$ by step 1.1, so [F3] applies there with $(q, p) = (θ^{r a d}, I^{r a d})$ : ${\dot{I}}_{i}^{r a d} = 0$ and ${\dot{θ}}_{i}^{r a d} = \partial \tilde{h} / \partial I_{i}^{r a d}$ . The chain rule gives $\partial \tilde{h} / \partial I_{i}^{r a d} = 2 π (\partial_{i} h) (2 π I^{r a d}) = 2 π {\dot{θ}}_{i}$ , consistent with $θ_{i}^{r a d} = 2 π θ_{i}$ .

Remarks

The rescaling is the standard conversion between the period-one convention of Action and angle coordinates and the radian convention used, for instance, in the adiabatic-invariant estimates of the approximation layer; the symplectic form, and with it the canonical structure, is unchanged.

Period-one to radian action-angle rescaling: $θ^{r a d} = 2 π θ$ and $I^{r a d} = I / (2 π)$ preserve $ω$

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Period-one to radian action-angle rescaling: θrad=2πθθrad=2πθ and Irad=I/(2π)Irad=I/(2π) preserve ωω

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources

Period-one to radian action-angle rescaling: $θ^{r a d} = 2 π θ$ and $I^{r a d} = I / (2 π)$ preserve $ω$