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 takes every value between and
The sum of a real power series is continuous at every point strictly inside its interval of convergence