CD0041

prime_modular_normalized_boundary_exists

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

A normalized nontrivial second set and a non-full upper sumset construct an actual boundary suitable for strict Dyson descent.

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 sb sc p k l m. ((~(p = 1) /\ forall frp_prime_left_cd_normalized_prime frp_prime_right_cd_normalized_prime. p = frp_prime_left_cd_normalized_prime * frp_prime_right_cd_normalized_prime -> frp_prime_left_cd_normalized_prime = 1 \/ frp_prime_right_cd_normalized_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) -> (exists fms_gap_le. fms_gap_le + (2) = (l)) -> (((exists fms_gap_member. fms_gap_member + S (0) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (0)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (0)) * e) + (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)))) -> ~(m=p) -> exists h t r. (((exists fms_gap_member. fms_gap_member + S (h) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (h)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (h)) * e) + (1))))) /\ ((((exists fms_gap_cd_boundary_source. fms_gap_cd_boundary_source + S (t) = (p)) /\ (((exists fs_h_fms_cd_boundary_source. fs_h_fms_cd_boundary_source + S (1) = S ((S (t)) * c)) /\ exists fs_q_fms_cd_boundary_source. b = fs_q_fms_cd_boundary_source * S ((S (t)) * c) + (1))))) /\ ((exists fms_gap_cd_boundary_target. fms_gap_cd_boundary_target + S (r) = (p)) /\ ((exists fms_u_cd_boundary_shift fms_v_cd_boundary_shift. (t+h) + (p) * fms_u_cd_boundary_shift = (r) + (p) * fms_v_cd_boundary_shift) /\ ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (r)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (r)) * c) + (1))))))

Constructive proof overview

Generated structural guide

A normalized nontrivial second set and a non-full upper sumset construct an actual boundary suitable for strict Dyson descent.

The unchanged tactic script uses 6 declared prerequisites and contains 95 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD000D finite_bit_count_missing_zero CD0003 finite_bit_count_positive_member CD000E finite_bit_count_two_nonzero_member CD0035 prime_modular_set_translation_boundary_exists CD003F finite_modular_zero_sum_left_subset CD0023 finite_bit_zero_nonmember

Direct dependents

CD0042 prime_cauchy_davenport_normalized_bounded_induction

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

95 script commands · 21 reading checkpoints · 6 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 missing zerofinite bit count positive memberfinite bit count two nonzero memberprime modular set translation boundary existsfinite modular zero sum left subsetfinite bit zero nonmember

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

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

  1. L11
    intro hp
  2. L12
    intro hA
  3. L13
    intro hB
  4. L14
    intro hS
  5. L15
    intro hk
  6. L16
    intro hl
  7. L17
    intro hzero
  8. L18
    intro hcover
  9. L19
    intro hm
03Establish houtL20–27

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

  1. L20
    have hout : exists z. (exists fms_gap_lt. fms_gap_lt + S (z) = (p)) /\ (((exists fs_h_cd_normalized_out. fs_h_cd_normalized_out + S (0) = S ((S (z)) * sc)) /\ exists fs_q_cd_normalized_out. sb = fs_q_cd_normalized_out * S ((S (z)) * sc) + (0)))
  2. L21
    specialize finite_bit_count_missing_zero sb
  3. L22
    specialize finite_bit_count_missing_zero sc
  4. L23
    specialize finite_bit_count_missing_zero p
  5. L24
    specialize finite_bit_count_missing_zero m
  6. L25
    apply finite_bit_count_missing_zero
  7. L26
    exact hS
  8. L27
    exact hm
04Separate the logical casesL28–29

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

  1. L28
    cases hout
  2. L29
    cases hout_witness
05Establish haL30–37

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

  1. L30
    have ha : exists a. ((exists fms_gap_member. fms_gap_member + S (a) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (a)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (a)) * c) + (1))))
  2. L31
    specialize finite_bit_count_positive_member b
  3. L32
    specialize finite_bit_count_positive_member c
  4. L33
    specialize finite_bit_count_positive_member p
  5. L34
    specialize finite_bit_count_positive_member k
  6. L35
    apply finite_bit_count_positive_member
  7. L36
    exact hA
  8. L37
    exact hk
06Separate the logical casesL38–38

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

  1. L38
    cases ha
07Establish hhL39–46

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

  1. L39
    have hh : exists h. (((exists fms_gap_member. fms_gap_member + S (h) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (h)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (h)) * e) + (1))))) /\ ~(h=0)
  2. L40
    specialize finite_bit_count_two_nonzero_member d
  3. L41
    specialize finite_bit_count_two_nonzero_member e
  4. L42
    specialize finite_bit_count_two_nonzero_member p
  5. L43
    specialize finite_bit_count_two_nonzero_member l
  6. L44
    apply finite_bit_count_two_nonzero_member
  7. L45
    exact hB
  8. L46
    exact hl
08Separate the logical casesL47–48

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

  1. L47
    cases hh
  2. L48
    cases hh_witness
09Establish hsubL49–58

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite modular zero sum left subset.

  1. L49
    have hsub : forall fms_i_subset. (exists fms_gap_subset. fms_gap_subset + S (fms_i_subset) = (p)) -> (((exists fs_h_fms_subset_left. fs_h_fms_subset_left + S (1) = S ((S (fms_i_subset)) * c)) /\ exists fs_q_fms_subset_left. b = fs_q_fms_subset_left * S ((S (fms_i_subset)) * c) + (1))) -> (((exists fs_h_fms_subset_right. fs_h_fms_subset_right + S (1) = S ((S (fms_i_subset)) * sc)) /\ exists fs_q_fms_subset_right. sb = fs_q_fms_subset_right * S ((S (fms_i_subset)) * sc) + (1)))
  2. L50
    specialize finite_modular_zero_sum_left_subset b
  3. L51
    specialize finite_modular_zero_sum_left_subset c
  4. L52
    specialize finite_modular_zero_sum_left_subset d
  5. L53
    specialize finite_modular_zero_sum_left_subset e
  6. L54
    specialize finite_modular_zero_sum_left_subset sb
  7. L55
    specialize finite_modular_zero_sum_left_subset sc
  8. L56
    specialize finite_modular_zero_sum_left_subset p
  9. L57
    apply finite_modular_zero_sum_left_subset
  10. L58
    exact hcover
10Use earlier factsL59–59

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

  1. L59
    exact hzero
11Establish hnotAL60–69

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

  1. L60
    have hnotA : ~(((exists fs_h_cd_normalized_notA. fs_h_cd_normalized_notA + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_normalized_notA. b = fs_q_cd_normalized_notA * S ((S (x)) * c) + (1)))
  2. L61
    intro hmember
  3. L62
    specialize finite_bit_zero_nonmember sb
  4. L63
    specialize finite_bit_zero_nonmember sc
  5. L64
    specialize finite_bit_zero_nonmember x
  6. L65
    apply finite_bit_zero_nonmember
  7. L66
    exact hout_witness_right
  8. L67
    specialize hsub x
  9. L68
    apply hsub
  10. L69
    exact hout_witness_left
12Use earlier factsL70–70

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

  1. L70
    exact hmember
13Establish hboundaryL71–79

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

  1. L71
    have hboundary : ∃ cd_source_boundary. ∃ cd_target_boundary. ModularTranslationBoundary(b,c,p,x2,cd_source_boundary,cd_target_boundary)Definitions: ModularTranslationBoundary
  2. L72
    specialize prime_modular_set_translation_boundary_exists b
  3. L73
    specialize prime_modular_set_translation_boundary_exists c
  4. L74
    specialize prime_modular_set_translation_boundary_exists p
  5. L75
    specialize prime_modular_set_translation_boundary_exists x2
  6. L76
    specialize prime_modular_set_translation_boundary_exists x1
  7. L77
    specialize prime_modular_set_translation_boundary_exists x
  8. L78
    apply prime_modular_set_translation_boundary_exists
  9. L79
    exact hp
14Separate the logical casesL80–80

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

  1. L80
    cases hA
15Use earlier factsL81–85

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

  1. L81
    exact hA_right
  2. L82
    exact ha_witness
  3. L83
    exact hout_witness_left
  4. L84
    exact hnotA
  5. L85
    exact hh_witness_right
16Separate the logical casesL86–86

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

  1. L86
    cases hh_witness_left
17Use earlier factsL87–87

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

  1. L87
    exact hh_witness_left_left
18Separate the logical casesL88–89

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

  1. L88
    cases hboundary
  2. L89
    cases hboundary_witness
19Construct an explicit witnessL90–92

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

  1. L90
    exists x2
  2. L91
    exists x3
  3. L92
    exists x4
20Separate the logical casesL93–93

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

  1. L93
    split
21Use earlier factsL94–95

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

  1. L94
    exact hh_witness_left
  2. L95
    exact hboundary_witness_witness

Library-wide reading audit

Original exact command ledger · 95 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro sb
  6. 0006intro sc
  7. 0007intro p
  8. 0008intro k
  9. 0009intro l
  10. 0010intro m
  11. 0011intro hp
  12. 0012intro hA
  13. 0013intro hB
  14. 0014intro hS
  15. 0015intro hk
  16. 0016intro hl
  17. 0017intro hzero
  18. 0018intro hcover
  19. 0019intro hm
  20. 0020have hout : exists z. (exists fms_gap_lt. fms_gap_lt + S (z) = (p)) /\ (((exists fs_h_cd_normalized_out. fs_h_cd_normalized_out + S (0) = S ((S (z)) * sc)) /\ exists fs_q_cd_normalized_out. sb = fs_q_cd_normalized_out * S ((S (z)) * sc) + (0)))
  21. 0021specialize finite_bit_count_missing_zero sb
  22. 0022specialize finite_bit_count_missing_zero sc
  23. 0023specialize finite_bit_count_missing_zero p
  24. 0024specialize finite_bit_count_missing_zero m
  25. 0025apply finite_bit_count_missing_zero
  26. 0026exact hS
  27. 0027exact hm
  28. 0028cases hout
  29. 0029cases hout_witness
  30. 0030have ha : exists a. ((exists fms_gap_member. fms_gap_member + S (a) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (a)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (a)) * c) + (1))))
  31. 0031specialize finite_bit_count_positive_member b
  32. 0032specialize finite_bit_count_positive_member c
  33. 0033specialize finite_bit_count_positive_member p
  34. 0034specialize finite_bit_count_positive_member k
  35. 0035apply finite_bit_count_positive_member
  36. 0036exact hA
  37. 0037exact hk
  38. 0038cases ha
  39. 0039have hh : exists h. (((exists fms_gap_member. fms_gap_member + S (h) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (h)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (h)) * e) + (1))))) /\ ~(h=0)
  40. 0040specialize finite_bit_count_two_nonzero_member d
  41. 0041specialize finite_bit_count_two_nonzero_member e
  42. 0042specialize finite_bit_count_two_nonzero_member p
  43. 0043specialize finite_bit_count_two_nonzero_member l
  44. 0044apply finite_bit_count_two_nonzero_member
  45. 0045exact hB
  46. 0046exact hl
  47. 0047cases hh
  48. 0048cases hh_witness
  49. 0049have hsub : forall fms_i_subset. (exists fms_gap_subset. fms_gap_subset + S (fms_i_subset) = (p)) -> (((exists fs_h_fms_subset_left. fs_h_fms_subset_left + S (1) = S ((S (fms_i_subset)) * c)) /\ exists fs_q_fms_subset_left. b = fs_q_fms_subset_left * S ((S (fms_i_subset)) * c) + (1))) -> (((exists fs_h_fms_subset_right. fs_h_fms_subset_right + S (1) = S ((S (fms_i_subset)) * sc)) /\ exists fs_q_fms_subset_right. sb = fs_q_fms_subset_right * S ((S (fms_i_subset)) * sc) + (1)))
  50. 0050specialize finite_modular_zero_sum_left_subset b
  51. 0051specialize finite_modular_zero_sum_left_subset c
  52. 0052specialize finite_modular_zero_sum_left_subset d
  53. 0053specialize finite_modular_zero_sum_left_subset e
  54. 0054specialize finite_modular_zero_sum_left_subset sb
  55. 0055specialize finite_modular_zero_sum_left_subset sc
  56. 0056specialize finite_modular_zero_sum_left_subset p
  57. 0057apply finite_modular_zero_sum_left_subset
  58. 0058exact hcover
  59. 0059exact hzero
  60. 0060have hnotA : ~(((exists fs_h_cd_normalized_notA. fs_h_cd_normalized_notA + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_normalized_notA. b = fs_q_cd_normalized_notA * S ((S (x)) * c) + (1)))
  61. 0061intro hmember
  62. 0062specialize finite_bit_zero_nonmember sb
  63. 0063specialize finite_bit_zero_nonmember sc
  64. 0064specialize finite_bit_zero_nonmember x
  65. 0065apply finite_bit_zero_nonmember
  66. 0066exact hout_witness_right
  67. 0067specialize hsub x
  68. 0068apply hsub
  69. 0069exact hout_witness_left
  70. 0070exact hmember
  71. 0071have hboundary : exists cd_source_boundary cd_target_boundary. ((((exists fms_gap_cd_boundary_source. fms_gap_cd_boundary_source + S (cd_source_boundary) = (p)) /\ (((exists fs_h_fms_cd_boundary_source. fs_h_fms_cd_boundary_source + S (1) = S ((S (cd_source_boundary)) * c)) /\ exists fs_q_fms_cd_boundary_source. b = fs_q_fms_cd_boundary_source * S ((S (cd_source_boundary)) * c) + (1))))) /\ ((exists fms_gap_cd_boundary_target. fms_gap_cd_boundary_target + S (cd_target_boundary) = (p)) /\ ((exists fms_u_cd_boundary_shift fms_v_cd_boundary_shift. (cd_source_boundary+x2) + (p) * fms_u_cd_boundary_shift = (cd_target_boundary) + (p) * fms_v_cd_boundary_shift) /\ ~(((exists fs_h_cd_boundary_outside. fs_h_cd_boundary_outside + S (1) = S ((S (cd_target_boundary)) * c)) /\ exists fs_q_cd_boundary_outside. b = fs_q_cd_boundary_outside * S ((S (cd_target_boundary)) * c) + (1))))))
  72. 0072specialize prime_modular_set_translation_boundary_exists b
  73. 0073specialize prime_modular_set_translation_boundary_exists c
  74. 0074specialize prime_modular_set_translation_boundary_exists p
  75. 0075specialize prime_modular_set_translation_boundary_exists x2
  76. 0076specialize prime_modular_set_translation_boundary_exists x1
  77. 0077specialize prime_modular_set_translation_boundary_exists x
  78. 0078apply prime_modular_set_translation_boundary_exists
  79. 0079exact hp
  80. 0080cases hA
  81. 0081exact hA_right
  82. 0082exact ha_witness
  83. 0083exact hout_witness_left
  84. 0084exact hnotA
  85. 0085exact hh_witness_right
  86. 0086cases hh_witness_left
  87. 0087exact hh_witness_left_left
  88. 0088cases hboundary
  89. 0089cases hboundary_witness
  90. 0090exists x2
  91. 0091exists x3
  92. 0092exists x4
  93. 0093split
  94. 0094exact hh_witness_left
  95. 0095exact hboundary_witness_witness