CD0048

prime_cauchy_davenport_sumset_exists

Construct the actual canonical sumset and its exact cardinality together with the full sharp Cauchy--Davenport bound.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

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.

Exact theorem in conservative defined notation

∀ p. ∀ b. ∀ c. ∀ d. ∀ e. ∀ k. ∀ l. Prime(p) → BitCount(b,c,p,k) → BitCount(d,e,p,l) → ¬k = 0 → ¬l = 0 → ∃ x. ∃ y. ∃ z. BitCount(x,y,p,z) ∧ (ModularSetSum(b,c,d,e,x,y,p) ∧ CauchyDavenportBound(p,k,l,z))

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

ModularSetSum(b,c,d,e,u,v,p) · 2CauchyDavenportBound(p,k,l,m) · 1Prime(p) · 1BitCount(b,c,l,z) · 4

Actual proof prerequisites

prime_nonzero · checked external prerequisitefinite_modular_sumset_existsprime_cauchy_davenport_sumset_bound
Original expanded first-order statement 
forall p b c d e k l. ((~(p = 1) /\ forall frp_prime_left_cd_exist_prime frp_prime_right_cd_exist_prime. p = frp_prime_left_cd_exist_prime * frp_prime_right_cd_exist_prime -> frp_prime_left_cd_exist_prime = 1 \/ frp_prime_right_cd_exist_prime = 1)) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((k)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((k)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_summand. (b) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (c)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (c))) /\ exists ff_q_fms_count_decoded. (b) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (c)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((l)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((l)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_summand. (d) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (e)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (e))) /\ exists ff_q_fms_count_decoded. (d) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (e)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) -> ~(k=0) -> ~(l=0) -> exists sb sc m. (((exists ff_u_fms_count ff_v_fms_count. ((((exists ff_h_fms_count_start. ff_h_fms_count_start + S (0) = S ((S (0)) * ff_v_fms_count)) /\ exists ff_q_fms_count_start. ff_u_fms_count = ff_q_fms_count_start * S ((S (0)) * ff_v_fms_count) + (0))) /\ ((((exists ff_h_fms_count_terminal. ff_h_fms_count_terminal + S ((m)) = S ((S ((p))) * ff_v_fms_count)) /\ exists ff_q_fms_count_terminal. ff_u_fms_count = ff_q_fms_count_terminal * S ((S ((p))) * ff_v_fms_count) + ((m)))) /\ forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_a_fms_count ff_r_fms_count ff_s_fms_count. ((((exists ff_h_fms_count_summand. ff_h_fms_count_summand + S (ff_a_fms_count) = S ((S (ff_i_fms_count)) * (sc))) /\ exists ff_q_fms_count_summand. (sb) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (sc)) + (ff_a_fms_count))) /\ ((((exists ff_h_fms_count_partial. ff_h_fms_count_partial + S (ff_r_fms_count) = S ((S (ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_partial. ff_u_fms_count = ff_q_fms_count_partial * S ((S (ff_i_fms_count)) * ff_v_fms_count) + (ff_r_fms_count))) /\ ((((exists ff_h_fms_count_successor. ff_h_fms_count_successor + S (ff_s_fms_count) = S ((S (S ff_i_fms_count)) * ff_v_fms_count)) /\ exists ff_q_fms_count_successor. ff_u_fms_count = ff_q_fms_count_successor * S ((S (S ff_i_fms_count)) * ff_v_fms_count) + (ff_s_fms_count))) /\ ff_s_fms_count = ff_r_fms_count + ff_a_fms_count)))))) /\ (forall ff_i_fms_count. (exists ff_lt_fms_count_bound. ff_lt_fms_count_bound + S ff_i_fms_count = (p)) -> exists ff_bit_fms_count. ((((exists ff_h_fms_count_decoded. ff_h_fms_count_decoded + S (ff_bit_fms_count) = S ((S (ff_i_fms_count)) * (sc))) /\ exists ff_q_fms_count_decoded. (sb) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (sc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ ((forall fms_s_sumset. (exists fms_gap_sumset_s. fms_gap_sumset_s + S (fms_s_sumset) = (p)) -> ((((((exists fs_h_fms_sumset_result. fs_h_fms_sumset_result + S (1) = S ((S (fms_s_sumset)) * sc)) /\ exists fs_q_fms_sumset_result. sb = fs_q_fms_sumset_result * S ((S (fms_s_sumset)) * sc) + (1))) -> (exists fms_i_sumset fms_j_sumset. ((((exists fms_gap_sumset_left. fms_gap_sumset_left + S (fms_i_sumset) = (p)) /\ (((exists fs_h_fms_sumset_left. fs_h_fms_sumset_left + S (1) = S ((S (fms_i_sumset)) * c)) /\ exists fs_q_fms_sumset_left. b = fs_q_fms_sumset_left * S ((S (fms_i_sumset)) * c) + (1))))) /\ ((((exists fms_gap_sumset_right. fms_gap_sumset_right + S (fms_j_sumset) = (p)) /\ (((exists fs_h_fms_sumset_right. fs_h_fms_sumset_right + S (1) = S ((S (fms_j_sumset)) * e)) /\ exists fs_q_fms_sumset_right. d = fs_q_fms_sumset_right * S ((S (fms_j_sumset)) * e) + (1))))) /\ (exists fms_u_sumset fms_v_sumset. (fms_i_sumset + fms_j_sumset) + (p) * fms_u_sumset = (fms_s_sumset) + (p) * fms_v_sumset))))) /\ ((exists fms_i_sumset fms_j_sumset. ((((exists fms_gap_sumset_left. fms_gap_sumset_left + S (fms_i_sumset) = (p)) /\ (((exists fs_h_fms_sumset_left. fs_h_fms_sumset_left + S (1) = S ((S (fms_i_sumset)) * c)) /\ exists fs_q_fms_sumset_left. b = fs_q_fms_sumset_left * S ((S (fms_i_sumset)) * c) + (1))))) /\ ((((exists fms_gap_sumset_right. fms_gap_sumset_right + S (fms_j_sumset) = (p)) /\ (((exists fs_h_fms_sumset_right. fs_h_fms_sumset_right + S (1) = S ((S (fms_j_sumset)) * e)) /\ exists fs_q_fms_sumset_right. d = fs_q_fms_sumset_right * S ((S (fms_j_sumset)) * e) + (1))))) /\ (exists fms_u_sumset fms_v_sumset. (fms_i_sumset + fms_j_sumset) + (p) * fms_u_sumset = (fms_s_sumset) + (p) * fms_v_sumset)))) -> (((exists fs_h_fms_sumset_result. fs_h_fms_sumset_result + S (1) = S ((S (fms_s_sumset)) * sc)) /\ exists fs_q_fms_sumset_result. sb = fs_q_fms_sumset_result * S ((S (fms_s_sumset)) * sc) + (1))))))) /\ (((exists fms_gap_cd_bound_full. fms_gap_cd_bound_full + (p) = (m)) \/ (exists fms_gap_cd_bound_sum. fms_gap_cd_bound_sum + (k+l) = (S (m))))))

Complete tactic proof in conservative notation

All 57 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

57 script commands · 11 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

Named ingredients (2)
finite modular sumset existsprime cauchy davenport sumset bound
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro k
  7. L7
    intro l
  8. L8
    intro hprime
  9. L9
    intro hA
  10. L10
    intro hB
02Fix variables and assumptionsL11–12

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hk
  2. L12
    intro hl
03Establish hsumL13–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular sumset exists.

  1. L13
    have hsum : ∃ sb. ∃ sc. ∃ m. BitCount(sb,sc,p,m) ∧ ModularSetSum(b,c,d,e,sb,sc,p)Definitions: BitCount(sb,sc,p,m)ModularSetSum(b,c,d,e,sb,sc,p)Original native command in the exact edition
  2. L14
    specialize finite_modular_sumset_exists b
  3. L15
    specialize finite_modular_sumset_exists c
  4. L16
    specialize finite_modular_sumset_exists d
  5. L17
    specialize finite_modular_sumset_exists e
  6. L18
    specialize finite_modular_sumset_exists p
  7. L19
    specialize finite_modular_sumset_exists k
  8. L20
    specialize finite_modular_sumset_exists l
  9. L21
    apply finite_modular_sumset_exists
  10. L22
    intro he
04Use earlier factsL23–28

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L23
    specialize prime_nonzero p
  2. L24
    apply prime_nonzero
  3. L25
    exact hprime
  4. L26
    exact he
  5. L27
    exact hA
  6. L28
    exact hB
05Separate the logical casesL29–32

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L29
    cases hsum
  2. L30
    cases hsum_witness
  3. L31
    cases hsum_witness_witness
  4. L32
    cases hsum_witness_witness_witness
06Construct an explicit witnessL33–35

Supply the displayed value, then prove that it has the required property.

  1. L33
    exists x
  2. L34
    exists x1
  3. L35
    exists x2
07Separate the logical casesL36–36

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L36
    split
08Use earlier factsL37–37

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L37
    exact hsum_witness_witness_witness_left
09Separate the logical casesL38–38

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L38
    split
10Use earlier factsL39–48

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L39
    exact hsum_witness_witness_witness_right
  2. L40
    specialize prime_cauchy_davenport_sumset_bound p
  3. L41
    specialize prime_cauchy_davenport_sumset_bound b
  4. L42
    specialize prime_cauchy_davenport_sumset_bound c
  5. L43
    specialize prime_cauchy_davenport_sumset_bound d
  6. L44
    specialize prime_cauchy_davenport_sumset_bound e
  7. L45
    specialize prime_cauchy_davenport_sumset_bound x
  8. L46
    specialize prime_cauchy_davenport_sumset_bound x1
  9. L47
    specialize prime_cauchy_davenport_sumset_bound k
  10. L48
    specialize prime_cauchy_davenport_sumset_bound l
11Use earlier factsL49–57

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L49
    specialize prime_cauchy_davenport_sumset_bound x2
  2. L50
    apply prime_cauchy_davenport_sumset_bound
  3. L51
    exact hprime
  4. L52
    exact hA
  5. L53
    exact hB
  6. L54
    exact hsum_witness_witness_witness_left
  7. L55
    exact hk
  8. L56
    exact hl
  9. L57
    exact hsum_witness_witness_witness_right

Library-wide reading audit

Original defined command ledger · 57 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro k
  7. 0007intro l
  8. 0008intro hprime
  9. 0009intro hA
  10. 0010intro hB
  11. 0011intro hk
  12. 0012intro hl
  13. 0013have hsum : ∃ sb. ∃ sc. ∃ m. BitCount(sb,sc,p,m) ∧ ModularSetSum(b,c,d,e,sb,sc,p)
  14. 0014specialize finite_modular_sumset_exists b
  15. 0015specialize finite_modular_sumset_exists c
  16. 0016specialize finite_modular_sumset_exists d
  17. 0017specialize finite_modular_sumset_exists e
  18. 0018specialize finite_modular_sumset_exists p
  19. 0019specialize finite_modular_sumset_exists k
  20. 0020specialize finite_modular_sumset_exists l
  21. 0021apply finite_modular_sumset_exists
  22. 0022intro he
  23. 0023specialize prime_nonzero p
  24. 0024apply prime_nonzero
  25. 0025exact hprime
  26. 0026exact he
  27. 0027exact hA
  28. 0028exact hB
  29. 0029cases hsum
  30. 0030cases hsum_witness
  31. 0031cases hsum_witness_witness
  32. 0032cases hsum_witness_witness_witness
  33. 0033exists x
  34. 0034exists x1
  35. 0035exists x2
  36. 0036split
  37. 0037exact hsum_witness_witness_witness_left
  38. 0038split
  39. 0039exact hsum_witness_witness_witness_right
  40. 0040specialize prime_cauchy_davenport_sumset_bound p
  41. 0041specialize prime_cauchy_davenport_sumset_bound b
  42. 0042specialize prime_cauchy_davenport_sumset_bound c
  43. 0043specialize prime_cauchy_davenport_sumset_bound d
  44. 0044specialize prime_cauchy_davenport_sumset_bound e
  45. 0045specialize prime_cauchy_davenport_sumset_bound x
  46. 0046specialize prime_cauchy_davenport_sumset_bound x1
  47. 0047specialize prime_cauchy_davenport_sumset_bound k
  48. 0048specialize prime_cauchy_davenport_sumset_bound l
  49. 0049specialize prime_cauchy_davenport_sumset_bound x2
  50. 0050apply prime_cauchy_davenport_sumset_bound
  51. 0051exact hprime
  52. 0052exact hA
  53. 0053exact hB
  54. 0054exact hsum_witness_witness_witness_left
  55. 0055exact hk
  56. 0056exact hl
  57. 0057exact hsum_witness_witness_witness_right