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.
Second supplement:
Statement
For every odd prime ,
Equivalently, if and only if or , while if and only if or .
Facts & Assumptions
Given: An odd prime .
If counts the least positive residues of modulo , for , that exceed , then (Gauss's quadratic-residue lemma).
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 ).
Proof
Put . For , the least positive residue of is itself because . It exceeds exactly when , so [L1] counts precisely the integers with .
By [L2], write with . Since is odd, . In these cases the crossing indices of step 1.1 are respectively ; ; ; and . Their counts are , , , and .
For , direct substitution gives , , , and , respectively. These have parity even, odd, odd, and even, exactly matching the four crossing counts in step 2.1.
Fact [L1] and step 3.1 give . The exhaustive remainder cases yield value exactly for residues modulo , and value exactly for residues .
Depends on
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: 72 results over 24 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, Sections D.I and D.IV (standard reference, not scraped)
- W. Stein, Elementary Number Theory, Theorem 4.1.7 (standard reference, not scraped)