TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-14

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.

Analytic sine and cosine agree with right-triangle ratios

Statement

Given $A, O > 0$ , put

$H = \sqrt{A^{2} + O^{2}}, P = (A, O) .$

There is a unique $θ \in (0, π / 2)$ such that

$(\frac{A}{H}, \frac{O}{H}) = (\cos θ, \sin θ) .$

The counterclockwise unit-circle arc from $(1, 0)$ to $(A / H, O / H)$ has radian measure $θ$ . The coordinate right triangle with vertices $(0, 0)$ , $(A, 0)$ , and $P$ therefore satisfies

$\cos θ = \frac{A}{H}, \sin θ = \frac{O}{H} .$

Facts & Assumptions

Given: Positive real numbers $A$ and $O$ , with $H = \sqrt{A^{2} + O^{2}}$ and $P = (A, O)$ .

[F1]

Every nonnegative real $a$ has a unique nonnegative square root $\sqrt{a}$ satisfying $(\sqrt{a})^{2} = a$ (Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

[F2]

For $(x, y) \in R^{2}$ , the Euclidean norm is $∥ (x, y) ∥_{2} = \sqrt{x^{2} + y^{2}}$ (The $p$ -norms $∥ x ∥_{p}$ for rational $p \geq 1$ , and $∥ x ∥_{\infty}$ ).

[F3]

Sine and cosine are differentiable on $R$ , with $(\sin x)^{'} = \cos x$ , $(\cos x)^{'} = - \sin x$ , $\sin 0 = 0$ , and $\cos 0 = 1$ (The derivatives of sine and cosine are cosine and minus sine).

[F4]

A real function differentiable on a set is continuous at every point of that set (A function differentiable at $c$ is continuous at $c$ ).

[F5]

If $f : [a, b] \to R$ is continuous and $y$ lies between $f (a)$ and $f (b)$ , then $f (c) = y$ for some $c \in [a, b]$ (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a, b]$ takes every value between $f (a)$ and $f (b)$ ).

[F6]

The number $π / 2$ is the smallest positive zero of cosine, and $π > 0$ (Pi as twice the smallest positive zero of cosine).

[F7]

For $0 < x \leq 2$ , one has $\sin x \geq x - x^{3} / 6 \geq x / 3 > 0$ ; also $\cos 2 \leq - 1 / 3$ , and cosine is strictly decreasing on $[0, 2]$ (Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3).

[F8]

For every real $x$ , $\sin^{2} x + \cos^{2} x = 1$ (Parity and the Pythagorean identity for sine and cosine).

[F9]

If $γ (t) = (\cos t, \sin t)$ and $0 \leq t \leq 2 π$ , then the counterclockwise angle swept from $γ (0) = (1, 0)$ to $γ (t)$ has radian measure $L (γ ⁣ ↾_{[0, t]}) = t$ (Radian angle by unit-circle arc length).

Proof

technique · direct

1.1

Since $A, O > 0$ , the number $A^{2} + O^{2}$ is positive. Hence [F1] gives $H \geq 0$ with $H^{2} = A^{2} + O^{2} > 0$ , so in fact $H > 0$ .

givenF1algebra

1.2

By [F3], cosine is differentiable on $R$ , so [F4] makes it continuous there and hence on every closed subinterval.

F3F4

2.1

From $H^{2} = A^{2} + O^{2} > A^{2}$ and $H, A > 0$ one gets $H > A$ ; similarly $H > O$ . Thus $0 < A / H < 1$ , $0 < O / H < 1$ , and $(A / H)^{2} + (O / H)^{2} = 1.$

step 1.1givenalgebra

2.2

Since $\cos 0 = 1$ and $\cos 2 \leq - 1 / 3 < 0$ , [F5] applied on $[0, 2]$ gives a $c \in (0, 2)$ with $\cos c = 0$ .

step 1.2F3F5F7choose

2.3

By [F2] and [F1], the three side vectors $(A, 0)$ , $(0, O)$ , and $(A, O)$ have Euclidean lengths $A$ , $O$ , and $H$ , respectively.

givenstep 1.1F1F2algebra

3.1

By [F6], $π / 2$ is the smallest positive zero of cosine. Step 2.2 therefore gives $0 < π / 2 \leq c < 2,$ and in particular $π / 2 < 2$ .

step 2.2F6algebra

4.1

Thus $[0, π / 2] \subset [0, 2)$ , and [F7] shows that cosine is strictly decreasing on $[0, π / 2]$ .

step 3.1F7

4.2

On $[0, π / 2]$ , cosine is continuous by step 1.2 and has endpoint values $\cos 0 = 1$ and $\cos (π / 2) = 0$ by [F3] and [F6]. Since $0 < A / H < 1$ , [F5] gives a $θ \in (0, π / 2)$ with $\cos θ = A / H$ .

step 1.2step 2.1step 3.1F3F5F6choose

5.1

If $φ \in (0, π / 2)$ also satisfies $\cos φ = A / H$ , then strict decrease from step 4.1 forces $φ = θ$ . Hence the angle in step 4.2 is unique.

step 4.1step 4.2algebra

5.2

The Pythagorean identity gives $\sin^{2} θ = 1 - \cos^{2} θ = 1 - (A / H)^{2} = (O / H)^{2} .$

step 1.1step 4.2F8algebra

6.1

Step 3.1 and $0 < θ < π / 2$ place $θ$ in $(0, 2)$ , so [F7] gives $\sin θ > 0$ ; step 2.1 gives $O / H > 0$ . These two positive numbers have the same square by step 5.2, and uniqueness in [F1] yields $\sin θ = O / H$ .

step 2.1step 3.1step 4.2step 5.2F1F7

7.1

Since $π > 0$ and $0 < θ < π / 2 < 2 π$ , [F9] applies. Steps 4.2 and 6.1 identify its endpoint as $γ (θ) = (A / H, O / H)$ , so the counterclockwise unit-circle arc from $(1, 0)$ to $(A / H, O / H)$ has radian measure $θ$ .

step 4.2step 6.1F6F9algebra

8.1

The horizontal and vertical legs of the coordinate triangle meet at a right angle at $(A, 0)$ . By step 2.3 their lengths are $A$ and $O$ , while the hypotenuse from $(0, 0)$ to $P$ has length $H$ ; moreover steps 4.2 and 6.1 give $P = H (\cos θ, \sin θ)$ , so $P$ is the positive multiple $H$ of the unit-circle point $γ (θ) = (A / H, O / H)$ at which the arc of step 7.1 ends. The triangle's leg-to-hypotenuse ratios are therefore exactly the two coordinates of $γ (θ)$ : adjacent over hypotenuse is $A / H = \cos θ$ , and opposite over hypotenuse is $O / H = \sin θ$ .

step 2.3step 4.2step 6.1step 7.1algebra

9.1

Therefore the parameter $θ$ of step 4.2 is the unique element of $(0, π / 2)$ with $(A / H, O / H) = (\cos θ, \sin θ)$ , the counterclockwise unit-circle arc from $(1, 0)$ to $(A / H, O / H)$ has radian measure $θ$ , and in the stated coordinate right triangle adjacent over hypotenuse is $A / H = \cos θ$ and opposite over hypotenuse is $O / H = \sin θ$ .

step 5.1step 7.1step 8.1∎

Remarks

The strict hypotheses $A, O > 0$ make the triangle nondegenerate and place $θ$ in the acute range $(0, π / 2)$ . If one of the legs is zero, the normalized point lies on a coordinate axis and the radian definition still supplies the corresponding unit-circle value, but the resulting configuration is not a nondegenerate right triangle; the theorem does not impose an acute-triangle side-ratio convention on those axis or quadrantal cases.

What is measured, and what is not. The library assigns radian measure only to a counterclockwise unit-circle arc starting at $(1, 0)$ (Radian angle by unit-circle arc length); it defines no interior angle of a triangle, and no invariance of an angle under scaling. So the theorem identifies $θ$ as the radian measure of the arc ending at $(A / H, O / H)$ — the unit-circle point of which the hypotenuse vertex $P = H (\cos θ, \sin θ)$ is the positive multiple $H$ — and asserts the two side ratios of the triangle. It does not assert that the triangle's interior angle at the origin equals $θ$ , which would need a notion of angle the library has not built.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

64 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

J. Lebl, Basic Analysis, §11.4.3, The unit circle and polar coordinates (standard reference, not scraped)
OpenStax, Algebra and Trigonometry 2e, §7.2, Right Triangle Trigonometry (standard reference, not scraped)
OpenStax, Algebra and Trigonometry 2e, §7.3, Unit Circle (standard reference, not scraped)