Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-14
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.

Irrational circle rotations are uniquely ergodic

Statement

Assume the Axiom of Countable Choice. If α is irrational, then the circle rotation Rα is uniquely ergodic, and its unique invariant Borel probability is Lebesgue measure λ.

Facts & Assumptions

Given: Countable choice and an irrational real α.

[F2]

Rα is an isometry preserving Lebesgue probability, and irrationality makes it ergodic (Circle rotations preserve Lebesgue measure, Circle rotation is ergodic for Lebesgue measure exactly at irrational angles).

[F3]

Birkhoff supplies an invariant a.e. limit; on an ergodic probability system it is constant a.e. (Birkhoff pointwise ergodic theorem, Equivalent invariant-set and invariant-function criteria for ergodicity).

[F4]

Dominated convergence and integral invariance identify limits of bounded averages (Dominated convergence, Integral invariance under measure-preserving maps).

[F5]

Unique ergodicity is equivalent, under countable choice, to uniform convergence of every continuous real ergodic average to a constant (Unique ergodicity is equivalent to uniform ergodic averages).

Proof

technique · direct Birkhoff–equicontinuity argument
1.1F2F3F4

Fix f∈C(T,R). Compactness makes f bounded, hence f∈L1(λ). By [F2]–[F3], Anf converges on a conull set Yf to a constant cf. Since ∣Anf∣≤∥f∥∞, dominated convergence and invariance give cf=∫cf dλ=lim⁡n∫Anf dλ=∫f dλ.

1.2F1F2

Given ε>0, uniform continuity of f gives δ>0 such that d(x,y)<δ implies ∣f(x)−f(y)∣<ε/3. Rotations are isometries, so the same δ gives ∣Anf(x)−Anf(y)∣<ε/3 for every n whenever d(x,y)<δ.

2.1F2F6step 1.1

The set Yf is dense. Indeed, every nonempty circle-open set contains a nondegenerate ordinary interval, possibly on one side of the cut, and such an interval has positive Lebesgue measure by the interval-measure formula. A conull set must meet it.

3.1F1step 2.1step 1.2

Compactness supplies a finite δ/3-net x1,…,xm. By density choose, using only finite choice, yi∈Yf with d(xi,yi)<δ/3. For all sufficiently large n, every ∣Anf(yi)−cf∣<ε/3. Given x, choose i with d(x,xi)<δ/3; then d(x,yi)<2δ/3, and step 1.2 gives ∣Anf(x)−cf∣<2ε/3. Thus Anf→cf uniformly.

4.1F2F5step 1.1step 3.1∎

The argument applies to every real continuous f, with cf=∫f dλ. By [F5], Rα is uniquely ergodic and its unique invariant probability is the already invariant λ. Countable choice is inherited from [F2] and [F5]; the finite net and finite choices in step 3.1 require no stronger principle. No Fourier series or Weyl criterion was used.

Depends on

Used by

Dependency tree · two levels

88 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