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.
First supplement:
Statement
For every odd prime ,
Equivalently, if and only if , while if and only if .
Facts & Assumptions
Given: An odd prime .
Euler's criterion gives for every integer (Euler's criterion: ).
Division by a positive integer has a unique quotient and remainder in the standard range (Division with remainder in : for and there are unique with and ).
The congruence means that divides (Congruence modulo an integer: when , including the moduli and ).
For an odd prime , when and is a quadratic residue modulo , and when and is a quadratic nonresidue modulo (The Legendre symbol, including its zero value).
Proof
Substitute in [L1]. An odd prime never divides , so [L4] gives , and is likewise or ; two such integers differ by at most , so their congruence modulo the odd prime is equality: .
By [L2], write with . Since is odd, is or . If , then is even; if , then is odd.
By [L3], the two remainder cases in step 1.2 are exactly and . Combining their parities with step 1.1 proves both biconditionals.
Depends on
- Euler's criterion: $(a/p)\equiv a^{(p-1)/2}\pmod p$
- Congruence modulo an integer: $a\equiv b\pmod n$ when $n\mid(a-b)$, including the moduli $0$ and $1$
- Division with remainder in $\mathbb{Z}$: for $a \in \mathbb{Z}$ and $b > 0$ there are unique $q, r \in \mathbb{Z}$ with $a = qb + r$ and $0 \le r < b$
- The Legendre symbol, including its zero value
Used by
Nothing in the library uses this result yet.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 85 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- H. Hackman, Elementary Number Theory, Chapter D, Section D.I (standard reference, not scraped)
- W. Stein, Elementary Number Theory, Theorem 4.1.7 (standard reference, not scraped)
- A. Gorodnik, Number Theory, Lecture 9, Theorem 1.6 (standard reference, not scraped)