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.

✓ 6 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 6 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Logarithm and General Powers: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

Two to the square root of two from rational suprema and from exp(sqrt(2) log 2)

Example

Let $s = \sqrt{2}$ . The two constructions give the same number: $2^{[s]} = \sup {2^{q} : q \in Q, q < s} = \exp (s \log 2) = \lim_{q_{n} \to s, q_{n} \in Q} 2^{q_{n}} .$

Facts & Assumptions

Given: The nonnegative square root $s = \sqrt{2}$ .

[L1]

The rational-supremum and exponential constructions agree (The rational-supremum construction of real powers agrees with the exponential construction).

[L2]

Rational approximations to an exponent converge to its real power (Every rational approximation to a real exponent gives the same limiting real power).

[L3]

$\sqrt{2}$ exists and is positive (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Verification

technique · direct

1.1

By [L3], $s$ is a real exponent, so [L1] gives $2^{[s]} = \exp (s \log 2)$ .

L1L3

1.2

For every rational sequence $q_{n} \to s$ , [L2] gives $2^{q_{n}} \to 2^{s} = \exp (s \log 2)$ .

2.1

Thus the supremum, exponential, and rational-limit descriptions agree.

step 1.1step 1.2∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The alternating harmonic series sums to log 2

Example

$\sum_{n = 1}^{\infty} \frac{(- 1)^{n + 1}}{n} = \log 2.$

Facts & Assumptions

Given: The endpoint formula for $\log (1 + x)$ .

[L1]

At $x = 1$ , $\log (1 + x) = \sum_{n \geq 1} (- 1)^{n + 1} x^{n} / n$ converges to $\log 2$ ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)).

Verification

technique · direct

1.1

Substituting $x = 1$ into [L1] gives exactly the displayed alternating harmonic series.

2.1

Therefore the alternating harmonic series has sum $l o g 2$ .

step 1.1∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

Concrete logarithmic, polynomial, and exponential growth comparisons

Example

As $x \to + \infty$ , $\frac{\log x}{\sqrt{x}} \to 0, \frac{x^{5}}{\exp x} \to 0, \frac{x^{2}}{\exp (3 x)} \to 0.$

Facts & Assumptions

Given: Positive real $x$ tending to $+ \infty$ .

[L1]

$\log x / x^{α} \to 0$ for every $α > 0$ (The logarithm grows more slowly than every positive real power).

[L2]

$x^{m} / \exp (a x) \to 0$ for every natural $m$ and $a > 0$ (The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

Verification

technique · direct

1.1

Apply [L1] with $α = 1 / 2$ .

1.2

Apply [L2] with $(m, a) = (5, 1)$ and $(m, a) = (2, 3)$ .

2.1

These are the three displayed limits.

step 1.1step 1.2∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

x^x tends to one as x tends to zero from the right

Example

$\lim_{x \to 0 +} x^{x} = 1.$

Facts & Assumptions

Given: $x > 0$ tending to $0$ .

[L1]

$x^{x} = \exp (x \log x)$ for $x > 0$ (Real powers for positive bases, with the zero-base positive-exponent convention).

[L2]

$\log t / t \to 0$ as $t \to + \infty$ (The logarithm grows more slowly than every positive real power).

[L3]

The exponential is continuous and $\exp 0 = 1$ (The exponential function is strictly increasing).

Verification

technique · direct

1.1

With $t = 1 / x$ , one has $t \to + \infty$ and $x \log x = - (\log t) / t \to 0$ by [L2].

2.1

Therefore $x^{x} = \exp (x \log x) \to \exp 0 = 1$ .

step 1.1L1L3∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The log(1+x) power series diverges at x=-1

Statement refuted

The power series for $\log (1 + x)$ converges at $x = - 1$ .

Facts & Assumptions

Given: The endpoint $x = - 1$ .

[L1]

The formula for $\log (1 + x)$ is stated only on $(- 1, 1]$ ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)).

[L2]

The series $\sum_{n \geq 1} 1 / n$ diverges (The p-series for a real exponent p converges exactly when p is greater than one).

Counterexample

technique · direct

1.1

At $x = - 1$ , its $n$ -th formal term is $(- 1)^{n + 1} (- 1)^{n} / n = - 1 / n$ .

givenalgebra

2.1

Hence the formal series is $- \sum_{n \geq 1} 1 / n$ , which diverges by [L2].

step 1.1L2

3.1

Thus $x = - 1$ cannot be added to the convergence interval in [L1].

step 2.1L1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The logarithm is not uniformly continuous on the positive half-line

Statement refuted

The natural logarithm is uniformly continuous on $(0, \infty)$ .

Facts & Assumptions

Given: The positive half-line and the natural logarithm.

[L1]

Uniform continuity has one $δ > 0$ for all pairs in the domain (Uniform continuity of $f : A \to R$ : one $δ$ serving every pair of points of $A$ ).

[L2]

$\log (x y) = \log x + \log y$ and $\log 2 > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm as the inverse of the exponential function).

[L3]

For every $δ > 0$ , some natural $n \geq 1$ satisfies $1 / n < δ$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Counterexample

technique · direct

1.1

For $n \geq 1$ , put $x_{n} = 1 / n$ and $y_{n} = 2 / n$ . Then $∣ x_{n} - y_{n} ∣ = 1 / n$ .

givenalgebra

2.1

The logarithm gap is $∣ \log y_{n} - \log x_{n} ∣ = ∣ \log 2 ∣ = \log 2$ .

step 1.1L2

3.1

With $ε = \log 2 / 2$ , every $δ > 0$ admits an $n$ from [L3] for which the pair in step 1.1 is within $δ$ but its image gap exceeds $ε$ .

step 1.1step 2.1L3

4.1

This contradicts [L1], so $\log$ is not uniformly continuous on $(0, \infty)$ .

step 3.1L1∎

The Logarithm and General Powers: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Two to the square root of two from rational suprema and from exp(sqrt(2) log 2)

Example

Facts & Assumptions

Verification

The alternating harmonic series sums to log 2

Example

Facts & Assumptions

Verification

Concrete logarithmic, polynomial, and exponential growth comparisons

Example

Facts & Assumptions

Verification

x^x tends to one as x tends to zero from the right

Example

Facts & Assumptions

Verification

The log(1+x) power series diverges at x=-1

Statement refuted

Facts & Assumptions

Counterexample

The logarithm is not uniformly continuous on the positive half-line

Statement refuted

Facts & Assumptions

Counterexample

Sources