Alphabeta MathHow 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 zero, period, arc-length, polygonal, area, circumference, series, and product characterizations all give the same pi
Statement
The constant defined as twice the least positive cosine zero is also:
- the least positive sine zero;
- half the least positive common period of sine and cosine;
- the length of a unit semicircle;
- half the common limit of regular inscribed and circumscribed unit-circle perimeters;
- the Riemann area of the unit disc;
- for every circle of radius ;
- four times the Gregory-Leibniz series sum;
- twice the Wallis-product limit;
- twice the reciprocal of the Viète-product limit.
Facts & Assumptions
Given: The constant of the statement.
The zero and least-common-period conditions are equivalent characterizations of (Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period).
A once-traversed unit semicircle has length (The arc length of a unit semicircle is pi).
Every positive-radius circle has circumference and circumference-to-diameter ratio (Every circle has circumference 2 pi r and circumference-to-diameter ratio pi).
Regular inscribed and circumscribed unit-circle perimeters both tend to (Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi).
The unit disc has Riemann area (A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi).
The Gregory-Leibniz series converges to (The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...).
The finite Wallis products converge to (Wallis's product: pi over two is the limit of the finite Wallis products).
The finite Viète products converge to (Viete's nested-radical product: two over pi is the limit of the finite cosine products).
Proof
Claims 1 and 2 are [L1].
Claim 3 is [L2], and claim 6 is [L3].
Claim 4 follows from [L4] by dividing the common limit by , and claim 5 is [L5].
Claim 7 follows from [L6] by multiplying by , and claim 8 follows from [L7] by multiplying by .
By [L8], the Viète-product limit is , so twice its reciprocal is , which is claim 9.
Every listed value is therefore equal to the originally defined constant ; no one of these equalities was used to define another.
Depends on
- Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period
- The arc length of a unit semicircle is pi
- Every circle has circumference 2 pi r and circumference-to-diameter ratio pi
- Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi
- A disc of radius r has Riemann area pi r squared; in particular the unit disc has area pi
- The Gregory-Leibniz series: pi over four equals 1-1/3+1/5-1/7+...
- Wallis's product: pi over two is the limit of the finite Wallis products
- Viete's nested-radical product: two over pi is the limit of the finite cosine products
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 145 results over 27 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
- J. Lebl, Basic Analysis II, section 11.4 (standard reference, not scraped)
- D. Galvin, Primitives and techniques of integration, section 13.2 (standard reference, not scraped)