ExampleConstruction: AI-generatedVerification: 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.

$x ψ (1 / x) \to 0$ as $x \to 0$ , by the squeeze theorem

Example

Let $A : = R ∖ {0}$ and define $h : A \to R$ by

$h (x) : = x \cdot ψ (1 / x),$

with $ψ$ as in The trigonometry-free oscillator $ψ (x) = \inf_{n \in Z} ∣ x - n ∣$ is well defined and attained at a nearest integer, takes values in $[0, 1 / 2]$ , vanishes exactly on $Z$ , equals $1 / 2$ at half-integers, and is $1$ -periodic. Then $0$ is a limit point of $A$ , the limit of $h$ at $0$ exists, and

$\lim_{x \to 0} h (x) = 0.$

The point of the example. The factor $ψ (1 / x)$ has no limit at $0$ at all ( $ψ (1 / x)$ has no limit at $0$ : two sequences tending to $0$ give values constantly $0$ and constantly $1 / 2$ ), so Sums, scalar multiples, products and quotients of function limits, the quotient under the hypothesis that the denominator limit is nonzero cannot be applied to the product: its product rule requires both factors to have limits. What is available is that $ψ (1 / x)$ stays inside $[0, 1 / 2]$ , and a bounded factor multiplied by one tending to $0$ is killed. That is exactly what If $f \leq g \leq h$ near $c$ and $f$ and $h$ have the same limit at $c$ , then so does $g$ delivers, and it delivers the existence of the limit, not merely its value.

Facts & Assumptions

Given: The set $A = R ∖ {0}$ and the function $h : A \to R$ , $h (x) = x \cdot ψ (1 / x)$ , with $ψ$ the function of The trigonometry-free oscillator $ψ (x) = \inf_{n \in Z} ∣ x - n ∣$ is well defined and attained at a nearest integer, takes values in $[0, 1 / 2]$ , vanishes exactly on $Z$ , equals $1 / 2$ at half-integers, and is $1$ -periodic.

[L1]

Range of $ψ$ : $0 \leq ψ (u) \leq 1 / 2$ for every real $u$ (The trigonometry-free oscillator $ψ (x) = \inf_{n \in Z} ∣ x - n ∣$ is well defined and attained at a nearest integer, takes values in $[0, 1 / 2]$ , vanishes exactly on $Z$ , equals $1 / 2$ at half-integers, and is $1$ -periodic, claim 2).

[L2]

The limit condition (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ): $\lim_{x \to c} f (x) = P$ means that for every real $ε > 0$ there is a real $δ > 0$ such that every $x$ in the domain with $0 < ∣ x - c ∣ < δ$ satisfies $∣ f (x) - P ∣ < ε$ .

[L3]

Squeeze theorem: if $f \leq g \leq k$ on $A \cap N_{η}^{*} (c)$ for some real $η > 0$ , and the limits of $f$ and of $k$ at $c$ exist and are equal to $L$ , then the limit of $g$ at $c$ exists and equals $L$ (If $f \leq g \leq h$ near $c$ and $f$ and $h$ have the same limit at $c$ , then so does $g$ ).

[L4]

Absolute value: $∣ u ∣ \geq 0$ ; $∣ u ∣ = 0$ exactly when $u = 0$ ; $∣ u v ∣ = ∣ u ∣ ∣ v ∣$ ; $∣ - u ∣ = ∣ u ∣$ ; $∣ u ∣ = u$ for $u \geq 0$ ; and $- ∣ u ∣ \leq u \leq ∣ u ∣$ (Basic properties of the absolute value).

[L5]

Order and field arithmetic: $x \neq 0$ has an inverse $1 / x$ (Field); $0 < 1$ , so $2 > 0$ and $1 / 2 > 0$ with $t / 2 < t$ for $t > 0$ (The multiplicative identity is positive, Inverses of positives are positive, and reciprocation reverses order, Sign rules for products and monotonicity of multiplication); multiplying an inequality by a non-negative factor, and adding inequalities (Sign rules for products and monotonicity of multiplication, Order is preserved by adding a constant and by adding inequalities); the order is total (Ordered field). Those two sources state their moves in their STRICT forms only; the non-strict forms used below follow by adjoining the equality case, in which the two sides coincide (Ordered field).

[L6]

Limit point and neighbourhoods (Limit point, isolated point, adherent point, derived set, and dense subset of $R$ , The $ε$ -neighbourhood and the punctured $ε$ -neighbourhood of a point of $R$ ).

Verification

technique · direct

1.1

$0$ is a limit point of $A = R ∖ {0}$ : given a real $ε > 0$ , the real $ε / 2$ satisfies $ε / 2 > 0$ , so it lies in $A$ , and $0 < ∣ ε / 2 - 0 ∣ = ε / 2 < ε$ .

L4L5L6

1.2

$h$ is defined on all of $A$ , and $∣ h (x) ∣ \leq ∣ x ∣ / 2$ there: for $x \in A$ we have $x \neq 0$ , so $1 / x$ exists, and $∣ h (x) ∣ = ∣ x ∣ \cdot ψ (1 / x)$ by [L4], while $0 \leq ψ (1 / x) \leq 1 / 2$ by [L1] and $∣ x ∣ \geq 0$ , so multiplying the inequality $ψ (1 / x) \leq 1 / 2$ by the non-negative factor $∣ x ∣$ gives $∣ h (x) ∣ \leq ∣ x ∣ / 2$ .

L1L4L5

1.3

The two functions $x \mapsto - ∣ x ∣ / 2$ and $x \mapsto ∣ x ∣ / 2$ on $A$ each have limit $0$ at $0$ : given a real $ε > 0$ , take $δ : = ε$ ; every $x \in A$ with $0 < ∣ x - 0 ∣ < δ$ satisfies $∣ ∣ x ∣ / 2 - 0 ∣ = ∣ x ∣ / 2 < ε / 2 < ε$ , and likewise $∣ - ∣ x ∣ / 2 - 0 ∣ = ∣ x ∣ / 2 < ε$ .

L2L4L5

2.1

Hence $- ∣ x ∣ / 2 \leq h (x) \leq ∣ x ∣ / 2$ for every $x \in A$ , by [L4] applied to $∣ h (x) ∣ \leq ∣ x ∣ / 2$ .

step 1.2L4

3.1

The three functions satisfy $- ∣ x ∣ / 2 \leq h (x) \leq ∣ x ∣ / 2$ on all of $A$ , in particular on $A \cap N_{1}^{*} (0)$ , and the two outer ones have limit $0$ at $0$ ; since $0$ is a limit point of $A$ , the squeeze theorem [L3] gives that the limit of $h$ at $0$ exists and equals $0$ .

step 1.1step 1.3step 2.1L3∎

Remarks

Where the hypotheses of the squeeze theorem are met. The order hypothesis holds on all of $A$ , so any $η > 0$ serves and $η = 1$ is taken; the two outer limits are computed by hand in step 1.3; and $0$ is a limit point of $A$ by step 1.1, which is what makes every limit here well posed (The $ε$ - $δ$ limit $\lim_{x \to c} f (x) = L$ of $f : A \to R$ at a limit point $c$ of $A$ ).
Nothing about $ψ$ beyond its range is used. Replacing $ψ$ by any function with values in a fixed bounded set would give the same conclusion by the same three steps. What makes the example worth stating is the contrast with $ψ (1 / x)$ has no limit at $0$ : two sequences tending to $0$ give values constantly $0$ and constantly $1 / 2$ : the same oscillating factor, multiplied by $x$ or not, is the difference between a limit existing and not.
The classical version of this example is $x \sin (1 / x) \to 0$ as $x \to 0$ ; see The classical form of the oscillator above is $\sin (1 / x)$ , which this library can only construct much later for why this library writes $ψ$ and not $\sin$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

34 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

Squeeze theorem (Wikipedia) (standard reference, not scraped)
Limit of a function (Wikipedia) (standard reference, not scraped)
J. Lebl, Basic Analysis I, §3.1 (standard reference, not scraped)

x ψ(1/x)→0xψ(1/x)→0 as x→0x→0, by the squeeze theorem