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.
Quarter-turn values and shifts by pi/2 and pi
Statement
For every real , In particular,
Facts & Assumptions
Given: A real and .
The addition formulas and Pythagorean identity hold (The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine).
Proof
From , , and , one gets .
Substituting into the addition formulas gives and .
Applying step 2.1 twice gives the shifts by and the listed special values.
Depends on
- Pi as twice the smallest positive zero of cosine
- Cosine has a smallest positive zero, lying strictly between zero and two
- The addition formulas for sine and cosine
- Parity and the Pythagorean identity for sine and cosine
- Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3
Used by
- Buffered certified rational phase approximation Algorithm
- Exact success amplification by attenuating the good branch Algorithm
- Known-amplitude amplification with integer rounding Algorithm
- Periodic Fourier collocation differentiation matrix Algorithm
- Szegedy-walk marked-set detection Algorithm
- 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 normal component of the curl is the limiting circulation per unit area of shrinking discs Corollary
- x sin(1/x) extended by zero is continuous but not differentiable at zero Corollary
- A fixed Grover iteration count can fail when a is unknown Counterexample
- A map with two preimages but degree zero Counterexample
- A real-valued optimum is not a fractional Grover iteration Counterexample
- A surjective map need not be a fibration Counterexample
- Agreement accumulating only at the boundary does not force a holomorphic identity Counterexample
- An invertible derivative at one point does not give a local inverse without C¹ regularity Counterexample
- Antipodal points on a round sphere have many minimizing geodesics Counterexample
- f(x+iy)=eˣ(cos 2y+i sin 2y) is continuous, satisfies f(z+w)=f(z)f(w) and f(1)=e, but is not the standard complex exponential Counterexample
- Fidelity and trace-distance inequalities do not imply QRE data processing Counterexample
- Generator convention matters Counterexample
- High frequencies destroy uniform translation control Counterexample
- I₂(5) admits no crystallographic scaling and no reduced crystallographic root system with that base pairing Counterexample
- Principal arcsine has no finite derivative at -1 or 1 Counterexample
- Sharp frequency cutoffs have kernels that are not in L1 Counterexample
- sin(1/x) has no limit as x tends to zero Counterexample
- sin(3π/2)=-1 shows that the positive square root is not an unconditional half-angle formula Counterexample
- The continuous path γ(x)=(x,x sin(1/x)) on [0,1], with γ(0)=(0,0), is not rectifiable Counterexample
- The final-time face is not part of the parabolic boundary Counterexample
- The topologist's sine curve is connected but not path connected Counterexample
- u=v=π/4 shows that the tangent addition formula cannot omit its domain restrictions Counterexample
- Volterra's function is differentiable everywhere with bounded derivative, but its derivative is not Riemann integrable Counterexample
- Best uniform polynomial error and Chebyshev interpolation operators Definition
- Periodic Fourier collocation grid and even-grid Nyquist convention Definition
- Principal inverse sine and inverse cosine Definition
- The Coxeter nerve and its Moussong metric Definition
- The real Coxeter form, its radical, reflections, and form-preserving maps Definition
- A closed cylinder as a finitely patched oriented surface Example
- A continuous argument computed along a spiralling contour Example
- A cycle and an overlong arm: explicit non-positive witnesses Example
- A four-dimensional product exactly integrated on a sparse node union Example
- A moved-space intersection in A₃ that is not the meet Example
…and 155 more results.
Dependency tree · two levels
16 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)