Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] New in the AFP: Vosper's Theorem and the Cauch...

Email Gateway (Jun 12 2026 at 10:12):

From: Manuel Eberl <manuel@pruvisto.org>

Vosper's Theorem and the Cauchy–Davenport Theorem via the Polynomial Method

by Arthur Freitas Ramos, David Barros Hulak and Ruy Jose Guerra Barretto
de Queiroz

This entry formalizes the Cauchy–Davenport lower bound and Vosper's
theorem for sumsets over finite fields of prime cardinality. It combines
a polynomial-method proof of Cauchy–Davenport with a Davenport-transform
proof of Vosper's classification of the nontrivial equality case, and it
provides modular-representative lemmas connecting the abstract
prime-field results to normalized representatives of ℤ/pℤ. AI assistance
was used for proof engineering. The final definitions, statements, and
proofs are checked by Isabelle.

https://isa-afp.org/entries/Cauchy_Davenport_Vosper.html

Enjoy,

Manuel

Last updated: Jul 02 2026 at 07:34 UTC