ND0137

CauchyDavenportBound(p,k,l,m)

The exact subtraction-free sharp bound: p≤m or k+l≤m+1, equivalent to m≥min(p,k+l−1) for positive input cardinalities.

Conservative notation; not a theorem, primitive, or axiom.

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.

Definition in prerequisite notation

Le(p,m) ∨ Le(k + l,S m)

Only definitions earlier in this acyclic notation graph are used here.

Hygienic expanded first-order definition 
((exists fms_gap_cd_secondwave_full. fms_gap_cd_secondwave_full + (p) = (m)) \/ (exists fms_gap_cd_secondwave_sum. fms_gap_cd_secondwave_sum + (k+l) = (S (m))))

The unchanged native kernel never receives this surface symbol. Binder-safe expansion produces only its existing first-order syntax.

Direct definition dependencies

Le(a,b)

Definitions depending on this notation

none

Checked theorems using this definition

CD0040 · finite_modular_singleton_cover_boundCD0042 · prime_cauchy_davenport_normalized_bounded_inductionCD0043 · prime_cauchy_davenport_normalized_cover_boundCD0046 · prime_cauchy_davenport_cover_boundCD0047 · prime_cauchy_davenport_sumset_boundCD0048 · prime_cauchy_davenport_sumset_exists