TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

Cauchy–Davenport: for $p$ prime and nonempty $A, B \subseteq Z / p$ , $∣ A + B ∣ \geq \min {p, ∣ A ∣ + ∣ B ∣ - 1}$

Statement

Let $p$ be prime and let $A, B \subseteq Z / p$ be nonempty. Then

$∣ A + B ∣ \geq \min {p, ∣ A ∣ + ∣ B ∣ - 1} .$

Facts & Assumptions

Given: a prime number $p$ and nonempty subsets $A, B \subseteq Z / p$ .

[F1]

The quotient ring $Z / p$ is a field when $p$ is prime (For every prime $p$ , the two operations on $Z / p$ make it a field, The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[L1]

Over a field, if $\deg f = t_{1} + t_{2}$ , the coefficient of $x^{t_{1}} y^{t_{2}}$ is nonzero, and $∣ S_{i} ∣ > t_{i}$ , then $f$ is nonzero at some point of $S_{1} \times S_{2}$ (Alon's Combinatorial Nullstellensatz: if $\deg f = \sum_{i} t_{i}$ , the coefficient of $x_{1}^{t_{1}} \dots x_{n}^{t_{n}}$ in $f$ is nonzero, and $∣ S_{i} ∣ > t_{i}$ , then $f (s_{1}, \dots, s_{n}) \neq 0$ for some $s_{i} \in S_{i}$ ).

[L2]

If $0 \leq k \leq m < p$ , then $p ∤ (\binom{m}{k})$ (If $p$ is prime and $0 \leq k \leq m < p$ then $p ∤ (\binom{m}{k})$ ).

Proof

technique · direct

1.1

If $∣ A ∣ + ∣ B ∣ - 1 > p$ , then the claimed lower bound is $p$ . In that case every class $c \in Z / p$ has a representation $c = a + b$ with $a \in A$ and $b \in B$ : otherwise the translate $c - B$ would be disjoint from $A$ , so the two subsets $A$ and $c - B$ of the $p$ -element set $Z / p$ would have total size at most $p$ , contradicting $∣ A ∣ + ∣ B ∣ > p$ . Hence $A + B = Z / p$ and the theorem holds.

given

1.2

Now assume $∣ A ∣ + ∣ B ∣ - 1 \leq p$ , and suppose toward contradiction that $∣ A + B ∣ \leq ∣ A ∣ + ∣ B ∣ - 2$ . Choose a set $C \subseteq Z / p$ with $A + B \subseteq C$ and $∣ C ∣ = ∣ A ∣ + ∣ B ∣ - 2$ , and consider the polynomial $f (x, y) : = \prod_{c \in C} (x + y - c) \in (Z / p) [x, y] .$

F1assume-contra

2.1

The total degree of $f$ is $∣ C ∣ = t_{1} + t_{2}$ with $t_{1} = ∣ A ∣ - 1$ and $t_{2} = ∣ B ∣ - 1$ . The coefficient of $x^{t_{1}} y^{t_{2}}$ is $(\binom{∣ A ∣ + ∣ B ∣ - 2}{∣ A ∣ - 1})$ , and this is nonzero in $Z / p$ by [L2] because the top is below $p$ .

L2step 1.2

3.1

The polynomial $f$ vanishes at every point of $A \times B$ , because $a + b \in A + B \subseteq C$ for every $a \in A$ and $b \in B$ . But [L1] and step 2.1 say that no polynomial with these degree data and this nonzero top coefficient can vanish on all of $A \times B$ . This contradiction proves the theorem.

L1step 1.2step 2.1discharge-contradiction∎

Remarks

Primality is load-bearing twice: it makes $Z / p$ a field, and it keeps the critical binomial coefficient nonzero there.

Depends on

Used by

Dependency tree · two levels

59 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

N. Alon, Combinatorial Nullstellensatz, Theorem 3.2 (standard reference, not scraped)
O. Pikhurko, An Introduction to Combinatorics, §11.1 (standard reference, not scraped)

Cauchy–Davenport: for pp prime and nonempty A,B⊆Z/pA,B⊆Z/p, ∣A+B∣≥min⁡{p,∣A∣+∣B∣−1}∣A+B∣≥min{p,∣A∣+∣B∣−1}