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.
Cosine has a smallest positive zero, lying strictly between zero and two
Statement
There is a unique with . It is the smallest positive zero of cosine.
Facts & Assumptions
Given: The cosine function.
, , and is strictly decreasing on (Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3).
Power-series sums are continuous on their interval of convergence (The sum of a real power series is continuous at every point strictly inside its interval of convergence).
A continuous real function whose endpoint values bracket zero has a zero between them (Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on takes every value between and ).
Proof
Continuity, , and give some with .
Strict decrease on makes this zero unique and gives for .
No positive number below is a zero, so is the smallest positive zero.
Depends on
- Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3
- Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on $[a,b]$ takes every value between $f(a)$ and $f(b)$
- The sum of a real power series is continuous at every point strictly inside its interval of convergence
Used by
- A uniform limit of smooth functions need not be differentiable anywhere Corollary
- x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
- The topologist's sine curve is connected but not path connected Counterexample
- Pi as twice the smallest positive zero of cosine Definition
- 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 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
- 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
- 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
- Quarter-turn values and shifts by pi/2 and pi Theorem
- Riemann–Lebesgue lemma for continuous functions on a compact interval Theorem
- Under ab>1+3π/2, the classical Weierstrass function is continuous everywhere and differentiable nowhere Theorem
Dependency tree · two levels
25 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)