ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The Pontryagin dual of the circle is $Z$

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Every continuous group homomorphism $χ : T \to T$ is $χ (z) = z^{n}$ for a unique $n \in Z$ ; consequently $n \mapsto (z \mapsto z^{n})$ is an isomorphism of topological groups $Z \to \hat{T}$ (equivalently, the dual of the published circle $R / Z$ is $Z$ ).

Facts & Assumptions

[F1]

$ε : R / Z \to T$ , $ε ([t]) = \exp (2 π i t)$ , is an isomorphism of topological groups, so it is continuous, surjective, and satisfies $ε ([0]) = 1$ ; the quotient homomorphism $p : R \to R / Z$ , $p (t) = [t]$ , is continuous and $ε (p (t)) = \exp (2 π i t)$ . (The multiplicative unit circle is a compact metrizable topological abelian group, The one-dimensional torus and its normalized Haar integral)

[F2]

Every continuous homomorphism $φ : R \to T$ is $φ (t) = \exp (2 π i ξ t)$ for a unique $ξ \in R$ . (Continuous characters of the real line are exponentials)

[F3]

$\exp (2 π i u) - 1 = (\cos 2 π u - 1) + i \sin 2 π u$ , so $∣ \exp (2 π i u) - 1 ∣^{2} = 2 - 2 \cos 2 π u = 4 \sin^{2} (π u)$ for real $u$ by the double-angle identity; and $\sin (π x) = 0$ exactly when $x \in Z$ . ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , Double-angle and quadratic power-reduction identities, The zero sets of sine and cosine and the least positive common period 2 pi)

[F4]

The addition formula for the complex exponential gives $\exp (n z) = (\exp z)^{n}$ for $n \in Z$ by induction and inversion. Exponent laws in a group: $z^{m + n} = z^{m} z^{n}$ ; the map $z \mapsto z^{k}$ is a continuous endomorphism of the topological group $T$ ; composites of continuous maps are continuous. ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential, Exponent laws in a group: $g^{m + n} = g^{m} g^{n}$ and $(g^{m})^{n} = g^{m n}$ for all $m, n \in Z$ , and $(g h)^{n} = g^{n} h^{n}$ when $g$ and $h$ commute, The multiplicative unit circle is a compact metrizable topological abelian group, Continuity may be checked on any open cover, and on any finite closed cover; composites of continuous maps are continuous)

[F5]

The dual of a compact abelian topological group is discrete, and the dual of a topological group is a Hausdorff topological group; every point of $T$ is $ε ([t])$ for some real $t$ . (Compact groups have discrete duals and discrete groups have compact duals, The multiplicative unit circle is a compact metrizable topological abelian group, The discrete, indiscrete, cofinite, cocountable, particular-point and Sierpinski topologies)

Verification

Given: A continuous group homomorphism $χ : T \to T$ , and the quotient circle $R / Z$ with the map $ε ([t]) = \exp (2 π i t)$ .

1.1F1F2F4

The composite $φ : = χ \circ ε \circ p : R \to T$ is a continuous group homomorphism: $p$ and $ε$ are continuous homomorphisms by [F1], $χ$ is one by hypothesis, and the composite of homomorphisms is a homomorphism; by [F2] there is a unique $ξ \in R$ with $φ (t) = \exp (2 π i ξ t)$ for all real $t$ .

2.1step 1.1F1F3

The parameter $ξ$ is an integer: for every integer $k$ one has $ε ([k]) = \exp (2 π i k) = 1$ by [F1] and [F3] (since $∣ \exp (2 π i k) - 1 ∣^{2} = 4 \sin^{2} (π k) = 0$ ), so $φ (k) = χ (1) = 1$ ; with $φ (k) = \exp (2 π i ξ k)$ this gives $\sin (π ξ k) = 0$ for every integer $k$ , in particular for $k = 1$ , and so $ξ \in Z$ by [F3].

3.1step 1.1step 2.1F1F4

Consequently $χ (z) = z^{ξ}$ for every $z \in T$ : write $z = ε ([t]) = \exp (2 π i t)$ for some real $t$ , which is possible because $ε$ is surjective by [F1]; then $χ (z) = φ (t) = \exp (2 π i ξ t) = (\exp (2 π i t))^{ξ} = z^{ξ}$ by step 1.1, step 2.1 and the power laws of [F4].

4.1step 3.1F1F3F4

Distinct integers give distinct characters: if $z^{n} = z^{m}$ for all $z \in T$ with $n \neq m$ , then evaluating at $z = ε ([t])$ gives $\exp (2 π i (n - m) t) = 1$ for all real $t$ , which fails for $t = 1 / (2 ∣ n - m ∣)$ by [F3], since then $\sin (π / 2) \neq 0$ ; hence $n = m$ . Each $z \mapsto z^{n}$ is a continuous endomorphism of $T$ by [F4].

5.1step 2.1step 3.1step 4.1F4

The map $n \mapsto (z \mapsto z^{n})$ is a bijective homomorphism from the discrete group $Z$ onto the dual: it is a homomorphism by the power laws $z^{n + m} = z^{n} z^{m}$ of [F4], injective by step 4.1, and surjective by steps 1.1, 2.1 and 3.1.

6.1step 5.1F1F5∎

It is a homeomorphism: $Z$ is discrete by [F5] and the dual of the compact group $T$ is discrete by [F5], so a bijection between discrete spaces is a homeomorphism; hence $Z ≅ \hat{T}$ as topological groups, and composing with the isomorphism $T ≅ R / Z$ gives the dual of the published circle.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

144 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

Dikran D. Dikranjan, Introduction to Topological Groups (author lecture notes, Universita di Udine / Universidad Complutense de Madrid, 2007) (standard reference, not scraped)
Manfred Einsiedler and Thomas Ward, Ergodic Theory with a View Towards Number Theory, Appendix C (course-hosted full text) (standard reference, not scraped)
Lynn H. Loomis, Introduction to Abstract Harmonic Analysis, D. Van Nostrand 1953, Chapter VII, Sections 34-35 (printed pp. 134-140) (standard reference, not scraped)

The Pontryagin dual of the circle is ZZ