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.

✓ 5 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 5 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Sine, Cosine, and the Definition of Pi: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The Bartle-Sherbert bounds 2.828 < pi < 3.185

Example

Let $γ = π / 2$ . Then $\sqrt{2} < γ < \sqrt{6 - 2 \sqrt{3}}, 2.828 < π < 3.185.$

Facts & Assumptions

Given: The first positive cosine zero $γ = π / 2$ .

[L1]

$\cos$ is strictly decreasing on $[0, 2]$ , with unique zero $γ$ (Pi as twice the smallest positive zero of cosine, Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3).

[L2]

The cosine power series and alternating-series remainder bounds are those of Sine and cosine defined by their real power series and The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ .

[L3]

Nonnegative square roots exist and preserve comparisons after squaring (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Verification

technique · direct

1.1

At $x = \sqrt{2}$ , the first two cosine terms cancel and the alternating tail beginning with $x^{4} / 4!$ is positive, so $\cos (\sqrt{2}) > 0$ .

L2L3

1.2

Put $a = \sqrt{6 - 2 \sqrt{3}}$ . Then $1 - a^{2} / 2 + a^{4} / 24 = 0$ , and the remaining alternating cosine tail begins negative with decreasing absolute terms, so $\cos a < 0$ .

L2L3algebra

2.1

Strict decrease and [L1] give $\sqrt{2} < γ < a$ .

step 1.1step 1.2L1

3.1

Since $(707 / 500)^{2} < 2$ , $2 \sqrt{2} > 707 / 250$ . Since $(433 / 250)^{2} < 3$ and $(637 / 400)^{2} > 6 - 2 (433 / 250)$ , one has $a < 637 / 400$ , hence $2 a < 637 / 200$ .

step 2.1L3algebra

4.1

Doubling the bounds of step 2.1 proves the displayed decimal bounds for $π$ .

step 2.1step 3.1∎

CounterexampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

sin(1/x) has no limit as x tends to zero

Statement refuted

The function $x \mapsto \sin (1 / x)$ , defined for $x \neq 0$ , has a limit at $0$ .

Facts & Assumptions

Given: The punctured real line.

[L1]

$\sin (π / 2 + 2 m π) = 1$ and $\sin (3 π / 2 + 2 m π) = - 1$ for integers $m$ (Quarter-turn values and shifts by pi/2 and pi, The zero sets of sine and cosine and the least positive common period 2 pi).

[L2]

A function limit implies convergence along every sequence in its punctured domain approaching the point (Heine criterion: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ ).

[L3]

Reciprocal natural-number sequences tend to zero (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

Counterexample

technique · direct

1.1

For $n \in N$ , put $x_{n} = 1 / (π / 2 + 2 π (n + 1))$ and $y_{n} = 1 / (3 π / 2 + 2 π (n + 1))$ . Both sequences are nonzero and tend to $0$ .

L3algebra

1.2

Their image values are $\sin (1 / x_{n}) = 1$ and $\sin (1 / y_{n}) = - 1$ .

2.1

A common function limit at zero would force both image sequences to converge to it, which is impossible.

step 1.1step 1.2L2∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

x sin(1/x) tends to zero despite its oscillation

Example

$\lim_{x \to 0} x \sin (1 / x) = 0,$ where the function is defined at $0$ by the displayed limit.

Facts & Assumptions

Given: A nonzero real $x$ approaching $0$ .

[L1]

$∣ \sin u ∣ \leq 1$ for every real $u$ (Parity and the Pythagorean identity for sine and cosine).

[L2]

The squeeze theorem for function limits holds (If $f \leq g \leq h$ near $c$ and $f$ and $h$ have the same limit at $c$ , then so does $g$ ).

Verification

technique · direct

1.1

From [L1], $∣ x \sin (1 / x) ∣ \leq ∣ x ∣$ for every $x \neq 0$ .

L1algebra

2.1

Since both $- ∣ x ∣$ and $∣ x ∣$ tend to $0$ , squeeze gives $x \sin (1 / x) \to 0$ .

step 1.1L2∎

ExampleConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

The extension of x^2 sin(1/x) by zero is differentiable but its derivative is discontinuous at zero

Example

Define $f (0) = 0$ and $f (x) = x^{2} \sin (1 / x)$ for $x \neq 0$ . Then $f$ is differentiable on $R$ , with $f^{'} (0) = 0$ , but $f^{'}$ is not continuous at $0$ .

Facts & Assumptions

Given: The function $f$ of the statement.

[L1]

$∣ \sin u ∣ \leq 1$ , $\sin^{'} = \cos$ , and the quarter-turn values of sine/cosine hold (Parity and the Pythagorean identity for sine and cosine, The derivatives of sine and cosine are cosine and minus sine, Quarter-turn values and shifts by pi/2 and pi).

[L2]

The chain and derivative-algebra rules, and the derivative definition, hold (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L3]

A function limit implies the same limit along every punctured convergent sequence (Heine criterion: $\lim_{x \to c} f (x) = L$ iff $f (x_{k}) \to L$ for every sequence in $A ∖ {c}$ converging to $c$ ).

Verification

technique · direct

1.1

The difference quotient at zero is $f (x) / x = x \sin (1 / x)$ , whose absolute value is at most $∣ x ∣$ ; hence $f^{'} (0) = 0$ .

L1L2

1.2

For $x \neq 0$ , product and chain rules give $f^{'} (x) = 2 x \sin (1 / x) - \cos (1 / x)$ .

L1L2

2.1

Along $r_{n} = 1 / (2 π (n + 1))$ , the derivative tends to $- 1$ ; along $s_{n} = 1 / ((2 n + 1) π)$ , it tends to $1$ .

step 1.2L1algebra

3.1

Both sequences tend to zero, so [L3] shows that $f^{'}$ has no limit at zero and is not continuous there.

step 2.1L3∎

False statementConstruction: AI-adaptedVerification: AI-generatedprecheck passaudited 2026-08-02Open item page →

A sector-area squeeze proves lim sin(x)/x=1 without first calibrating angle measure

Statement

False claim: the sector-area inequalities $\sin θ < θ < \tan θ$ prove $\lim_{x \to 0} \sin x / x = 1$ without any prior calibration of the angle variable $θ$ to arc length, sector area, and $π$ .

Facts & Assumptions

Given: The analytic sine function and the definition $π = 2 γ$ from the first positive cosine zero.

[L1]

The analytic proof already establishes $\lim_{x \to 0} \sin x / x = 1$ (The limit of sin x divided by x at zero is one).

[L2]

$π$ is defined analytically from cosine, not from geometric sector area (Pi as twice the smallest positive zero of cosine).

Refutation

technique · direct

1.1

The sector inequality uses an angle measured in radians, and its usual derivation identifies that measure through arc length or sector area in the unit circle.

given

1.2

Establishing that identification requires a normalization constant, equivalently the relationship between the geometric full turn and the analytic $π$ of [L2].

2.1

Thus the sector argument cannot be used as a foundation independent of that calibration; it may prove the limit only after importing the relation whose analytic construction it was meant to justify.

step 1.1step 1.2

3.1

The limit itself remains true by [L1], but the claimed independent proof is false.

step 2.1L1∎

Sine, Cosine, and the Definition of Pi: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The Bartle-Sherbert bounds 2.828 < pi < 3.185

Example

Facts & Assumptions

Verification

sin(1/x) has no limit as x tends to zero

Statement refuted

Facts & Assumptions

Counterexample

x sin(1/x) tends to zero despite its oscillation

Example

Facts & Assumptions

Verification

The extension of x^2 sin(1/x) by zero is differentiable but its derivative is discontinuous at zero

Example

Facts & Assumptions

Verification

A sector-area squeeze proves lim sin(x)/x=1 without first calibrating angle measure

Statement

Facts & Assumptions

Refutation

Sources