Alphabeta Math
PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-22
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.

Invariant Hamiltonians descend to reduced Hamiltonians

Statement

Assume ACω. Let (M,ω,G,μ) be a Hamiltonian G-space with a G-invariant Hamiltonian H∈C∞(M)G, let α be a regular value of μ, and suppose Gα acts freely and properly on the level μ−1(α), with reduction (Mα,ωα) and quotient map π. Then:

  1. XH is tangent to the level μ−1(α) and is Gα-invariant, so it pushes forward to a smooth vector field Y=dπ(XH∣μ−1(α)) on Mα;
  2. H∣μ−1(α) is Gα-invariant and descends to a unique smooth h∈C∞(Mα) with π∗h=ι∗H;
  3. Y=Xh; consequently every integral curve of XH that lies in the level projects under π to an integral curve of the flow of h on Mα.

Facts & Assumptions

Given: ACω, a Hamiltonian G-space with invariant Hamiltonian H, a regular value α, and a free proper Gα-action on the level.

[A1]

ACω is countable choice; it is used only through the reduction, fundamental-field and descent suppliers cited below.

[F1]

If H is G-invariant then {μξ,H}=0 for all ξ, and μ is constant along the flow of XH. Noether's conservation law for Hamiltonian actions.

[F2]

XH is the unique field with ιXHω=dH, and XG(F)={F,G} for the Poisson bracket. Hamiltonian vector fields exist uniquely for smooth functions, Poisson bracket on a symplectic manifold.

[F3]

Reduction gives the smooth quotient and π∗ωα=ι∗ω (Marsden--Weinstein--Meyer symplectic reduction). The free proper action quotient theorem makes π a smooth surjective submersion for this quotient structure (Free proper action quotient manifold).

[F5]

Integral curves of a smooth vector field through a given initial point are unique. Through each point there is a unique maximal integral curve.

[F6]

At a regular level, Tpμ−1(α)=ker⁡dμp (The tangent space of a regular level set is the kernel).

Proof

technique · direct
1.1F1F2F6

XH is tangent to the level: for every ξ, dμξ(XH)=XH(μξ)={μξ,H}=0 by [F1] and [F2], so XH lies in ker⁡dμ and hence in Tμ−1(α) by [F6].

1.2F1F2given

XH is invariant under the action: since H is G-invariant, for g∈G and p∈M, ωg⋅p(d(ag)pXH(p),d(ag)pv)=ωp(XH(p),v)=dHp(v)=dHg⋅p(d(ag)pv) for all v, so nondegeneracy gives d(ag)pXH(p)=XH(g⋅p).

2.1step 1.1step 1.2F3F4

By steps 1.1 and 1.2 the field XH is Gα-invariant and tangent to the level, so Y[p]:=dπp(XH(p)) is well defined: for p′=h⋅p with h∈Gα one has dπp′XH(p′)=dπp′d(ah)XH(p)=d(π∘ah)pXH(p)=dπpXH(p) because π∘ah=π. It is smooth: by [F4], submersion coordinates for π have the form (u,v)↦u; fixing v=v0 gives a smooth local section s. There Y=dπ∘XH∘s, interpreting XH as its tangent restriction to the level, so this local expression is smooth.

2.2step 1.2F3F4

By invariance, H∣μ−1(α) is constant on the fibres of π, so [F4] gives a unique continuous h:Mα→R with π∗h=ι∗H. Near every point of Mα, the submersion π has a smooth local section s by [F3] and [F4], by fixing the fibre coordinates as above, and there h=H∘ι∘s; hence h is smooth.

3.1step 2.1step 2.2F2F3

The projected field is the Hamiltonian field of h: for v∈Tpμ−1(α), dh[p](dπpv)=d(π∗h)p(v)=d(ι∗H)p(v)=dHp(v)=ωp(XH(p),v)=(π∗ωα)p(XH(p),v)=ωα(Y[p],dπpv), using [F3]; since dπp is onto, ιYωα=dh, and uniqueness of Hamiltonian fields [F2] gives Y=Xh.

4.1step 3.1F5A1∎

If γ is an integral curve of XH lying in the level, then π∘γ is an integral curve of Y=Xh by the chain rule, and by uniqueness of integral curves [F5] it agrees on its interval of definition with the reduced integral curve through the projected initial point. Thus the restricted flow projects wherever the original curve is defined; no completeness or equality of maximal time intervals is asserted. If the level is empty, there is a unique empty descended function and vector field and every assertion is vacuous.

Depends on

Used by

Dependency tree · two levels

47 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources