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
- Exact success amplification by attenuating the good branch Algorithm
- Finite truncated tanh–sinh, exp–sinh, and sinh–sinh trapezoid rules Algorithm
- Known-amplitude amplification with integer rounding Algorithm
- 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
- Two-dimensional simple symmetric walk is recurrent Corollary
- x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
- A real-valued optimum is not a fractional Grover iteration Counterexample
- Fidelity and trace-distance inequalities do not imply QRE data processing Counterexample
- I₂(5) admits no crystallographic scaling and no reduced crystallographic root system with that base pairing Counterexample
- 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
- Arcsine-weighted inner product on the Chebyshev interval Definition
- Circular arcs, circumference as arc length, and diameter Definition
- DCT-II and DST-I with fixed even and odd extension conventions Definition
- Standard Cauchy probability law Definition
- The classical Weierstrass function Definition
- The Jacobi theta function θ(t)=∑_n∈ℤ e^-π n² t for t>0 Definition
- The real Coxeter form, its radical, reflections, and form-preserving maps Definition
- Type-I cosine transform for Chebyshev–Lobatto data Definition
- A compactly supported contrast with volume-operator norm greater than two Example
- A cycle and an overlong arm: explicit non-positive witnesses Example
- A moved-space intersection in A₃ that is not the meet Example
- A unit contrast on a small cube lies in the Born regime Example
- A vector with mixed signs is not a root, while every root has a sign Example
- An indefinite Coxeter form: infinite, but not of affine type Example
- B-tilde versus C-tilde: the n=2 coincidence and the duality behind the difference Example
- Chamber faces and their stabilizers in A₂ Example
- Dihedral diagrams I₂(m): Gram determinants, the infinite case, and the low-rank coincidences Example
- Exact Grover rotation for four addresses and one marked item Example
- Extremal length of a rectangle and of a round annulus by hand Example
- 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
- G2 from I2(6): the scaled realization and its twelve roots Example
…and 66 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)