ExampleConstruction: AI-adaptedVerification: AI-adaptedprecheck 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 first Viete nested-radical products approximate two over pi

Example

Write $a_{1} = \sqrt{2}$ and $a_{n + 1} = \sqrt{2 + a_{n}}$ . The first four finite Viète products are

$P_{1} = \frac{a_{1}}{2}, P_{2} = \frac{a_{1} a_{2}}{2^{2}}, P_{3} = \frac{a_{1} a_{2} a_{3}}{2^{3}}, P_{4} = \frac{a_{1} a_{2} a_{3} a_{4}}{2^{4}} .$

Facts & Assumptions

Given: The positive nested radicals $a_{n}$ and the products $P_{n}$ above.

[L1]

For every real $x$ and natural $n$ , $\sin x = 2^{n} \sin (x / 2^{n}) \prod_{k = 1}^{n} \cos (x / 2^{k}),$ with empty product $1$ at $n = 0$ ; at $x = π / 2$ , its cosine factors are the positive half-angle nested radicals (The finite Viete cosine product and its positive nested-radical factors).

[L2]

These finite products satisfy $P_{n} \to 2 / π$ (Viete's nested-radical product: two over pi is the limit of the finite cosine products).

[L3]

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

Verification

technique · direct

1.1

Starting with $a_{1} = \sqrt{2}$ , the recurrence gives $a_{2} = \sqrt{2 + \sqrt{2}}, a_{3} = \sqrt{2 + \sqrt{2 + \sqrt{2}}}, a_{4} = \sqrt{2 + \sqrt{2 + \sqrt{2 + \sqrt{2}}}} .$

givenalgebra

1.2

Since every $a_{k}$ is positive, each $P_{n} > 0$ , and $Π_{n} : = \frac{2}{P_{n}} = \frac{2^{n + 1}}{a_{1} a_{2} \dots a_{n}}$ is defined.

givenalgebra

2.1

Substitution into $\prod_{k = 1}^{n} (a_{k} / 2)$ gives exactly the four products displayed in the Example, as also identified by [L1].

step 1.1L1algebra

3.1

By [L2] and [L3], the nonzero-limit quotient law gives $Π_{n} \to 2 / (2 / π) = π$ . Thus doubling the reciprocals of the displayed finite products gives certified approximants to $π$ , with convergence supplied by the finite identity rather than a numerical pattern.

step 1.2L2L3algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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

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