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.
The Jacobi symbol is well defined on numerator residue classes
Statement
For every integer and odd positive integer , the product in The Jacobi symbol, with its zero value and empty-product convention is independent of the ordering used to list the canonical prime factors and belongs to . The Jacobi symbol depends only on , and it is zero exactly when . At it has the value .
Facts & Assumptions
Given: An integer and an odd positive integer .
For odd with canonical prime factorisation , define (The Jacobi symbol, with its zero value and empty-product convention).
In a prime factorisation of a positive integer, the exponents are determined by the integer; primes outside the factor list have exponent zero (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
For every odd prime , the Legendre symbol belongs to , depends only on the numerator modulo , and equals zero exactly when divides the numerator (The Legendre symbol is well defined on residue classes).
Every integer greater than has a prime divisor (Every integer has a prime divisor; indeed the least divisor of that exceeds is prime).
Proof
The uniqueness in [L2] fixes the set of prime factors and every exponent in [L1]; changing their order does not change a finite product of integers. Each factor belongs to by [L3], so their product does too, and at the empty product is .
If , then for every prime factor of , so [L3] makes every corresponding factor in [L1] equal. The product is zero exactly when some prime factor of divides , which gives ; conversely, if , [L4] supplies a prime divisor of the gcd, hence a prime factor of dividing , and [L3] makes that Legendre factor zero.
Depends on
- The Jacobi symbol, with its zero value and empty-product convention
- For $n \ge 1$ and any injective list $p : r \to \mathbb{Z}$ of primes containing every prime divisor of $n$, one has $n = \prod_{i<r} p_i^{\,v_{p_i}(n)}$; the exponents are determined by $n$, and $v_q(n) = 0$ for every prime $q$ outside the list
- The Legendre symbol is well defined on residue classes
- Every integer $n > 1$ has a prime divisor; indeed the least divisor of $n$ that exceeds $1$ is prime
Used by
- For fixed odd modulus, the Jacobi symbol is a homomorphism on the unit group Proposition
- The Euclidean algorithm computes the Jacobi symbol without factoring the denominator Theorem
Cited to discharge well-definedness by The Jacobi symbol, with its zero value and empty-product convention.
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 89 results over 26 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
- A. Gorodnik, Number Theory, Lecture 10, §1 (standard reference, not scraped)
- V. Shoup, A Computational Introduction to Number Theory and Algebra, 2nd ed., §12.2 (standard reference, not scraped)