Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + claude-opus-5[1m])audited 2026-08-24
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.

Thue's lemma on small nonzero representatives

Statement

Let p be a prime and let a∈Z with p∤a. Then there are nonzero integers r,s with ∣r∣,∣s∣<p and ra≡s(modp).

Facts & Assumptions

Given: A prime p and an integer a with p∤a.

[L1]

Every nonempty finite subset of R has a maximum and a minimum (Every nonempty finite set of reals has a maximum and a minimum).

[L2]

Every nonnegative real t has a unique nonnegative square root t whose square is t (Square roots exist: a unique a≥0 with (a)2=a; the positives are {x2:x≠0}).

[L5]

If a map from a finite set A to a finite set B has ∣A∣>∣B∣, then some fibre contains more than one element (If ∣A∣>k∣B∣ then every f:A→B has a fibre with more than k elements, and for nonempty B some fibre has at least ⌈∣A∣/∣B∣⌉ elements).

[L6]

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

[F1]

The congruence u≡v(modn) means that n∣(u−v) (Congruence modulo an integer: a≡b(modn) when n∣(a−b), including the moduli 0 and 1).

Proof

technique · direct
1.1givenL1construct

The set H:={k∈N:k≤p and k2<p} is finite and contains 0, so [L1] gives its largest element h.

2.1step 1.1L2givenalgebra

One has (h+1)2>p: a strict inequality in the other direction would put h+1 in H, while equality would factor the prime p as (h+1)(h+1) with 1<h+1<p. Also h2<p=(p)2, so h<p by nonnegativity and [L2].

3.1step 2.1L3L4algebra

Put I:={0,1,…,h}. Then [L3] gives ∣I×I∣=(h+1)2>p=∣Z/p∣ by step 2.1 and [L4].

4.1step 3.1L5F1construct

Apply [L5] to (i,j)↦[ia−j]p. Distinct pairs (i,j),(i′,j′)∈I×I have the same image. With r=i−i′ and s=j−j′, this says ra≡s(modp).

5.1step 4.1step 2.1F1L2algebra

The coordinate bounds give ∣r∣,∣s∣≤h<p.

6.1step 5.1L6F1givenalgebra

If r=0, then [F1] gives p∣s; the bound ∣s∣<p<p forces s=0, contrary to distinctness. If s=0, then p∣ra; [L6] and p∤a give p∣r, and the same bound forces r=0, again a contradiction.

7.1step 4.1step 5.1step 6.1∎

Thus the integers r,s from step 4.1 are both nonzero, satisfy ra≡s(modp), and obey the required strict bounds.

Depends on

Used by

Dependency tree · two levels

47 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