ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck passjudge pass (z-ai/glm-5.2)audited 2026-07-27

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.

Condensation reduces $\sum 1 / k^{p}$ to a geometric series with ratio $2^{1 - p}$

Example

Let $p \in Q$ with $p > 0$ . Condensation (For a nonincreasing nonnegative sequence, $\sum a_{k}$ converges iff $\sum 2^{k} a_{2^{k}}$ converges) applied to the family $a_{k} = 1 / k^{p}$ , $k \geq 1$ , produces a geometric series of ratio $2^{1 - p}$ :

$2^{j} a_{2^{j}} = 2^{j} (2^{j})^{- p} = 2^{(1 - p) j} = (2^{1 - p})^{j} (j \in N) .$

So the whole $p$ -series family collapses onto the single question of when a geometric ratio is below $1$ , and the threshold $p = 1$ is where $2^{1 - p} = 2^{0} = 1$ . That is the computation behind For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ , displayed here on its own and instantiated at three exponents:

$p$	ratio $2^{1 - p}$	condensed series	verdict
$1 / 2$	$2^{1 / 2}$	diverges, ratio $> 1$	$\sum_{k \geq 1} k^{- 1 / 2}$ diverges
$1$	$1$	diverges, terms constantly $1$	$\sum_{k \geq 1} 1 / k$ diverges
$2$	$1 / 2$	converges, sum $2$	$\sum_{k \geq 1} 1 / k^{2}$ converges

Facts & Assumptions

Given: A rational $p > 0$ and the family $a_{k} : = ι (k)^{- p}$ for naturals $k \geq 1$ (Rational powers $a^{r}$ of a positive base, Canonical naturals are positive and strictly increasing).

[L1]

Condensation: for a nonnegative nonincreasing family from $1$ , $\sum_{k \geq 1} x_{k}$ converges if and only if $\sum_{j \geq 0} 2^{j} x_{2^{j}}$ converges (For a nonincreasing nonnegative sequence, $\sum a_{k}$ converges iff $\sum 2^{k} a_{2^{k}}$ converges, Nondecreasing, increasing, nonincreasing, decreasing, monotone, and eventually monotone sequences).

[L2]

Rational powers of a positive base: $a^{r + s} = a^{r} a^{s}$ , $(a^{r})^{s} = a^{r s}$ , $a^{- r} = 1 / a^{r}$ , $a^{r} > 0$ ; the integer power agrees with the rational power at an integer exponent, since $a^{1 / 1} = a$ ; and $a^{0} = 1$ (Laws of rational exponents, Rational powers $a^{r}$ of a positive base, Existence and uniqueness of $n$ -th roots: a unique $a^{1 / n} \geq 0$ with $(a^{1 / n})^{n} = a$ , Integer powers $a^{m}$ ).

[L3]

Monotonicity of rational powers: for $a > 1$ and rationals $r < s$ , $a^{r} < a^{s}$ ; and for rational $t > 0$ , $0 < a < b$ implies $a^{t} < b^{t}$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ).

[L4]

The geometric series $\sum_{j \geq 0} r^{j}$ converges exactly when $∣ r ∣ < 1$ , with sum $1 / (1 - r)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L5]

$\sum_{k \geq 1} 1 / k^{p}$ converges if and only if $p > 1$ (For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ ); the canonical naturals are positive and order preserving, and reciprocation reverses the order on the positives (Canonical naturals are positive and strictly increasing, Inverses of positives are positive, and reciprocation reverses order).

Verification

technique · direct

1.1

Each $a_{k} = ι (k)^{- p}$ is positive, and $a_{j} \geq a_{k}$ whenever $1 \leq j \leq k$ , since $ι (j)^{p} \leq ι (k)^{p}$ for $p > 0$ and reciprocation reverses the order; so condensation applies.

givenL3L5L1

1.2

For every $j \in N$ : $2^{j} a_{2^{j}} = 2^{j} (2^{j})^{- p} = 2^{j} \cdot 2^{- j p} = 2^{j - j p} = 2^{(1 - p) j} = (2^{1 - p})^{j}$ , reading each integer exponent as a rational one.

L2algebra

2.1

So the condensed series is the geometric series of ratio $r : = 2^{1 - p}$ , which is positive; and $r < 1$ exactly when $1 - p < 0$ , since $2 > 1$ makes $t \mapsto 2^{t}$ strictly increasing and $2^{0} = 1$ .

step 1.2L2L3

3.1

At $p = 2$ : the ratio is $2^{- 1} = 1 / 2$ , so the condensed series converges with sum $1 / (1 - 1 / 2) = 2$ , and $\sum_{k \geq 1} 1 / k^{2}$ converges.

step 1.2step 2.1L1L4L5

3.2

At $p = 1$ : the ratio is $2^{0} = 1$ , the condensed terms are constantly $1$ , so the condensed series diverges and $\sum_{k \geq 1} 1 / k$ diverges.

step 1.2step 2.1L1L4L5

3.3

At $p = 1 / 2$ : the ratio is $2^{1 / 2}$ , which exceeds $1$ because $2 > 1$ and $1 / 2 > 0$ ; so the condensed series diverges and $\sum_{k \geq 1} k^{- 1 / 2}$ diverges.

step 1.2step 2.1L1L3L4L5

4.1

The three verdicts agree with the $p$ -series theorem, whose content is exactly step 2.1 together with the geometric threshold.

step 3.1step 3.2step 3.3L5∎

Remarks

The sum of the condensed series is not the sum of the original. At $p = 2$ the condensed series sums to $2$ while $\sum_{k \geq 1} 1 / k^{2}$ sums to $π^{2} / 6$ . Condensation preserves the fact of convergence and nothing numerical, which is visible in its proof: the two estimates there differ by a factor $2$ .
Why the exponent has to be rational. The identity in step 1.2 is a chain of rational-exponent laws, and $2^{1 - p}$ is meaningful here only because $1 - p$ is rational (Rational powers $a^{r}$ of a positive base). The same computation with a real exponent is the standard one, and it waits for the exponential function.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

57 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

Cauchy condensation test (Wikipedia) (standard reference, not scraped)
Geometric series (Wikipedia) (standard reference, not scraped)
Stephen Semmes, Elements of Analysis (standard reference, not scraped)
John K. Hunter, An Introduction to Real Analysis (standard reference, not scraped)

Condensation reduces ∑1/kp∑1/kp to a geometric series with ratio 21−p21−p