CounterexampleConstruction: AI-adaptedVerification: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

For every $x > 2$ the uncontinued Mercator series at $u = x - 1$ diverges

Statement refuted

The Mercator expression $\sum_{n = 1}^{\infty} (- 1)^{n + 1} (x - 1)^{n} / n$ does not define the natural logarithm for every $x > 0$ . For every $x > 2$ , this uncontinued series diverges.

Facts & Assumptions

Given: $x > 2$ and $u : = x - 1 > 1$ .

[L1]

The ratio test says that a series diverges if the lower limit of the absolute ratios of successive nonzero terms is greater than $1$ (Ratio test: $lim sup ∣ a_{k + 1} / a_{k} ∣ < 1$ gives absolute convergence and hence convergence, and $lim inf ∣ a_{k + 1} / a_{k} ∣ > 1$ gives divergence).

[L2]

If a series converges, then its terms tend to $0$ (If a series converges then its terms tend to $0$ ).

[L3]

The Mercator series gives local data on $- 1 < u \leq 1$ ; a separate product law continues those data uniquely to all positive inputs (The Mercator series, its value at $1$ and the product law determine $\log$ on all positive reals, while the series alone is only local).

Counterexample

technique · direct

1.1

Let $a_{n} = (- 1)^{n + 1} u^{n} / n$ for $n \geq 1$ . Every $a_{n}$ is nonzero, and $∣ \frac{a_{n + 1}}{a_{n}} ∣ = u \frac{n}{n + 1} ⟶ u > 1.$

givenalgebra

2.1

The ratio test [L1] therefore makes $\sum_{n} a_{n}$ divergent.

step 1.1L1

2.2

More explicitly, choose $q$ with $1 < q < u$ . The ratios in step 1.1 are at least $q$ for all sufficiently large $n$ , so $∣ a_{n} ∣$ then grows by a factor at least $q$ and cannot tend to $0$ ; [L2] again rules out convergence.

step 1.1L2choosealgebra

3.1

This does not conflict with [L3]: for $x > 2$ , the direct substitution $u = x - 1$ lies outside the local interval, and the value at $x$ is obtained by the product-law continuation instead.

step 2.1L3∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 87 results over 19 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

OpenStax, Calculus Volume 1, Section 6.7 (standard reference, not scraped)

For every x>2x>2 the uncontinued Mercator series at u=x−1u=x−1 diverges