Alphabeta Math
False statementConstruction: AI-adaptedVerification: AI-generatedprecheck 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.

FALSE: a function with a limit at c is bounded on its whole domain

Statement

False claim: let A⊆R, let c be a limit point of A (Limit point, isolated point, adherent point, derived set, and dense subset of R) and let f:A→R have a limit at c (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A). Then f is bounded on A, that is, the image f(A) is a bounded subset of R (Lower bound, bounded below, bounded set).

What is true is the local statement, If f has a finite limit at c then f is bounded on some punctured neighbourhood of c: there is a radius δ>0 such that f is bounded on A∩Nδ∗(c). The radius is produced by the limit condition at the single tolerance ε=1, and it carries no information whatever about the values of f far from c, which the limit condition never constrains.

The witness below is f(x)=1/x on (0,∞) at the point c=1: the limit there is 1, and f is bounded near 1, while on the whole domain f takes values above every real.

Facts & Assumptions

Given: The set A:=(0,∞) (Intervals of R: the nine order-convex forms, nondegeneracy, and length), the point c:=1, and the function f:A→R with f(x):=1/x=x−1.

[L1]

The limit condition (The ε-δ limit lim⁡x→cf(x)=L of f:A→R at a limit point c of A): lim⁡x→ch(x)=P means that for every real ε>0 there is a real δ>0 such that every x in the domain of h with 0<∣x−c∣<δ satisfies ∣h(x)−P∣<ε.

[L3]

Absolute value: ∣u∣≥0; ∣u∣=u for u≥0; ∣uv∣=∣u∣ ∣v∣; ∣−u∣=∣u∣; and for t>0, ∣u∣<t is equivalent to −t<u<t (Basic properties of the absolute value).

[L4]

Inverses and order: a>0 gives a−1>0, and 0<a<b gives 0<b−1<a−1 (Inverses of positives are positive, and reciprocation reverses order); (a−1)−1=a for a≠0, inverses being unique (Field); and for t>0, u<v is equivalent to ut<vt (Sign rules for products and monotonicity of multiplication).

[L5]

Order arithmetic: 0<1, hence 2>0 and 1/2>0 with 1−1/2=1/2 (The multiplicative identity is positive, Order is preserved by adding a constant and by adding inequalities); of two positive reals the smaller is positive, the order being total (Ordered field).

[L6]

Archimedean property: for every real M there is a natural n≥1 with M<n⋅1R, and the canonical naturals satisfy n⋅1R>0 (Every complete ordered field is Archimedean, Canonical naturals are positive and strictly increasing, Complete ordered field (least-upper-bound property)).

[L7]

Bounded set: S⊆R is bounded when it has an upper bound and a lower bound; a set with no upper bound is not bounded (Lower bound, bounded below, bounded set).

Refutation

technique · direct
1.1

The point 1 lies in A=(0,∞) and is a limit point of A: given a real ε>0, let ρ be the smaller of ε and 1, so ρ>0; then 1+ρ/2>1>0 lies in A and satisfies 0<∣(1+ρ/2)−1∣=ρ/2<ε.

L2L3L5
1.2

f is well defined on A: every x∈A has x>0, hence x≠0 and x−1 exists, with x−1>0.

L4L7
2.1

The limit of f at 1 exists and equals 1. Let ε>0 be an arbitrary real and let δ be the smaller of 1/2 and ε/2, so δ>0. For x∈A with 0<∣x−1∣<δ we get x>1−1/2=1/2>0, hence 0<1/x<2 by [L4]; and ∣1/x−1∣=∣(1−x)/x∣=∣x−1∣⋅(1/x)<δ⋅2≤ε.

step 1.1step 1.2L1L3L4L5
2.2

The image f(A) has no upper bound. Let M be an arbitrary real; by [L6] fix a natural n≥1 with M<n⋅1R, and note n⋅1R>0. Then x:=(n⋅1R)−1 satisfies x>0, so x∈A, and f(x)=x−1=n⋅1R>M. So no real bounds f(A) above, and f(A) is not bounded.

step 1.2L4L6L7
3.1

So f has a limit at the limit point c=1 of its domain and is unbounded on that domain: the claim is false, while If f has a finite limit at c then f is bounded on some punctured neighbourhood of c remains true and gives boundedness on A∩N1/2∗(1), where indeed 0<f(x)<2 by step 2.1.

step 2.1step 2.2L7∎

Remarks

  • The limit hypothesis is entirely local and the conclusion asked for is global, so no argument could bridge them. The witness makes that concrete by putting the unbounded behaviour at the other end of the domain, arbitrarily far from c in the only sense available here.

  • The sequential analogue is true, and that contrast is worth noting: a convergent sequence is bounded (Every convergent sequence is bounded), because a sequence has only finitely many terms outside any tail, and finitely many reals are bounded. A function has no such structure: the part of A outside a punctured neighbourhood of c can be infinite and can carry arbitrary values.

  • A bounded version does hold with an extra hypothesis: if A is itself contained in a punctured neighbourhood of c on which the limit estimate applies, then local and global boundedness coincide. That is a hypothesis on the domain, not a theorem about limits.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

25 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