TheoremStatement: 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.

Viete's nested-radical product: two over pi is the limit of the finite cosine products

Statement

Let

$P_{n} : = \prod_{k = 1}^{n} \cos (π / 2^{k + 1}), P_{0} : = 1.$

Then $P_{n} \to 2 / π$ . Equivalently, substituting the positive half-angle radicals from The finite Viete cosine product and its positive nested-radical factors,

$\frac{2}{π} = \frac{\sqrt{2}}{2} \cdot \frac{\sqrt{2 + \sqrt{2}}}{2} \cdot \frac{\sqrt{2 + \sqrt{2 + \sqrt{2}}}}{2} \dots,$

where the infinite product means the limit of its finite products.

Facts & Assumptions

Given: The finite products $P_{n}$ .

[L1]

For every $x$ and natural $n$ , $\sin x = 2^{n} \sin (x / 2^{n}) \prod_{k = 1}^{n} \cos (x / 2^{k})$ , and at $x = π / 2$ the factors have the stated positive nested-radical forms (The finite Viete cosine product and its positive nested-radical factors).

[L2]

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

[L3]

Products and quotients of convergent real sequences have the corresponding limits when the limiting denominator is nonzero (Algebra of limits: sums, scalar multiples, products and quotients).

[L4]

A finite product in a monoid has empty product equal to the identity (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).

[L5]

For every $ε > 0$ there is a natural $N \geq 1$ with $1 / N < ε$ , and $π > 0$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ , Pi as twice the smallest positive zero of cosine).

Proof

technique · direct

1.1

Apply [L1] with $x = π / 2$ and replace its index $n$ by $n + 1$ : $1 = 2^{n + 1} \sin (π / 2^{n + 2}) P_{n + 1} .$

L1algebra

2.1

Put $y_{n} : = π / 2^{n + 2}$ . Then $y_{n} > 0$ by [L5]. Since $2^{n + 2} \geq n + 1$ , [L5] gives $0 < y_{n} \leq π / (n + 1) \to 0$ , while $2^{n + 1} y_{n} = π / 2$ . Thus step 1.1 becomes $1 = \frac{π}{2} \frac{\sin y_{n}}{y_{n}} P_{n + 1} .$

step 1.1L5algebra

3.1

Every factor of $P_{n + 1}$ is positive by [L1], so division is legitimate. By [L2] and [L3], step 2.1 gives $P_{n + 1} \to 2 / π$ , hence also $P_{n} \to 2 / π$ .

step 2.1L1L2L3

4.1

The case $n = 0$ is the finite empty product $P_{0} = 1$ by [L4]; it is not an extra factor in the limit. Substituting the radical factors from [L1] into step 3.1 gives the displayed Viète product.

step 3.1L1L4∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 97 results over 30 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)