Alphabeta Math
PropositionStatement: AI-adaptedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-17
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 a and odd positive integer n, 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 {1,0,1}. The Jacobi symbol depends only on a(modn), and it is zero exactly when gcd(a,n)>1. At n=1 it has the value 1.

Facts & Assumptions

Given: An integer a and an odd positive integer n.

[L1]

For odd n1 with canonical prime factorisation n=i<rpiei, define (an):=i<r(api)ei (The Jacobi symbol, with its zero value and empty-product convention).

[L3]

For every odd prime p, the Legendre symbol belongs to {1,0,1}, depends only on the numerator modulo p, and equals zero exactly when p divides the numerator (The Legendre symbol is well defined on residue classes).

Proof

technique · direct
1.1

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 {1,0,1} by [L3], so their product does too, and at n=1 the empty product is 1.

L1L2L3algebra
2.1

If ab(modn), then ab(modp) for every prime factor p of n, so [L3] makes every corresponding factor in [L1] equal. The product is zero exactly when some prime factor p of n divides a, which gives gcd(a,n)>1; conversely, if gcd(a,n)>1, [L4] supplies a prime divisor of the gcd, hence a prime factor of n dividing a, and [L3] makes that Legendre factor zero.

step 1.1L1L3L4algebra

Depends on

Used by

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