LemmaStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-13

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.

The finite Viete cosine product and its positive nested-radical factors

Statement

For every real $x$ and natural $n$ ,

$\sin x = 2^{n} \sin (x / 2^{n}) \prod_{k = 1}^{n} \cos (x / 2^{k}),$

with the product equal to $1$ when $n = 0$ . At $x = π / 2$ , all factors are positive and

$\cos (π / 4) = \frac{\sqrt{2}}{2}, \cos (π / 8) = \frac{\sqrt{2 + \sqrt{2}}}{2},$

with each later factor obtained by placing the previous positive radical inside $\sqrt{2 + \cdot} / 2$ .

Facts & Assumptions

Given: A real $x$ and a natural $n$ .

[L1]

For all real $x, y$ , $\sin (x + y) = \sin x \cos y + \cos x \sin y$ and $\cos (x + y) = \cos x \cos y - \sin x \sin y$ ; moreover, $\sin^{2} x + \cos^{2} x = 1$ for every real $x$ (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).

[L2]

$\sin (π / 2) = 1$ , and cosine is positive on $(0, π / 2)$ (Quarter-turn values and shifts by pi/2 and pi, Signs, monotonicity intervals, and ranges of sine and cosine).

[L3]

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

[L4]

A finite product in a monoid has empty product equal to the identity and is extended by adjoining its last factor (The product $g_{0} g_{1} \dots g_{n - 1}$ of a finite list in a monoid, by recursion, with the empty product ( $n = 0$ ) equal to the identity).

Proof

technique · induction

1.1

At $n = 0$ , the right side is $2^{0} \sin x$ times the empty product, hence equals $\sin x$ by [L4].

baseL4algebra

1.2

Assume the finite identity at $n$ . Put $x = y = u / 2$ in the sine addition formula of [L1] to obtain $\sin u = 2 \sin (u / 2) \cos (u / 2)$ . Apply this with $u = x / 2^{n}$ and adjoin the factor $\cos (x / 2^{n + 1})$ using [L4]; this gives the identity at $n + 1$ .

ihL1L4algebra

1.3

At $x = π / 2$ , every angle $π / 2^{k + 1}$ lies in $(0, π / 2)$ , so [L2] makes every factor positive. Put $x = y = u / 2$ in the cosine addition formula of [L1] and use the Pythagorean identity there to obtain $\cos u = 2 \cos^{2} (u / 2) - 1$ . Thus $\cos (u / 2) = \frac{\sqrt{2 + 2 \cos u}}{2},$ where [L3] selects the positive square root.

L1L2L3algebra

2.1

By induction, the finite identity holds for every natural $n$ .

step 1.1step 1.2

3.1

Starting with $\cos (π / 2) = 0$ in [L2] and iterating step 1.3 gives $\cos (π / 4) = \sqrt{2} / 2$ , $\cos (π / 8) = \sqrt{2 + \sqrt{2}} / 2$ , and all subsequent positive nested-radical factors stated above.

step 2.1step 1.3L2L3discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 73 results over 24 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources

Imperial College London, History of Mathematics, Problems VI solutions (standard reference, not scraped)