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.
Pi as twice the smallest positive zero of cosine
Definition
Let be the unique smallest positive zero of cosine supplied by Cosine has a smallest positive zero, lying strictly between zero and two. Define
Thus and .
Depends on
Used by
- A uniform limit of smooth functions need not be differentiable anywhere Corollary
- exp(x+iy)=eˣ(cos y+i sin y), |exp(x+iy)|=eˣ, and e^iπ+1=0 Corollary
- Pi is the first positive zero of sine Corollary
- The central binomial coefficient is asymptotic to 4ⁿ divided by the square root of pi n Corollary
- The normalized integral around a positively oriented circle centred at a is 1 Corollary
- x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
- The circular curve defeats the equality form of the vector-valued mean value theorem Counterexample
- The continuous path γ(x)=(x,x sin(1/x)) on [0,1], with γ(0)=(0,0), is not rectifiable Counterexample
- The map (z₁,z₂)↦(e^z₁,z₂) has invertible complex Jacobian everywhere and is not injective Counterexample
- The topologist's sine curve is connected but not path connected Counterexample
- The vortex field is closed but not exact on the punctured plane Counterexample
- Volterra's function is differentiable everywhere with bounded derivative, but its derivative is not Riemann integrable Counterexample
- Circular arcs, circumference as arc length, and diameter Definition
- The classical Weierstrass function Definition
- G(x)=x² sin(1/x) has a bounded derivative discontinuous at 0 that is nevertheless Riemann integrable, and Newton–Leibniz evaluates its integral Example
- r² sin(1/r) is differentiable at the origin with a discontinuous gradient Example
- Tangent identifies a bounded incomplete interval with the unbounded complete real line Example
- The arc length of one sine period is 4√2 E(1/√2) Example
- The Bartle-Sherbert bounds 2.828 < pi < 3.185 Example
- The family sin(nx)sin(ny) is uniformly bounded but not equicontinuous Example
- The four Dini derivatives of x sin(1/x) at 0 take two distinct values Example
- The sine harmonics are pointwise bounded but have no uniformly convergent subsequence Example
- The Weierstrass function with a=1/2 and b=15 Example
- x² sin(1/x²) has an unbounded, non-Riemann-integrable derivative Example
- xy sin(1/(x²+y²)) is differentiable at the origin with unbounded partial derivatives nearby Example
- A sector-area squeeze proves lim sin(x)/x=1 without first calibrating angle measure False statement
- False: any positive zero of sine characterizes pi False statement
- False: circumference divided by radius equals pi False statement
- False: every closed C1 field on a connected open set is exact False statement
- FALSE: every continuous function on a compact interval has a rectifiable graph False statement
- FALSE: every pointwise bounded sequence of continuous functions has a uniformly convergent subsequence False statement
- FALSE: spherical coordinates are globally injective False statement
- Low-frequency bound for the Weierstrass difference quotient Lemma
- The topologist's sine curve is connected Lemma
- The Weierstrass tail has one sign and dominates at the probe points Lemma
- Wallis integrals satisfy the two-step recurrence, closed forms, and the adjacent-integral squeeze Lemma
- [t]↦(cos 2π t,sin 2π t) is a homeomorphism from ℝ/ℤ to the unit circle Theorem
- Analytic sine and cosine agree with right-triangle ratios Theorem
- Inscribed regular-polygon perimeters increase to 2 pi, while circumscribed perimeters decrease to 2 pi Theorem
- Pi is equivalently the first sine zero, twice the first cosine zero, and half the least common period Theorem
…and 5 more results.
Dependency tree · two levels
4 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
- NIST Digital Library of Mathematical Functions, Chapter 4 (standard reference, not scraped)
- C. Schmeiser, Introduction to Analysis (standard reference, not scraped)