CD0045

finite_modular_opposite_translates_sum_cover

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

Opposite actual translations of the input sets preserve every coded upper bound for their 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 b c d e ab ac bb bc sb sc p t v. ~(p=0) -> t+v=p -> (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 + v) + (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))))))) -> (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 + t) + (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))))))) -> (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)))) -> (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)) * ac)) /\ exists fs_q_fms_cover_left. ab = fs_q_fms_cover_left * S ((S (fms_i_cover)) * ac) + (1))) -> (((exists fs_h_fms_cover_right. fs_h_fms_cover_right + S (1) = S ((S (fms_j_cover)) * bc)) /\ exists fs_q_fms_cover_right. bb = fs_q_fms_cover_right * S ((S (fms_j_cover)) * bc) + (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))))

Constructive proof overview

Generated structural guide

Opposite actual translations of the input sets preserve every coded upper bound for their sumset.

The unchanged tactic script uses 4 declared prerequisites and contains 91 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD0028 finite_modular_pushforward_membership_witness CD0027 finite_modular_pullback_membership_witness CD0029 finite_modular_shifted_sum_congruence mod_eq_trans Stable theorem; checked-use authorized

Direct dependents

CD0046 prime_cauchy_davenport_cover_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

91 script commands · 16 reading checkpoints · 4 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 (3)
finite modular pushforward membership witnessfinite modular pullback membership witnessfinite modular shifted sum congruence

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 b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro ab
  6. L6
    intro ac
  7. L7
    intro bb
  8. L8
    intro bc
  9. L9
    intro sb
  10. L10
    intro sc
02Fix variables and assumptionsL11–20

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

  1. L11
    intro p
  2. L12
    intro t
  3. L13
    intro v
  4. L14
    intro hp
  5. L15
    intro htv
  6. L16
    intro hApull
  7. L17
    intro hBpull
  8. L18
    intro hcover
  9. L19
    intro a
  10. L20
    intro z
03Fix variables and assumptionsL21–27

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

  1. L21
    intro w
  2. L22
    intro ha
  3. L23
    intro hz
  4. L24
    intro hw
  5. L25
    intro hA
  6. L26
    intro hB
  7. L27
    intro hmod
04Establish hAiffL28–37

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

  1. L28
    have hAiff : (BetaAt(ab,ac,a,1) → ∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + t,a)) ∧ ((∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + t,a)) → BetaAt(ab,ac,a,1))Definitions: ModularSetMemberModEqBetaAt
  2. L29
    specialize finite_modular_pushforward_membership_witness b
  3. L30
    specialize finite_modular_pushforward_membership_witness c
  4. L31
    specialize finite_modular_pushforward_membership_witness ab
  5. L32
    specialize finite_modular_pushforward_membership_witness ac
  6. L33
    specialize finite_modular_pushforward_membership_witness p
  7. L34
    specialize finite_modular_pushforward_membership_witness t
  8. L35
    specialize finite_modular_pushforward_membership_witness v
  9. L36
    specialize finite_modular_pushforward_membership_witness a
  10. L37
    apply finite_modular_pushforward_membership_witness
05Use earlier factsL38–41

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

  1. L38
    exact hp
  2. L39
    exact htv
  3. L40
    exact hApull
  4. L41
    exact ha
06Separate the logical casesL42–42

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

  1. L42
    cases hAiff
07Establish hBiffL43–52

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

  1. L43
    have hBiff : (BetaAt(bb,bc,z,1) → ∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,z + t,x)) ∧ ((∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,z + t,x)) → BetaAt(bb,bc,z,1))Definitions: ModularSetMemberModEqBetaAt
  2. L44
    specialize finite_modular_pullback_membership_witness d
  3. L45
    specialize finite_modular_pullback_membership_witness e
  4. L46
    specialize finite_modular_pullback_membership_witness bb
  5. L47
    specialize finite_modular_pullback_membership_witness bc
  6. L48
    specialize finite_modular_pullback_membership_witness p
  7. L49
    specialize finite_modular_pullback_membership_witness t
  8. L50
    specialize finite_modular_pullback_membership_witness z
  9. L51
    apply finite_modular_pullback_membership_witness
  10. L52
    exact hp
08Use earlier factsL53–54

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

  1. L53
    exact hBpull
  2. L54
    exact hz
09Separate the logical casesL55–55

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

  1. L55
    cases hBiff
10Establish hAsourceL56–58

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

  1. L56
    have hAsource : exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)
  2. L57
    apply hAiff_left
  3. L58
    exact hA
11Separate the logical casesL59–61

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

  1. L59
    cases hAsource
  2. L60
    cases hAsource_witness
  3. L61
    cases hAsource_witness_left
12Establish hBsourceL62–64

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

  1. L62
    have hBsource : exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (j)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  2. L63
    apply hBiff_left
  3. L64
    exact hB
13Separate the logical casesL65–67

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

  1. L65
    cases hBsource
  2. L66
    cases hBsource_witness
  3. L67
    cases hBsource_witness_left
14Use earlier factsL68–77

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

  1. L68
    specialize hcover x
  2. L69
    specialize hcover x1
  3. L70
    specialize hcover w
  4. L71
    apply hcover
  5. L72
    exact hAsource_witness_left_left
  6. L73
    exact hBsource_witness_left_left
  7. L74
    exact hw
  8. L75
    exact hAsource_witness_left_right
  9. L76
    exact hBsource_witness_left_right
  10. L77
    specialize mod_eq_trans p
15Use earlier factsL78–87

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

  1. L78
    specialize mod_eq_trans x+x1
  2. L79
    specialize mod_eq_trans a+z
  3. L80
    specialize mod_eq_trans w
  4. L81
    apply mod_eq_trans
  5. L82
    specialize finite_modular_shifted_sum_congruence p
  6. L83
    specialize finite_modular_shifted_sum_congruence x
  7. L84
    specialize finite_modular_shifted_sum_congruence x1
  8. L85
    specialize finite_modular_shifted_sum_congruence a
  9. L86
    specialize finite_modular_shifted_sum_congruence z
  10. L87
    specialize finite_modular_shifted_sum_congruence t
16Use earlier factsL88–91

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

  1. L88
    apply finite_modular_shifted_sum_congruence
  2. L89
    exact hAsource_witness_right
  3. L90
    exact hBsource_witness_right
  4. L91
    exact hmod

Library-wide reading audit

Original exact command ledger · 91 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro ab
  6. 0006intro ac
  7. 0007intro bb
  8. 0008intro bc
  9. 0009intro sb
  10. 0010intro sc
  11. 0011intro p
  12. 0012intro t
  13. 0013intro v
  14. 0014intro hp
  15. 0015intro htv
  16. 0016intro hApull
  17. 0017intro hBpull
  18. 0018intro hcover
  19. 0019intro a
  20. 0020intro z
  21. 0021intro w
  22. 0022intro ha
  23. 0023intro hz
  24. 0024intro hw
  25. 0025intro hA
  26. 0026intro hB
  27. 0027intro hmod
  28. 0028have hAiff : (((((exists fs_h_cd_norm_A. fs_h_cd_norm_A + S (1) = S ((S (a)) * ac)) /\ exists fs_q_cd_norm_A. ab = fs_q_cd_norm_A * S ((S (a)) * ac) + (1))) -> (exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod))) /\ ((exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)) -> (((exists fs_h_cd_norm_A. fs_h_cd_norm_A + S (1) = S ((S (a)) * ac)) /\ exists fs_q_cd_norm_A. ab = fs_q_cd_norm_A * S ((S (a)) * ac) + (1)))))
  29. 0029specialize finite_modular_pushforward_membership_witness b
  30. 0030specialize finite_modular_pushforward_membership_witness c
  31. 0031specialize finite_modular_pushforward_membership_witness ab
  32. 0032specialize finite_modular_pushforward_membership_witness ac
  33. 0033specialize finite_modular_pushforward_membership_witness p
  34. 0034specialize finite_modular_pushforward_membership_witness t
  35. 0035specialize finite_modular_pushforward_membership_witness v
  36. 0036specialize finite_modular_pushforward_membership_witness a
  37. 0037apply finite_modular_pushforward_membership_witness
  38. 0038exact hp
  39. 0039exact htv
  40. 0040exact hApull
  41. 0041exact ha
  42. 0042cases hAiff
  43. 0043have hBiff : (((((exists fs_h_cd_norm_B. fs_h_cd_norm_B + S (1) = S ((S (z)) * bc)) /\ exists fs_q_cd_norm_B. bb = fs_q_cd_norm_B * S ((S (z)) * bc) + (1))) -> (exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (j)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod))) /\ ((exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (j)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)) -> (((exists fs_h_cd_norm_B. fs_h_cd_norm_B + S (1) = S ((S (z)) * bc)) /\ exists fs_q_cd_norm_B. bb = fs_q_cd_norm_B * S ((S (z)) * bc) + (1)))))
  44. 0044specialize finite_modular_pullback_membership_witness d
  45. 0045specialize finite_modular_pullback_membership_witness e
  46. 0046specialize finite_modular_pullback_membership_witness bb
  47. 0047specialize finite_modular_pullback_membership_witness bc
  48. 0048specialize finite_modular_pullback_membership_witness p
  49. 0049specialize finite_modular_pullback_membership_witness t
  50. 0050specialize finite_modular_pullback_membership_witness z
  51. 0051apply finite_modular_pullback_membership_witness
  52. 0052exact hp
  53. 0053exact hBpull
  54. 0054exact hz
  55. 0055cases hBiff
  56. 0056have hAsource : exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (j+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)
  57. 0057apply hAiff_left
  58. 0058exact hA
  59. 0059cases hAsource
  60. 0060cases hAsource_witness
  61. 0061cases hAsource_witness_left
  62. 0062have hBsource : exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (j)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  63. 0063apply hBiff_left
  64. 0064exact hB
  65. 0065cases hBsource
  66. 0066cases hBsource_witness
  67. 0067cases hBsource_witness_left
  68. 0068specialize hcover x
  69. 0069specialize hcover x1
  70. 0070specialize hcover w
  71. 0071apply hcover
  72. 0072exact hAsource_witness_left_left
  73. 0073exact hBsource_witness_left_left
  74. 0074exact hw
  75. 0075exact hAsource_witness_left_right
  76. 0076exact hBsource_witness_left_right
  77. 0077specialize mod_eq_trans p
  78. 0078specialize mod_eq_trans x+x1
  79. 0079specialize mod_eq_trans a+z
  80. 0080specialize mod_eq_trans w
  81. 0081apply mod_eq_trans
  82. 0082specialize finite_modular_shifted_sum_congruence p
  83. 0083specialize finite_modular_shifted_sum_congruence x
  84. 0084specialize finite_modular_shifted_sum_congruence x1
  85. 0085specialize finite_modular_shifted_sum_congruence a
  86. 0086specialize finite_modular_shifted_sum_congruence z
  87. 0087specialize finite_modular_shifted_sum_congruence t
  88. 0088apply finite_modular_shifted_sum_congruence
  89. 0089exact hAsource_witness_right
  90. 0090exact hBsource_witness_right
  91. 0091exact hmod