Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-sonnet-5)audited 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 two reciprocity lattice counts partition an open rectangle

Statement

Let p and q be distinct odd primes, and let Sp,q and Sq,p be the lower-half lattice counts of Gauss's lemma as a lower-half lattice-point count. Then Sp,q+Sq,p=(p−1)(q−1)/4.

Facts & Assumptions

Given: Distinct odd primes p,q and the integer rectangle R={(x,y):1≤x≤(p−1)/2, 1≤y≤(q−1)/2}.

[L1]

Put Sp,q:=∣{(x,y)∈Z2:1≤x≤(p−1)/2, 0<py<qx}∣ (Gauss's lemma as a lower-half lattice-point count).

[L2]

If a prime p divides a product ab, then p∣a or p∣b (Euclid's lemma: if p is prime and p∣ab then p∣a or p∣b).

Proof

technique · direct
1.1L2given

No point (x,y)∈R lies on the diagonal py=qx: equality would give p∣qx, so [L2] would give p∣q or p∣x; distinctness of the primes rules out the first alternative, while 1≤x≤(p−1)/2<p rules out the second. Thus every point of R satisfies exactly one of py<qx and qx<py.

2.1step 1.1L1algebra∎

The points of R with py<qx are exactly those counted by Sp,q: the inequality itself forces y<q/2, hence y≤(q−1)/2; after interchanging the coordinates and the primes, the points with qx<py are exactly those counted by Sq,p. By step 1.1 these two sets partition R, whose cardinality is ((p−1)/2)((q−1)/2)=(p−1)(q−1)/4.

Depends on

Used by

Dependency tree · two levels

15 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