LemmaStatement: Literature-sourcedProof: Literature-sourcedPipeline-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 unit-circle arc ${z : ∣ z - 1 ∣ < 1}$ contains no nontrivial subgroup

Statement

Let $T$ be the multiplicative unit circle (The multiplicative unit circle is a compact metrizable topological abelian group) and $D : = {z \in T : ∣ z - 1 ∣ < 1}$ . Every subgroup $H \leq T$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups) with $H \subseteq D$ is trivial; equivalently, for every $z \in T$ with $z \neq 1$ there is a positive integer $n$ with $z^{n} \notin D$ .

Facts & Assumptions

[F1]

$ε : R / Z \to T$ , $ε ([t]) = \exp (2 π i t)$ , is an isomorphism of topological groups; in particular it is injective and surjective, and $∣ z^{- 1} - w^{- 1} ∣ = ∣ z - w ∣$ for all $z, w \in T$ . (The multiplicative unit circle is a compact metrizable topological abelian group)

[F2]

$\exp (x + i y) = e^{x} (\cos y + i \sin y)$ for real $x, y$ , and $\exp (0) = 1$ from the defining series of the complex exponential. Also $\cos (2 u) = 1 - 2 \sin^{2} u$ for every real $u$ . ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The complex exponential by its power series, Double-angle and quadratic power-reduction identities)

[F3]

$\sin$ and $\cos$ are differentiable on $R$ , with $\sin 0 = 0$ and $\cos 0 = 1$ . (The derivatives of sine and cosine are cosine and minus sine)

[F4]

Sine is strictly increasing on $[- π / 2, π / 2]$ . (Signs, monotonicity intervals, and ranges of sine and cosine)

[F5]

For every real $x$ , $\sin (- x) = - \sin x$ , $\cos (- x) = \cos x$ , and $\cos (x + π / 2) = - \sin x$ . (Pythagorean and parity identities for all six trigonometric functions on their natural domains, Quarter-turn values and shifts by pi/2 and pi)

[F6]

For every real $x$ there is a unique integer $⌊ x ⌋$ with $⌊ x ⌋ \leq x < ⌊ x ⌋ + 1$ . (Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ )

[F7]

Every class in $R / Z$ has exactly one representative in $[0, 1)$ , and $R / Z$ is the quotient group of the additive group $R$ by its subgroup $Z$ , so that $[s] + [t] = [s + t]$ and in particular $[1 - t_{0}] = [- t_{0}]$ . (The one-dimensional torus and its normalized Haar integral, The quotient group $G / N$ and coset product $(g N) (h N) = g h N$ )

Proof

Given: The multiplicative unit circle $T$ , the arc $D = {z \in T : ∣ z - 1 ∣ < 1}$ , and a subgroup $H \leq T$ .

1.1F2F3F4F5

For real $u$ , $\exp (2 π i u) - 1 = (\cos 2 π u - 1) + i \sin 2 π u$ by [F2], so $∣ \exp (2 π i u) - 1 ∣^{2} = (\cos 2 π u - 1)^{2} + \sin^{2} 2 π u = 2 - 2 \cos 2 π u = 4 \sin^{2} (π u)$ ; hence $∣ \exp (2 π i u) - 1 ∣ = 2 ∣ \sin (π u) ∣$ . In particular $\sin (π / 6) = 1 / 2$ : writing $s : = \sin (π / 6)$ , we have $s > 0$ because $0 < π / 6 < π / 2$ and sine is strictly increasing on $[- π / 2, π / 2]$ with $\sin 0 = 0$ by [F4] and [F3]; the double-angle identity of [F2] gives $\cos (π / 3) = 1 - 2 s^{2}$ , while $\cos (π / 3) = \cos (π / 2 - π / 6) = - \sin (- π / 6) = \sin (π / 6) = s$ by [F5]; thus $2 s^{2} + s - 1 = 0$ , that is $(2 s - 1) (s + 1) = 0$ , and $s > 0$ forces $s = 1 / 2$ .

1.2F1F2F7

Let $z \in T$ , $z \neq 1$ , with $∣ z - 1 ∣ < 1$ . By [F1] and [F7] write $z = ε ([t_{0}]) = \exp (2 π i t_{0})$ with $t_{0} \in [0, 1)$ , and put $u : = z$ and $t : = t_{0}$ if $t_{0} \leq 1 / 2$ , while if $t_{0} > 1 / 2$ put $u : = z^{- 1}$ and $t : = 1 - t_{0} \in (0, 1 / 2)$ ; in the second case $u = ε ([- t_{0}]) = ε ([1 - t_{0}]) = \exp (2 π i t)$ because $[1 - t_{0}] = [- t_{0}]$ in $R / Z$ by [F1] and [F7]. Then $0 < t \leq 1 / 2$ , $u \neq 1$ (as $t \neq 0$ , $ε$ being injective with $ε ([0]) = \exp (0) = 1$ by [F1] and [F2]), and $∣ u - 1 ∣ = ∣ z - 1 ∣ < 1$ by [F1]; moreover $∣ u^{n} - 1 ∣ = ∣ z^{n} - 1 ∣$ for every $n \geq 1$ , again by [F1].

2.1step 1.1step 1.2F4

In the situation of step 1.2 we have $∣ u - 1 ∣ = 2 ∣ \sin (π t) ∣$ by step 1.1, so $∣ \sin (π t) ∣ < 1 / 2 = \sin (π / 6)$ by step 1.1 and the hypothesis; since $0 < π t \leq π / 2$ and sine is strictly increasing on $[0, π / 2]$ by [F4], this gives $π t < π / 6$ , that is $0 < t < 1 / 6$ .

3.1step 1.1step 1.2step 2.1F4F6

Put $n : = ⌊ 1 / (6 t) ⌋ + 1 \geq 1$ for the $t$ of step 2.1 by [F6]. Then $n > 1 / (6 t)$ , so $n t > 1 / 6$ , and $n \leq 1 / (6 t) + 1$ , so $n t \leq 1 / 6 + t < 1 / 3 < 1 / 2$ ; hence $π / 6 < π n t < π / 2$ and strict monotonicity of sine on $[0, π / 2]$ by [F4] gives $\sin (π n t) > \sin (π / 6) = 1 / 2$ . Therefore $∣ u^{n} - 1 ∣ = 2 \sin (π n t) > 1$ by step 1.1, so $u^{n} \notin D$ ; by step 1.2 also $z^{n} \notin D$ when $u = z^{- 1}$ , and plainly $z^{n} \notin D$ when $u = z$ .

4.1step 3.1F1∎

Every $z \in T$ with $z \neq 1$ therefore has a positive power outside $D$ : if $∣ z - 1 ∣ < 1$ this is step 3.1, and if $∣ z - 1 ∣ \geq 1$ then $z \notin D$ already. Conversely let $H \leq T$ with $H \subseteq D$ and suppose $h \in H$ , $h \neq 1$ ; then $h^{n} \notin D$ for some $n \geq 1$ , while $h^{n} \in H \subseteq D$ , a contradiction, so $H = {1}$ and every subgroup contained in $D$ is trivial.

Depends on

Used by

Dependency tree · two levels

115 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)
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 unit-circle arc {z:∣z−1∣<1}{z:∣z−1∣<1} contains no nontrivial subgroup