Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 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.

Circle rotation on complex n-space and its quadratic moment map

Example

Identify Cn with R2n by zj=xj+iyj and equip it with the standard symplectic form ω0=∑j=1ndxj∧dyj; let the circle act by scalar multiplication, eiθ⋅z=eiθz. This action is Hamiltonian, and with the library's fundamental-field convention ξM=ddt∣0exp⁡(−tξ)⋅p the moment map is the negative quadratic function

μ(z)=−12∣z∣2+c,c∈R,

where the displayed real number denotes the corresponding covector under the standard identification (s1)∗≅R. The constant is a normalization. The positive quadratic +12∣z∣2 belongs to the opposite generator convention.

Facts & Assumptions

Given: ACω, Cn=R2n with ω0=∑jdxj∧dyj, and the scalar circle action. Identify the Lie algebra s1=T1S1 with R by ι(ξ)=ddt∣0eitξ and its dual with R by c↦(ι(ξ)↦cξ).

[A1]

ACω is countable choice; it is used only through the fundamental-field interface.

[F1]

For ι(ξ)∈s1 the fundamental field is ι(ξ)M(z)=ddt∣0e−itξz (Fundamental vector fields for a left action).

[F2]

ω0=∑jdxj∧dyj is symplectic and ι∂xjω0=dyj, ι∂yjω0=−dxj. The canonical cotangent two-form is symplectic.

[F3]

The component equation of the library convention is dμξ=−ιξMω0; the coadjoint action of the abelian group S1 is trivial, so equivariance means invariance. Moment map, component Hamiltonians and infinitesimal moment maps, The coadjoint representation, action and orbits.

Verification

technique · direct
1.1F1given

For ξ∈R and zj=xj+iyj, the curve t↦e−itξz has velocity ι(ξ)M=ξ∑j(yj∂xj−xj∂yj) at t=0.

2.1step 1.1F2

Contracting with ω0 using [F2] gives ιι(ξ)Mω0=ξ∑j(yj dyj+xj dxj)=d(ξ2∣z∣2).

3.1step 2.1F3given

Under the dual identification in the Given block, the component of μ(z)=−12∣z∣2+c at ι(ξ) is μι(ξ)(z)=ξ(−12∣z∣2+c). Hence step 2.1 gives dμι(ξ)=−ιι(ξ)Mω0 for every ξ, so the displayed scalar formula defines a genuine (s1)∗-valued moment map.

4.1step 3.1F3A1∎

The map μ is invariant: ∣eiθz∣=∣z∣. Since the coadjoint action of S1 is trivial, invariance is equivariance, so μ is an equivariant moment map. The opposite quadratic +12∣z∣2 has differential +ιξMω0 and therefore does not satisfy the library equation.

Depends on

Used by

Dependency tree · two levels

24 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