ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck passjudge 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.

Geometric sequences: the complete classification for every real ratio

Example

For every real $r$ , let $a_{k} = r^{k}$ for natural $k \geq 0$ , using the integer powers of Integer powers $a^{m}$ , so $a_{0} = 1$ even when $r = 0$ , and $a_{k + 1} = a_{k} r$ . This notation is valid for negative real ratios and is not rational exponentiation of a negative base. The complete classification is: if $∣ r ∣ < 1$ , then $r^{k} \to 0$ ; if $r = 1$ , the sequence is constantly $1$ and converges to $1$ ; if $r = - 1$ , its even and odd subsequences are constantly $1$ and $- 1$ , so it is bounded but divergent; if $r > 1$ , then $r^{k} \to + \infty$ ; if $r < - 1$ , then $∣ r^{k} ∣ \to + \infty$ , while the even subsequence diverges to $+ \infty$ and the odd subsequence to $- \infty$ , and the whole sequence neither converges nor diverges to either signed infinity. Consequently $(r^{k})$ converges exactly when $- 1 < r \leq 1$ . Here signed-infinity assertions mean Divergence to $+ \infty$ and to $- \infty$ , not a finite limit value. Quantitative checks: if $0 < ∣ r ∣ < 1$ and $h = ∣ r ∣^{- 1} - 1 > 0$ , then $∣ r^{k} ∣ \leq (1 + k h)^{- 1}$ for every natural $k$ , and for $k \geq 1$ one has $∣ r^{k} ∣ < (k h)^{- 1}$ ; if $∣ r ∣ > 1$ and $d = ∣ r ∣ - 1 > 0$ , then $∣ r^{k} ∣ \geq 1 + k d$ . The weak Bernoulli estimates have equality for $k = 0, 1$ and are strict for $k \geq 2$ . Thus $(1 / 2)^{k}$ and $(- 1 / 2)^{k}$ are both null, $2^{k}$ diverges positively, and $(- 2)^{k}$ grows in absolute value while alternating sign.

Facts & Assumptions

Given: A real $r$ , the sequence $a_{k} : = r^{k}$ with integer powers (Integer powers $a^{m}$ , Sequences of reals: bounded, eventually, frequently, tails, subsequences), the alternating sequence $(s_{k})$ with $s_{0} = 1$ , $s_{σ (k)} = - s_{k}$ and its index map $n$ with $n_{0} = 0$ , $n_{σ (j)} = σ (σ (n_{j}))$ (FALSE: every bounded sequence converges), and $m_{j} : = σ (n_{j})$ .

[F1]

Integer powers: $a^{0} = 1$ and $a^{j + 1} = a^{j} a$ for every real $a$ and every natural $j$ (Integer powers $a^{m}$ ).

[F2]

Power laws: $a^{i + j} = a^{i} a^{j}$ , $(a^{i})^{j} = a^{i j}$ and $(a b)^{j} = a^{j} b^{j}$ for all naturals $i, j$ ; and if $a \neq 0$ then $a^{j} \neq 0$ for every $j$ (Laws of integer exponents).

[F3]

Signs of powers: if $a \geq 0$ then $a^{j} \geq 0$ , and if $a > 0$ then $a^{j} > 0$ (Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ ).

[F4]

Bernoulli's inequality: for $x \geq - 1$ and every natural $j$ , $(1 + x)^{j} \geq 1 + j x$ , with equality if and only if $j \leq 1$ or $x = 0$ (Bernoulli's inequality $(1 + x)^{n} \geq 1 + n x$ ).

[F5]

Archimedean property: for every real $x$ there is a natural number $j \geq 1$ with $x < j \cdot 1_{R}$ (Every complete ordered field is Archimedean).

[F6]

Inverses of positives: $a > 0$ implies $a^{- 1} > 0$ ; and $0 < a < b$ implies $0 < b^{- 1} < a^{- 1}$ (Inverses of positives are positive, and reciprocation reverses order).

[F7]

Canonical naturals: $n \mapsto n \cdot 1_{R}$ is strictly increasing, hence preserves non-strict order, on ${1, 2, 3, \dots}$ (Canonical naturals are positive and strictly increasing).

[F8]

$0 < 1$ and $1 \neq 0$ (The multiplicative identity is positive).

[F9]

Absolute value: $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ , $∣ - u ∣ = ∣ u ∣$ , $∣ u ∣ \geq 0$ , $∣ u ∣ = 0$ if and only if $u = 0$ , and $∣ u ∣ = u$ for $u \geq 0$ (Basic properties of the absolute value, Absolute value in an ordered field).

[F10]

A product with a zero factor vanishes: $0 \cdot a = 0$ (Multiplication by zero: $0 \cdot a = 0$ ).

[F11]

The alternating sequence: $(s_{k})$ is the unique sequence with $s_{0} = 1$ and $s_{σ (k)} = - s_{k}$ (FALSE: every bounded sequence converges).

[F25]

The index map $n$ of the same item satisfies $n_{0} = 0$ , $n_{σ (j)} = σ (σ (n_{j}))$ , is strictly increasing, and has $s_{n_{j}} = 1$ for every $j$ (FALSE: every bounded sequence converges).

[F12]

Growth of index maps: if $p$ is strictly increasing then $p_{j} \geq j$ for every $j$ (A strictly increasing index map satisfies $n_{k} \geq k$ ).

[F13]

Consecutive comparisons suffice: if $p_{i} < p_{σ (i)}$ for every $i$ then $p$ is strictly increasing (A strictly increasing index map satisfies $n_{k} \geq k$ ).

[F14]

Discreteness: for naturals $a, b$ , $a < b ⟺ σ (a) \leq b$ (Discreteness: $σ (n)$ is the immediate successor).

[F15]

Subsequences inherit limits, and the divergence test: if a sequence converges to $x$ and $p$ is strictly increasing, then the subsequence along $p$ converges to $x$ ; consequently, if two subsequences converge to different limits the sequence does not converge (Subsequences inherit the limit).

[F16]

Every convergent sequence is bounded (Every convergent sequence is bounded).

[F17]

Divergence to $+ \infty$ and to $- \infty$ means, respectively, that for every real $M$ one has $x_{k} > M$ eventually and $x_{k} < M$ eventually (Divergence to $+ \infty$ and to $- \infty$ ).

[F18]

Trichotomy, and $u \leq v < w$ implies $u < w$ (Ordered field).

[F19]

Scaling a strict inequality by a positive factor: if $c > 0$ then $a < b ⟺ a c < b c$ (Sign rules for products and monotonicity of multiplication).

[F20]

Convergence: $(z_{k})$ converges to $z$ when for every rational $ε > 0$ there is $K$ with $∣ z_{k} - z ∣ < ε$ for all $k \geq K$ (Limits and Cauchy sequences of reals).

[F21]

Field arithmetic: multiplication is associative and commutative, it distributes over addition, and every nonzero element has a multiplicative inverse (Field).

[F22]

Adding a constant preserves the strict order: $a < b$ implies $a + c < b + c$ (Order is preserved by adding a constant and by adding inequalities).

[F23]

Induction principle: if a property $P$ satisfies $P (0)$ and $P (n) \Rightarrow P (σ (n))$ for all $n$ , then $P (n)$ holds for all $n \in N$ (The principle of mathematical induction).

[F24]

Boundedness: $(z_{k})$ is bounded when there is a real $M$ with $∣ z_{k} ∣ \leq M$ for every $k \in N$ ; it is unbounded otherwise (Sequences of reals: bounded, eventually, frequently, tails, subsequences).

Verification

technique · cases

1.1baseihdischarge-inductiongivenF1F8F9F23

Absolute values of powers: for every real $r$ and every $k$ one has $∣ r^{k} ∣ = ∣ r ∣^{k}$ , by induction. The base case is $∣ r^{0} ∣ = ∣ 1 ∣ = 1 = ∣ r ∣^{0}$ by [F1], [F8] and [F9]; and assuming $∣ r^{k} ∣ = ∣ r ∣^{k}$ for a fixed $k$ , the recursion [F1] and multiplicativity [F9] give $∣ r^{σ (k)} ∣ = ∣ r^{k} r ∣ = ∣ r^{k} ∣ ∣ r ∣ = ∣ r ∣^{k} ∣ r ∣ = ∣ r ∣^{σ (k)}$ . Hence by the induction principle [F23] the identity holds for every $k$ ; in particular $∣ (- b)^{k} ∣ = ∣ - b ∣^{k} = b^{k}$ for every real $b \geq 0$ and every $k$ .

1.2givenF4F5F6F7F9F17F19algebra

Growth for bases above $1$ : let $b > 1$ be real and put $d : = b - 1 > 0$ . Bernoulli [F4] gives $b^{k} = (1 + d)^{k} \geq 1 + k d$ for every $k$ , with equality exactly when $k \leq 1$ , since $d \neq 0$ . Given any real $M$ , apply [F5] to the real $1 + ∣ M / d ∣$ to get a natural $N \geq 1$ with $N > 1 + ∣ M / d ∣$ ; then $N d > d + ∣ M ∣ \geq ∣ M ∣$ , so for every $k \geq N$ the order preservation [F7] and scaling by $d > 0$ [F19] give $k d \geq N d > ∣ M ∣ \geq M$ , hence $b^{k} \geq 1 + k d > M$ . Therefore $b^{k} \to + \infty$ in the sense of [F17].

1.3assume-case zerogivenF1F9F10F20

The case $r = 0$ : here $r^{0} = 1$ by [F1], and $r^{k} = 0$ for every $k \geq 1$ by induction, since $r^{σ (k)} = r^{k} r$ and a product with a zero factor vanishes [F10]. Given a rational $ε > 0$ , for every $k \geq 1$ we have $∣ r^{k} - 0 ∣ = ∣ 0 ∣ = 0 < ε$ by [F9], so $r^{k} \to 0$ by [F20] with threshold $K = 1$ .

1.4F9F20

Constant sequences converge to their values: for every real $c$ , given a rational $ε > 0$ one has $∣ c - c ∣ = ∣ 0 ∣ = 0 < ε$ at every index by [F9], so the threshold $K = 0$ witnesses [F20].

1.5baseihdischarge-inductiongivenF1F2F9F11F21F23

Alternating powers: for every positive real $b$ and every $k$ , $(- b)^{k} = s_{k} b^{k}$ by induction: the base case is $(- b)^{0} = 1 = s_{0} b^{0}$ , and if $(- b)^{k} = s_{k} b^{k}$ then $(- b)^{σ (k)} = (- b)^{k} (- b) = s_{k} b^{k} (- b) = (- s_{k}) b^{k} b = s_{σ (k)} b^{σ (k)}$ by [F1], [F2], [F11] and field arithmetic [F21]. Alongside, $∣ s_{k} ∣ = 1$ for every $k$ by induction: $∣ s_{0} ∣ = ∣ 1 ∣ = 1$ , and $∣ s_{σ (k)} ∣ = ∣ - s_{k} ∣ = ∣ s_{k} ∣ = 1$ by [F9] and [F11].

1.6givenF11F12F13F14F25

The index maps: $n$ is strictly increasing with $n_{0} = 0$ and $s_{n_{j}} = 1$ [F25], so $n_{j} \geq j$ [F12]; the map $m_{j} = σ (n_{j})$ is strictly increasing, because $n_{j} < n_{σ (j)}$ gives $m_{j} = σ (n_{j}) \leq n_{σ (j)} < σ (n_{σ (j)}) = m_{σ (j)}$ by [F14] and [F13], and then $m_{j} \geq j$ by [F12]; moreover $s_{m_{j}} = s_{σ (n_{j})} = - s_{n_{j}} = - 1$ by [F11].

2.1assume-case smallstep 1.1givenF2F3F4F5F6F7F9F19F20F21algebra

The case $0 < ∣ r ∣ < 1$ : put $b : = ∣ r ∣ \in (0, 1)$ and $h : = b^{- 1} - 1 > 0$ , positive by [F6]. Bernoulli [F4] applied to $h \geq - 1$ gives $(b^{- 1})^{k} = (1 + h)^{k} \geq 1 + k h$ for every $k$ , with equality exactly when $k \leq 1$ ; since $b^{k} (b^{- 1})^{k} = (b b^{- 1})^{k} = 1^{k} = 1$ by [F2], uniqueness of inverses [F21] gives $b^{k} = ((b^{- 1})^{k})^{- 1} \leq (1 + k h)^{- 1}$ by the reciprocal reversal [F6], both sides positive by [F3]; for $k \geq 1$ also $1 + k h > k h > 0$ , so $(1 + k h)^{- 1} < (k h)^{- 1}$ and $∣ r^{k} ∣ = b^{k} < (k h)^{- 1}$ by step 1.1. Now let a rational $ε > 0$ be given; [F5] applied to $1 / (h ε)$ supplies a natural $N \geq 1$ with $N > 1 / (h ε)$ , so $(N h)^{- 1} < ε$ ; for every $k \geq N$ the order preservation [F7] and scaling by $h > 0$ [F19] give $k h \geq N h$ , hence $(k h)^{- 1} \leq (N h)^{- 1} < ε$ by [F6], and therefore $∣ r^{k} - 0 ∣ = ∣ r^{k} ∣ < ε$ by [F9]. So $r^{k} \to 0$ .

2.2assume-case unitstep 1.4givenF1

The case $r = 1$ : then $r^{k} = 1$ for every $k$ , by induction from $1^{0} = 1$ and $1^{σ (k)} = 1^{k} \cdot 1 = 1$ by [F1]; hence $r^{k} \to 1$ by step 1.4.

2.3assume-case negunitstep 1.1step 1.4step 1.5step 1.6givenF8F15F17F18F22F24

The case $r = - 1$ : by step 1.5 with $b = 1$ one has $r^{k} = (- 1)^{k} = s_{k}$ for every $k$ . The even subsequence along $n$ is constantly $1$ and the odd subsequence along $m$ is constantly $- 1$ : $r^{n_{j}} = s_{n_{j}} = 1$ and $r^{m_{j}} = s_{m_{j}} = - 1$ by step 1.6, and both index maps are strictly increasing by step 1.6, so these are subsequences in the sense of [F15] converging to $1$ and to $- 1$ respectively. The limits differ: $- 1 < 1$ since $0 < 1$ by [F8] and adding $- 1$ preserves the order by [F22], so $1 \neq - 1$ by [F18], and the divergence test [F15] shows that $(r^{k})$ does not converge. It is bounded in the sense of [F24], since $∣ r^{k} ∣ = ∣ r ∣^{k} = 1$ for every $k$ by step 1.1, and it diverges to neither signed infinity: at the bound $M = 1$ the condition $x_{k} > 1$ of [F17] fails at every index, and at $M = - 1$ the condition $x_{k} < - 1$ fails at every index.

2.4assume-case bigstep 1.2givenF3F16F17F24

The case $r > 1$ : with $b : = r > 1$ , step 1.2 gives $b^{k} \to + \infty$ , and $r^{k} = b^{k}$ for every $k$ ; hence $r^{k} \to + \infty$ in the sense of [F17]. Since the terms are positive and eventually exceed every real bound, the sequence is unbounded and cannot converge by [F16].

2.5assume-case negbigstep 1.1step 1.2step 1.5step 1.6givenF9F16F17F24

The case $r < - 1$ : put $b : = ∣ r ∣ > 1$ . By step 1.5, $r^{k} = s_{k} b^{k}$ for every $k$ , so $∣ r^{k} ∣ = ∣ s_{k} ∣ b^{k} = b^{k} \to + \infty$ by step 1.1, step 1.2 and [F9]; since $b^{k}$ exceeds every real eventually, no real $M$ satisfies $∣ r^{k} ∣ \leq M$ for all $k$ , so $(r^{k})$ is unbounded in the sense of [F24] and therefore not convergent by [F16]. Along the even index map, $r^{n_{j}} = s_{n_{j}} b^{n_{j}} = b^{n_{j}}$ by step 1.6: given a real $M$ , step 1.2 gives $K$ with $b^{k} > M$ for all $k \geq K$ , while $n_{j} \geq j \geq K$ for $j \geq K$ by step 1.6, so $r^{n_{j}} = b^{n_{j}} > M$ for all $j \geq K$ , which is divergence of that subsequence to $+ \infty$ by [F17]. Along the odd index map, $r^{m_{j}} = s_{m_{j}} b^{m_{j}} = - b^{m_{j}}$ by step 1.6: given a real $M$ , step 1.2 supplies $K$ such that $b^{k} > - M$ for $k \geq K$ , and $m_{j} \geq j \geq K$ for $j \geq K$ by step 1.6; hence $b^{m_{j}} > - M$ , so $- b^{m_{j}} < M$ for every $j \geq K$ , so the odd subsequence diverges to $- \infty$ by [F17]. Finally the whole sequence fails both signed-infinity tests at $M = 0$ : the condition $x_{k} > 0$ eventually fails because $r^{m_{j}} = - b^{m_{j}} < 0$ at the arbitrarily large indices $m_{j} \geq j$ , and the condition $x_{k} < 0$ eventually fails because $r^{n_{j}} = b^{n_{j}} > 0$ at the arbitrarily large indices $n_{j} \geq j$ ; so it neither converges nor diverges to either signed infinity.

3.1cases-exhaustivestep 1.2step 1.3step 2.1step 2.2step 2.3step 2.4step 2.5givenF18∎

The cases are exhaustive: by trichotomy [F18] every real $r$ satisfies exactly one of $r < - 1$ , $r = - 1$ , $- 1 < r < 1$ , $r = 1$ , $r > 1$ , and these have been disposed of in steps 2.5, 2.3, 2.1 and 1.3 (for $- 1 < r < 1$ , splitting at $r = 0$ ), 2.2 and 2.4 respectively. So $(r^{k})$ converges exactly when $- 1 < r \leq 1$ : to $0$ for $- 1 < r < 1$ by steps 1.3 and 2.1, and to $1$ for $r = 1$ by step 2.2, while it diverges for $r = - 1$ , for $r > 1$ and for $r < - 1$ . The quantitative bounds are those derived in steps 1.2 and 2.1 — $∣ r^{k} ∣ \leq (1 + k h)^{- 1}$ and $∣ r^{k} ∣ < (k h)^{- 1}$ for $k \geq 1$ when $0 < ∣ r ∣ < 1$ , and $∣ r^{k} ∣ \geq 1 + k d$ when $∣ r ∣ > 1$ — and the displayed numerical instances $(1 / 2)^{k}$ , $(- 1 / 2)^{k}$ (null), $2^{k}$ (diverging to $+ \infty$ ) and $(- 2)^{k}$ (absolute values diverging, signs alternating) are the substitutions $r = \pm 1 / 2$ and $r = \pm 2$ into the proved clauses.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

61 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

John K. Hunter, An Introduction to Real Analysis (complete author-hosted lecture notes) (standard reference, not scraped)
Jiri Lebl, Basic Analysis I: Introduction to Real Analysis, Volume I (standard reference, not scraped)