Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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.

Degree of the power map on the circle

Statement

Equip S1=R/Z with the smooth structure and orientation whose local quotient coordinates increase with the real coordinate. For every m∈Z, the smooth power map Pm:S1⟶S1,Pm([t])=[mt], equivalently z↦zm on the counterclockwise unit circle, has deg⁡(Pm)=m.

Facts & Assumptions

Given: An integer m and the oriented quotient-circle model in the statement.

[F1]

The circle as S1=R/Z with basepoint [0] gives [s]=[t] exactly when s−t∈Z.

[F3]

Regular-value formula for degree computes the degree of a proper smooth same-dimensional map at a supplied regular value as the finite sum of its derivative orientation signs, including an empty fibre.

Proof

technique · regular-value calculation
1.1F1F2given

The formula is well defined: if [s]=[t], then s−t∈Z by [F1], so m(s−t)∈Z and [ms]=[mt]. On every quotient arc shorter than one, source and target lift coordinates express Pm as u↦mu+k for an integer constant k; hence it is smooth with derivative m. For any compact K⊆S1, Hausdorffness makes K closed, continuity makes Pm−1(K) closed, and [F2] makes this closed subset of the compact circle compact. Thus Pm is proper.

2.1F1F3step 1.1

Suppose m>0. The fibre over [0] is exactly Pm−1([0])={[k/m]:0≤k<m}. Indeed, after taking the unique representative t∈[0,1), the condition mt∈Z says mt=k for exactly one of these integers. The derivative in positive lift coordinates is m>0, so every one of these m points has local sign +1. The value is regular, and [F3] gives deg⁡(Pm)=∑k=0m−11=m.

2.2F1F3step 1.1

Suppose m<0 and put r=−m>0. The same representative calculation gives the r distinct preimages [k/r], 0≤k<r, of [0]. In positive lift coordinates the derivative is m<0, so every local sign is −1. Hence [F3] gives deg⁡(Pm)=∑k=0r−1(−1)=−r=m.

3.1F3step 1.1step 2.1step 2.2∎

If m=0, P0 is the constant map with value [0]. The point [1/2] has empty fibre and is therefore a regular value; [F3] gives degree equal to the empty sum, namely zero. Thus all integers are covered. In particular P1 is the identity and P−1 reverses orientation. All fibres used are explicitly finite, no root is selected from a family, and no choice axiom is used.

Depends on

Used by

Dependency tree · two levels

28 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