Session-authored (Fable 5 assisted)

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.

✓ 3 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 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Further Trigonometric Identities and Inverse Functions: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Machin's formula $\pi/4=4\arctan(1/5)-\arctan(1/239)$

Example

Machin's formula is

$\frac\pi4=4\arctan\frac15-\arctan\frac1{239}.$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arctangent takes values in $(-\pi/2,\pi/2)$ , is the inverse of tangent there, and is strictly increasing (The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$ , Tangent is a continuous strictly increasing bijection from $(-\pi/2,\pi/2)$ onto $\mathbb R$ ).

[L2]

The tangent addition and subtraction formulas hold when their displayed denominators and domains are nonzero (Addition and subtraction formulas for tangent, cotangent, secant, and cosecant on their exact domains).

[L3]

Tangent is the quotient of sine by cosine; $\sin0=0$ and $\cos0=1$ ; and the cofunction and Pythagorean identities give $\tan(\pi/4)=1$ (Tangent, cotangent, secant, and cosecant on their exact natural domains, The derivatives of sine and cosine are cosine and minus sine, Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

Proof

technique · direct

1.1

Put $a:=\arctan(1/5)$ and $b:=\arctan(1/239)$ . Then $\tan a=1/5$ and $\tan b=1/239$ . Comparing with $\tan0=0$ and [L3] on the principal branch gives $0<a,b<\pi/4$ .

L1L3

2.1

Since $0<a<\pi/4$ , we have $0<2a<\pi/2$ , so the tangent addition formula applies. It gives $\tan(2a)=\frac5{12}<1=\tan(\pi/4).$ Strict increase of tangent on the principal branch now gives $2a<\pi/4$ , hence $0<4a<\pi/2$ .

step 1.1L1L2L3algebra

3.1

The addition formula, now applied to $2a+2a$ , gives $\tan(4a)=\frac{120}{119}>1.$ All displayed denominators are positive.

step 2.1L2algebra

4.1

A final use of [L2] gives $\tan(4a-b)= \frac{120/119-1/239}{1+(120/119)(1/239)}=1.$ The denominator is positive.

step 1.1step 3.1L2algebra

4.2

By step 2.1, $4a$ lies in the principal tangent interval. Since $\tan(4a)>1=\tan(\pi/4)$ , strict increase gives $4a>\pi/4>b$ . Thus $0<4a-b<4a<\pi/2$ . Consequently $4a-b$ and $\pi/4$ lie in the same injective branch of tangent.

step 1.1step 2.1step 3.1L1L3

5.1

Steps 4.1 and 4.2 imply $4a-b=\pi/4$ , which is the claimed formula.

step 4.1step 4.2∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

$\arcsin(\sin x)$ is not the identity outside the principal interval

Example

The identity $\arcsin(\sin x)=x$ is not valid for every $x\in\mathbb R$ . For example,

$\arcsin(\sin(3\pi/4))=\pi/4\ne3\pi/4.$

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

Principal arcsine is the inverse of sine with values restricted to $[-\pi/2,\pi/2]$ (Principal inverse sine and inverse cosine).

[L2]

The supplementary identity is $\sin(\pi-x)=\sin x$ (Cofunction, supplementary, quarter-turn, and reflection identities for the six trigonometric functions).

Proof

technique · direct

1.1

By [L2], $\sin(3\pi/4)=\sin(\pi/4)$ . Since $\pi/4$ lies in the principal range of arcsine, [L1] gives $\arcsin(\sin(3\pi/4))=\pi/4$ .

L1L2algebra

2.1

Since $\pi/4\ne3\pi/4$ , step 1.1 is the claimed counterexample.

step 1.1algebra∎

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-03Open item page →

Principal arcsine has no finite derivative at $-1$ or $1$

Example

The principal arcsine $\arcsin:[-1,1]\to[-\pi/2,\pi/2]$ has no finite derivative at either endpoint $1$ or $-1$ (with the library's relative, one-sided endpoint convention).

Facts & Assumptions

Given: No hypotheses beyond those quantified in the statement.

[L1]

On $[-1,1]$ , $\sin(\arcsin y)=y$ , and $\arcsin(1)=\pi/2$ , $\arcsin(-1)=-\pi/2$ (Principal inverse sine and inverse cosine).

[L2]

The chain rule applies to derivatives relative to their domains (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)$ ).

[L3]

$(\sin x)'=\cos x$ , while $\cos(\pi/2)=\cos(-\pi/2)=0$ (The derivatives of sine and cosine are cosine and minus sine, Quarter-turn values and shifts by pi/2 and pi, Pythagorean and parity identities for all six trigonometric functions on their natural domains).

Proof

technique · contradiction

1.1

Suppose $\arcsin$ had a finite derivative at $1$ . Differentiate the identity $\sin(\arcsin y)=y$ at $1$ relative to $[-1,1]$ . The derivative of the right side is $1$ , whereas [L2] and [L3] make the derivative of the left side $\cos(\pi/2)(\arcsin)'(1)=0$ , a contradiction.

assume-contraL1L2L3

1.2

The identical argument at $-1$ gives $1=\cos(-\pi/2)(\arcsin)'(-1)=0$ .

assume-contraL1L2L3

2.1

Therefore neither finite endpoint derivative exists.

step 1.1step 1.2discharge-contradiction∎

Sources

Standard references

Recommended treatments; not extraction sources.

Further Trigonometric Identities and Inverse Functions: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Machin's formula π/4=4arctan⁡(1/5)−arctan⁡(1/239)\pi/4=4\arctan(1/5)-\arctan(1/239)π/4=4arctan(1/5)−arctan(1/239)

Example

Facts & Assumptions

Proof

arcsin⁡(sin⁡x)\arcsin(\sin x)arcsin(sinx) is not the identity outside the principal interval

Example

Facts & Assumptions

Proof

Principal arcsine has no finite derivative at −1-1−1 or 111

Example

Facts & Assumptions

Proof

Sources

Standard references

Machin's formula $\pi/4=4\arctan(1/5)-\arctan(1/239)$

$\arcsin(\sin x)$ is not the identity outside the principal interval

Principal arcsine has no finite derivative at $-1$ or $1$