Session-authored (Fable 5 assisted)

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=\sqrt2$ . The two constructions give the same number: $2^{[s]}=\sup\{2^q:q\in\mathbb Q,\ q<s\}=\exp(s\log2)=\lim_{q_n\to s,\ q_n\in\mathbb Q}2^{q_n}.$

Facts & Assumptions

Given: The nonnegative square root $s=\sqrt2$ .

[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]

$\sqrt2$ exists and is positive (Square roots exist: a unique $\sqrt{a} \ge 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\log2)$ .

L1L3

1.2

For every rational sequence $q_n\to s$ , [L2] gives $2^{q_n}\to2^s=\exp(s\log2)$ .

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=\log2.$

Facts & Assumptions

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

[L1]

At $x=1$ , $\log(1+x)=\sum_{n\ge1}(-1)^{n+1}x^n/n$ converges to $\log2$ ([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 $log2$ .

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}\to0,\qquad\frac{x^5}{\exp x}\to0,\qquad\frac{x^2}{\exp(3x)}\to0.$

Facts & Assumptions

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

[L1]

$\log x/x^\alpha\to0$ for every $\alpha>0$ (The logarithm grows more slowly than every positive real power).

[L2]

$x^m/\exp(ax)\to0$ 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 $\alpha=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\to0+}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\to0$ as $t\to+\infty$ (The logarithm grows more slowly than every positive real power).

[L3]

The exponential is continuous and $\exp0=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\to0$ by [L2].

2.1

Therefore $x^x=\exp(x\log x)\to\exp0=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\ge1}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\ge1}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 $\delta>0$ for all pairs in the domain (Uniform continuity of $f : A \to \mathbb{R}$ : one $\delta$ serving every pair of points of $A$ ).

[L2]

$\log(xy)=\log x+\log y$ and $\log2>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 $\delta>0$ , some natural $n\ge1$ satisfies $1/n<\delta$ (For every $\varepsilon > 0$ in a complete ordered field there is a natural $n \ge 1$ with $1/n < \varepsilon$ ).

Counterexample

technique · direct

1.1

For $n\ge1$ , 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|=|\log2|=\log2$ .

step 1.1L2

3.1

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

step 1.1step 2.1L3

4.1

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

step 3.1L1∎

Sources

Standard references

Recommended treatments; not extraction sources.