CD0041

prime_modular_normalized_boundary_exists

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

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

∀ b. ∀ c. ∀ d. ∀ e. ∀ sb. ∀ sc. ∀ p. ∀ k. ∀ l. ∀ m. Prime(p) → BitCount(b,c,p,k) → BitCount(d,e,p,l) → BitCount(sb,sc,p,m) → ¬k = 0 → Lt(1,l) → ModularSetMember(d,e,p,0) → ModularSetSumCover(b,c,d,e,sb,sc,p) → ¬m = p → ∃ x. ∃ y. ∃ z. ModularSetMember(d,e,p,x) ∧ ModularTranslationBoundary(b,c,p,x,y,z)

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

Definition DAG

ModularSetMember(b,c,p,x) · 4ModularSetSubset(b,c,d,e,p) · 1ModularSetSumCover(b,c,d,e,u,v,p) · 1ModularTranslationBoundary(b,c,p,d,a,r) · 2Lt(a,b) · 2Prime(p) · 1BetaAt(b,c,i,x) · 2BitCount(b,c,l,z) · 3

Actual proof prerequisites

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
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

All 95 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

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.

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 (6)
finite bit count missing zerofinite bit count positive memberfinite bit count two nonzero memberfinite modular zero sum left subsetfinite bit zero nonmemberprime modular set translation boundary exists
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 : ∃ z. Lt(z,p) ∧ BetaAt(sb,sc,z,0)Definitions: Lt(z,p)BetaAt(sb,sc,z,0)Original native command in the exact edition
  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 : ∃ a. ModularSetMember(b,c,p,a)Definitions: ModularSetMember(b,c,p,a)Original native command in the exact edition
  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 : ∃ h. ModularSetMember(d,e,p,h) ∧ ¬h = 0Definitions: ModularSetMember(d,e,p,h)Original native command in the exact edition
  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 : ModularSetSubset(b,c,sb,sc,p)Definitions: ModularSetSubset(b,c,sb,sc,p)Original native command in the exact edition
  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 : ¬BetaAt(b,c,x,1)Definitions: BetaAt(b,c,x,1)Original native command in the exact edition
  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(b,c,p,x2,cd_source_boundary,cd_target_boundary)Original native command in the exact edition
  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 defined 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 : ∃ z. Lt(z,p) ∧ BetaAt(sb,sc,z,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 : ∃ a. ModularSetMember(b,c,p,a)
  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 : ∃ h. ModularSetMember(d,e,p,h) ∧ ¬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 : ModularSetSubset(b,c,sb,sc,p)
  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 : ¬BetaAt(b,c,x,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 : ∃ cd_source_boundary. ∃ cd_target_boundary. ModularTranslationBoundary(b,c,p,x2,cd_source_boundary,cd_target_boundary)
  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