CD0046

prime_cauchy_davenport_cover_bound

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Full Cauchy--Davenport for arbitrary nonempty prime-field characteristic sets, against every actual coded upper sumset.

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 expanded first-order arithmetic statement

forall p b c d e sb sc k l m. ((~(p = 1) /\ forall frp_prime_left_cd_full_prime frp_prime_right_cd_full_prime. p = frp_prime_left_cd_full_prime * frp_prime_right_cd_full_prime -> frp_prime_left_cd_full_prime = 1 \/ frp_prime_right_cd_full_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))))) -> (((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))))) -> ~(k=0) -> ~(l=0) -> (forall fms_i_cover fms_j_cover fms_s_cover. (exists fms_gap_cover_i. fms_gap_cover_i + S (fms_i_cover) = (p)) -> (exists fms_gap_cover_j. fms_gap_cover_j + S (fms_j_cover) = (p)) -> (exists fms_gap_cover_s. fms_gap_cover_s + S (fms_s_cover) = (p)) -> (((exists fs_h_fms_cover_left. fs_h_fms_cover_left + S (1) = S ((S (fms_i_cover)) * c)) /\ exists fs_q_fms_cover_left. b = fs_q_fms_cover_left * S ((S (fms_i_cover)) * c) + (1))) -> (((exists fs_h_fms_cover_right. fs_h_fms_cover_right + S (1) = S ((S (fms_j_cover)) * e)) /\ exists fs_q_fms_cover_right. d = fs_q_fms_cover_right * S ((S (fms_j_cover)) * e) + (1))) -> (exists fms_u_cover fms_v_cover. (fms_i_cover + fms_j_cover) + (p) * fms_u_cover = (fms_s_cover) + (p) * fms_v_cover) -> (((exists fs_h_fms_cover_result. fs_h_fms_cover_result + S (1) = S ((S (fms_s_cover)) * sc)) /\ exists fs_q_fms_cover_result. sb = fs_q_fms_cover_result * S ((S (fms_s_cover)) * 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)))))

Constructive proof overview

Generated structural guide

Full Cauchy--Davenport for arbitrary nonempty prime-field characteristic sets, against every actual coded upper sumset.

The unchanged tactic script uses 7 declared prerequisites and contains 108 exact native proof lines.

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

Proof neighborhood

Direct dependencies

prime_nonzero Stable theorem; checked-use authorized CD0003 finite_bit_count_positive_member CD0025 finite_modular_additive_complement CD0022 finite_modular_set_pullback_exists CD0043 prime_cauchy_davenport_normalized_cover_bound CD0044 finite_modular_pullback_zero_member CD0045 finite_modular_opposite_translates_sum_cover

Direct dependents

CD0047 prime_cauchy_davenport_sumset_bound

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

108 script commands · 18 reading checkpoints · 5 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.

Named ingredients (6)
finite bit count positive memberfinite modular additive complementfinite modular set pullback existsprime cauchy davenport normalized cover boundfinite modular pullback zero memberfinite modular opposite translates sum cover

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

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 sb
  7. L7
    intro sc
  8. L8
    intro k
  9. L9
    intro l
  10. L10
    intro m
02Fix variables and assumptionsL11–17

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

  1. L11
    intro hprime
  2. L12
    intro hA
  3. L13
    intro hB
  4. L14
    intro hS
  5. L15
    intro hk
  6. L16
    intro hl
  7. L17
    intro hcover
03Establish hpzeroL18–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime nonzero.

  1. L18
    have hpzero : ~(p=0)
  2. L19
    intro he
  3. L20
    specialize prime_nonzero p
  4. L21
    apply prime_nonzero
  5. L22
    exact hprime
  6. L23
    exact he
04Establish hmemberL24–31

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite bit count positive member.

  1. L24
    have hmember : exists t. ((exists fms_gap_member. fms_gap_member + S (t) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (t)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (t)) * e) + (1))))
  2. L25
    specialize finite_bit_count_positive_member d
  3. L26
    specialize finite_bit_count_positive_member e
  4. L27
    specialize finite_bit_count_positive_member p
  5. L28
    specialize finite_bit_count_positive_member l
  6. L29
    apply finite_bit_count_positive_member
  7. L30
    exact hB
  8. L31
    exact hl
05Separate the logical casesL32–32

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

  1. L32
    cases hmember
06Establish hcompL33–36

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

  1. L33
    have hcomp : exists v. x+v=p
  2. L34
    specialize finite_modular_additive_complement p
  3. L35
    specialize finite_modular_additive_complement x
  4. L36
    apply finite_modular_additive_complement
07Separate the logical casesL37–37

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

  1. L37
    cases hmember_witness
08Use earlier factsL38–38

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

  1. L38
    exact hmember_witness_left
09Separate the logical casesL39–39

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

  1. L39
    cases hcomp
10Establish hAnormL40–48

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

  1. L40
    have hAnorm : ∃ ab. ∃ ac. BitCount(ab,ac,p,k) ∧ ModularSetPullback(b,c,ab,ac,p,x1)Definitions: ModularSetPullbackBitCount
  2. L41
    specialize finite_modular_set_pullback_exists b
  3. L42
    specialize finite_modular_set_pullback_exists c
  4. L43
    specialize finite_modular_set_pullback_exists p
  5. L44
    specialize finite_modular_set_pullback_exists k
  6. L45
    specialize finite_modular_set_pullback_exists x1
  7. L46
    apply finite_modular_set_pullback_exists
  8. L47
    exact hpzero
  9. L48
    exact hA
11Separate the logical casesL49–51

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

  1. L49
    cases hAnorm
  2. L50
    cases hAnorm_witness
  3. L51
    cases hAnorm_witness_witness
12Establish hBnormL52–60

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

  1. L52
    have hBnorm : ∃ bb. ∃ bc. BitCount(bb,bc,p,l) ∧ ModularSetPullback(d,e,bb,bc,p,x)Definitions: ModularSetPullbackBitCount
  2. L53
    specialize finite_modular_set_pullback_exists d
  3. L54
    specialize finite_modular_set_pullback_exists e
  4. L55
    specialize finite_modular_set_pullback_exists p
  5. L56
    specialize finite_modular_set_pullback_exists l
  6. L57
    specialize finite_modular_set_pullback_exists x
  7. L58
    apply finite_modular_set_pullback_exists
  8. L59
    exact hpzero
  9. L60
    exact hB
13Separate the logical casesL61–63

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

  1. L61
    cases hBnorm
  2. L62
    cases hBnorm_witness
  3. L63
    cases hBnorm_witness_witness
14Use earlier factsL64–73

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

  1. L64
    specialize prime_cauchy_davenport_normalized_cover_bound p
  2. L65
    specialize prime_cauchy_davenport_normalized_cover_bound x2
  3. L66
    specialize prime_cauchy_davenport_normalized_cover_bound x3
  4. L67
    specialize prime_cauchy_davenport_normalized_cover_bound x4
  5. L68
    specialize prime_cauchy_davenport_normalized_cover_bound x5
  6. L69
    specialize prime_cauchy_davenport_normalized_cover_bound sb
  7. L70
    specialize prime_cauchy_davenport_normalized_cover_bound sc
  8. L71
    specialize prime_cauchy_davenport_normalized_cover_bound k
  9. L72
    specialize prime_cauchy_davenport_normalized_cover_bound l
  10. L73
    specialize prime_cauchy_davenport_normalized_cover_bound m
15Use earlier factsL74–83

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

  1. L74
    apply prime_cauchy_davenport_normalized_cover_bound
  2. L75
    exact hprime
  3. L76
    exact hAnorm_witness_witness_left
  4. L77
    exact hBnorm_witness_witness_left
  5. L78
    exact hS
  6. L79
    exact hk
  7. L80
    specialize finite_modular_pullback_zero_member d
  8. L81
    specialize finite_modular_pullback_zero_member e
  9. L82
    specialize finite_modular_pullback_zero_member x4
  10. L83
    specialize finite_modular_pullback_zero_member x5
16Use earlier factsL84–93

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

  1. L84
    specialize finite_modular_pullback_zero_member p
  2. L85
    specialize finite_modular_pullback_zero_member x
  3. L86
    apply finite_modular_pullback_zero_member
  4. L87
    exact hpzero
  5. L88
    exact hBnorm_witness_witness_right
  6. L89
    exact hmember_witness
  7. L90
    specialize finite_modular_opposite_translates_sum_cover b
  8. L91
    specialize finite_modular_opposite_translates_sum_cover c
  9. L92
    specialize finite_modular_opposite_translates_sum_cover d
  10. L93
    specialize finite_modular_opposite_translates_sum_cover e
17Use earlier factsL94–103

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

  1. L94
    specialize finite_modular_opposite_translates_sum_cover x2
  2. L95
    specialize finite_modular_opposite_translates_sum_cover x3
  3. L96
    specialize finite_modular_opposite_translates_sum_cover x4
  4. L97
    specialize finite_modular_opposite_translates_sum_cover x5
  5. L98
    specialize finite_modular_opposite_translates_sum_cover sb
  6. L99
    specialize finite_modular_opposite_translates_sum_cover sc
  7. L100
    specialize finite_modular_opposite_translates_sum_cover p
  8. L101
    specialize finite_modular_opposite_translates_sum_cover x
  9. L102
    specialize finite_modular_opposite_translates_sum_cover x1
  10. L103
    apply finite_modular_opposite_translates_sum_cover
18Use earlier factsL104–108

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

  1. L104
    exact hpzero
  2. L105
    exact hcomp_witness
  3. L106
    exact hAnorm_witness_witness_right
  4. L107
    exact hBnorm_witness_witness_right
  5. L108
    exact hcover

Library-wide reading audit

Original exact command ledger · 108 lines
  1. 0001intro p
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro sb
  7. 0007intro sc
  8. 0008intro k
  9. 0009intro l
  10. 0010intro m
  11. 0011intro hprime
  12. 0012intro hA
  13. 0013intro hB
  14. 0014intro hS
  15. 0015intro hk
  16. 0016intro hl
  17. 0017intro hcover
  18. 0018have hpzero : ~(p=0)
  19. 0019intro he
  20. 0020specialize prime_nonzero p
  21. 0021apply prime_nonzero
  22. 0022exact hprime
  23. 0023exact he
  24. 0024have hmember : exists t. ((exists fms_gap_member. fms_gap_member + S (t) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (t)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (t)) * e) + (1))))
  25. 0025specialize finite_bit_count_positive_member d
  26. 0026specialize finite_bit_count_positive_member e
  27. 0027specialize finite_bit_count_positive_member p
  28. 0028specialize finite_bit_count_positive_member l
  29. 0029apply finite_bit_count_positive_member
  30. 0030exact hB
  31. 0031exact hl
  32. 0032cases hmember
  33. 0033have hcomp : exists v. x+v=p
  34. 0034specialize finite_modular_additive_complement p
  35. 0035specialize finite_modular_additive_complement x
  36. 0036apply finite_modular_additive_complement
  37. 0037cases hmember_witness
  38. 0038exact hmember_witness_left
  39. 0039cases hcomp
  40. 0040have hAnorm : exists ab ac. (((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)) * (ac))) /\ exists ff_q_fms_count_summand. (ab) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (ac)) + (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)) * (ac))) /\ exists ff_q_fms_count_decoded. (ab) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (ac)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + x1) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * ac)) /\ exists fs_q_fms_pullback_target. ab = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * ac) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * ac)) /\ exists fs_q_fms_pullback_target. ab = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * ac) + (1)))))))
  41. 0041specialize finite_modular_set_pullback_exists b
  42. 0042specialize finite_modular_set_pullback_exists c
  43. 0043specialize finite_modular_set_pullback_exists p
  44. 0044specialize finite_modular_set_pullback_exists k
  45. 0045specialize finite_modular_set_pullback_exists x1
  46. 0046apply finite_modular_set_pullback_exists
  47. 0047exact hpzero
  48. 0048exact hA
  49. 0049cases hAnorm
  50. 0050cases hAnorm_witness
  51. 0051cases hAnorm_witness_witness
  52. 0052have hBnorm : exists bb bc. (((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)) * (bc))) /\ exists ff_q_fms_count_summand. (bb) = ff_q_fms_count_summand * S ((S (ff_i_fms_count)) * (bc)) + (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)) * (bc))) /\ exists ff_q_fms_count_decoded. (bb) = ff_q_fms_count_decoded * S ((S (ff_i_fms_count)) * (bc)) + (ff_bit_fms_count))) /\ (ff_bit_fms_count = 0 \/ ff_bit_fms_count = 1))))) /\ (forall fms_i_pullback fms_j_pullback. (exists fms_gap_pullback_i. fms_gap_pullback_i + S (fms_i_pullback) = (p)) -> (exists fms_gap_pullback_j. fms_gap_pullback_j + S (fms_j_pullback) = (p)) -> (exists fms_u_pullback fms_v_pullback. (fms_i_pullback + x) + (p) * fms_u_pullback = (fms_j_pullback) + (p) * fms_v_pullback) -> ((((((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * bc)) /\ exists fs_q_fms_pullback_target. bb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * bc) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * e)) /\ exists fs_q_fms_pullback_source. d = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * e) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * e)) /\ exists fs_q_fms_pullback_source. d = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * e) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * bc)) /\ exists fs_q_fms_pullback_target. bb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * bc) + (1)))))))
  53. 0053specialize finite_modular_set_pullback_exists d
  54. 0054specialize finite_modular_set_pullback_exists e
  55. 0055specialize finite_modular_set_pullback_exists p
  56. 0056specialize finite_modular_set_pullback_exists l
  57. 0057specialize finite_modular_set_pullback_exists x
  58. 0058apply finite_modular_set_pullback_exists
  59. 0059exact hpzero
  60. 0060exact hB
  61. 0061cases hBnorm
  62. 0062cases hBnorm_witness
  63. 0063cases hBnorm_witness_witness
  64. 0064specialize prime_cauchy_davenport_normalized_cover_bound p
  65. 0065specialize prime_cauchy_davenport_normalized_cover_bound x2
  66. 0066specialize prime_cauchy_davenport_normalized_cover_bound x3
  67. 0067specialize prime_cauchy_davenport_normalized_cover_bound x4
  68. 0068specialize prime_cauchy_davenport_normalized_cover_bound x5
  69. 0069specialize prime_cauchy_davenport_normalized_cover_bound sb
  70. 0070specialize prime_cauchy_davenport_normalized_cover_bound sc
  71. 0071specialize prime_cauchy_davenport_normalized_cover_bound k
  72. 0072specialize prime_cauchy_davenport_normalized_cover_bound l
  73. 0073specialize prime_cauchy_davenport_normalized_cover_bound m
  74. 0074apply prime_cauchy_davenport_normalized_cover_bound
  75. 0075exact hprime
  76. 0076exact hAnorm_witness_witness_left
  77. 0077exact hBnorm_witness_witness_left
  78. 0078exact hS
  79. 0079exact hk
  80. 0080specialize finite_modular_pullback_zero_member d
  81. 0081specialize finite_modular_pullback_zero_member e
  82. 0082specialize finite_modular_pullback_zero_member x4
  83. 0083specialize finite_modular_pullback_zero_member x5
  84. 0084specialize finite_modular_pullback_zero_member p
  85. 0085specialize finite_modular_pullback_zero_member x
  86. 0086apply finite_modular_pullback_zero_member
  87. 0087exact hpzero
  88. 0088exact hBnorm_witness_witness_right
  89. 0089exact hmember_witness
  90. 0090specialize finite_modular_opposite_translates_sum_cover b
  91. 0091specialize finite_modular_opposite_translates_sum_cover c
  92. 0092specialize finite_modular_opposite_translates_sum_cover d
  93. 0093specialize finite_modular_opposite_translates_sum_cover e
  94. 0094specialize finite_modular_opposite_translates_sum_cover x2
  95. 0095specialize finite_modular_opposite_translates_sum_cover x3
  96. 0096specialize finite_modular_opposite_translates_sum_cover x4
  97. 0097specialize finite_modular_opposite_translates_sum_cover x5
  98. 0098specialize finite_modular_opposite_translates_sum_cover sb
  99. 0099specialize finite_modular_opposite_translates_sum_cover sc
  100. 0100specialize finite_modular_opposite_translates_sum_cover p
  101. 0101specialize finite_modular_opposite_translates_sum_cover x
  102. 0102specialize finite_modular_opposite_translates_sum_cover x1
  103. 0103apply finite_modular_opposite_translates_sum_cover
  104. 0104exact hpzero
  105. 0105exact hcomp_witness
  106. 0106exact hAnorm_witness_witness_right
  107. 0107exact hBnorm_witness_witness_right
  108. 0108exact hcover