Actual finite prime-field sets · exact cardinalities · Dyson descent · Constructive arithmetic

Constructive Cauchy–Davenport

∅≠A,B⊆𝔽ₚ ⇒ |A+B|≥min(p,|A|+|B|−1)

Construct genuine finite modular sets and their sumsets, then prove the sharp prime-field inequality by a witnessed cardinality-preserving transform and strict descent.

Open the definition-aware map Read the final theorem See campaign milestone G051

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact certificate

Fully expanded arithmetic

Inspect all 4626 native tactic lines and 255 actual proof prerequisites with every definition fully expanded.

Open the exact edition →

Focused route

Final dependency cone

Start at theorem CD0047 and follow only the lemmas and conservative definitions supporting prime_cauchy_davenport_sumset_bound.

Trace prerequisites →
Zoom between mathematical scales: complete research atlas → research domain → proof family → G051 milestone → theorem and definition dependencies.
Major independently established statements: CD0046 prime_cauchy_davenport_cover_bound · CD0048 prime_cauchy_davenport_sumset_exists · CD0047 prime_cauchy_davenport_sumset_bound.
Independently verified Alpha v34 checked-use theorem family: 72 dependency-curried kernel-checked theorem bodies · 255 proof prerequisites · 18 linked definitions · 33 definition-dependency arrows · 4626 exact tactic lines · first admitted v27 · not Stable. The unchanged intuitionistic kernel and separately compiled Lean verifier independently accept all 1224 bundle nodes; SHA-256 c4711433c92b67d2ebeb30131669c60563c70e0464dafa851d417fb88fb21a6d.
Exact mathematical boundary: Sets are complete characteristic-bit codes with actual finite cardinality witnesses. The proof constructs translations and the sumset; no finite-choice oracle, supplied cardinality conclusion, or unproved polynomial-method premise is used.