CD003D

finite_modular_dyson_sum_cover

Every actual sum from the Dyson pair remains in every coded upper set of the original sumset.

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. ∀ ub. ∀ uc. ∀ vb. ∀ vc. ∀ sb. ∀ sc. ∀ p. ∀ t. ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t) → ModularSetSumCover(b,c,d,e,sb,sc,p) → ModularSetSumCover(ub,uc,vb,vc,sb,sc,p)

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

Definition DAG

ModularSetMember(b,c,p,x) · 6ModularSetSumCover(b,c,d,e,u,v,p) · 2ModularDysonTransform(b,c,d,e,ub,uc,vb,vc,p,t) · 1ModEq(m,a,b) · 6BetaAt(b,c,i,x) · 10

Actual proof prerequisites

finite_modular_shifted_sum_congruencemod_eq_trans · checked external prerequisiteadd_comm · checked external prerequisite
Original expanded first-order statement 
forall b c d e ub uc vb vc sb sc p t. (((forall cd_output_dyson_upper. (exists fms_gap_cd_dyson_upper_bound. fms_gap_cd_dyson_upper_bound + S (cd_output_dyson_upper) = (p)) -> ((((((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))) -> ((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod)))) /\ (((((exists fs_h_cd_dyson_upper_old. fs_h_cd_dyson_upper_old + S (1) = S ((S (cd_output_dyson_upper)) * c)) /\ exists fs_q_cd_dyson_upper_old. b = fs_q_cd_dyson_upper_old * S ((S (cd_output_dyson_upper)) * c) + (1))) \/ (exists cd_source_dyson_upper. (((exists fms_gap_cd_dyson_upper_member. fms_gap_cd_dyson_upper_member + S (cd_source_dyson_upper) = (p)) /\ (((exists fs_h_fms_cd_dyson_upper_member. fs_h_fms_cd_dyson_upper_member + S (1) = S ((S (cd_source_dyson_upper)) * e)) /\ exists fs_q_fms_cd_dyson_upper_member. d = fs_q_fms_cd_dyson_upper_member * S ((S (cd_source_dyson_upper)) * e) + (1))))) /\ (exists fms_u_cd_dyson_upper_mod fms_v_cd_dyson_upper_mod. (cd_source_dyson_upper+t) + (p) * fms_u_cd_dyson_upper_mod = (cd_output_dyson_upper) + (p) * fms_v_cd_dyson_upper_mod))) -> (((exists fs_h_cd_dyson_upper_result. fs_h_cd_dyson_upper_result + S (1) = S ((S (cd_output_dyson_upper)) * uc)) /\ exists fs_q_cd_dyson_upper_result. ub = fs_q_cd_dyson_upper_result * S ((S (cd_output_dyson_upper)) * uc) + (1))))))) /\ (forall cd_output_dyson_lower. (exists fms_gap_cd_dyson_lower_bound. fms_gap_cd_dyson_lower_bound + S (cd_output_dyson_lower) = (p)) -> ((((((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (1))) -> ((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod)))) /\ (((((exists fs_h_cd_dyson_lower_old. fs_h_cd_dyson_lower_old + S (1) = S ((S (cd_output_dyson_lower)) * e)) /\ exists fs_q_cd_dyson_lower_old. d = fs_q_cd_dyson_lower_old * S ((S (cd_output_dyson_lower)) * e) + (1))) /\ (exists cd_source_dyson_lower. (((exists fms_gap_cd_dyson_lower_member. fms_gap_cd_dyson_lower_member + S (cd_source_dyson_lower) = (p)) /\ (((exists fs_h_fms_cd_dyson_lower_member. fs_h_fms_cd_dyson_lower_member + S (1) = S ((S (cd_source_dyson_lower)) * c)) /\ exists fs_q_fms_cd_dyson_lower_member. b = fs_q_fms_cd_dyson_lower_member * S ((S (cd_source_dyson_lower)) * c) + (1))))) /\ (exists fms_u_cd_dyson_lower_mod fms_v_cd_dyson_lower_mod. (cd_output_dyson_lower+t) + (p) * fms_u_cd_dyson_lower_mod = (cd_source_dyson_lower) + (p) * fms_v_cd_dyson_lower_mod))) -> (((exists fs_h_cd_dyson_lower_result. fs_h_cd_dyson_lower_result + S (1) = S ((S (cd_output_dyson_lower)) * vc)) /\ exists fs_q_cd_dyson_lower_result. vb = fs_q_cd_dyson_lower_result * S ((S (cd_output_dyson_lower)) * vc) + (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)) * uc)) /\ exists fs_q_fms_cover_left. ub = fs_q_fms_cover_left * S ((S (fms_i_cover)) * uc) + (1))) -> (((exists fs_h_fms_cover_right. fs_h_fms_cover_right + S (1) = S ((S (fms_j_cover)) * vc)) /\ exists fs_q_fms_cover_right. vb = fs_q_fms_cover_right * S ((S (fms_j_cover)) * vc) + (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))))

Complete tactic proof in conservative notation

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

87 script commands · 17 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.

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 (1)
finite modular shifted sum congruence
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 ub
  6. L6
    intro uc
  7. L7
    intro vb
  8. L8
    intro vc
  9. L9
    intro sb
  10. L10
    intro sc
02Fix variables and assumptionsL11–14

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

  1. L11
    intro p
  2. L12
    intro t
  3. L13
    intro hdyson
  4. L14
    intro hcover
03Separate the logical casesL15–15

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

  1. L15
    cases hdyson
04Fix variables and assumptionsL16–24

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

  1. L16
    intro a
  2. L17
    intro z
  3. L18
    intro w
  4. L19
    intro ha
  5. L20
    intro hz
  6. L21
    intro hw
  7. L22
    intro hU
  8. L23
    intro hV
  9. L24
    intro hmod
05Establish hupperL25–28

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

  1. L25
    have hupper : (BetaAt(ub,uc,a,1) → BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a))) ∧ (BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a)) → BetaAt(ub,uc,a,1))Definitions: BetaAt(ub,uc,a,1)BetaAt(b,c,a,1)ModularSetMember(d,e,p,x)ModEq(p,x + t,a)Original native command in the exact edition
  2. L26
    specialize hdyson_left a
  3. L27
    apply hdyson_left
  4. L28
    exact ha
06Separate the logical casesL29–29

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

  1. L29
    cases hupper
07Establish hlowerL30–33

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

  1. L30
    have hlower : (BetaAt(vb,vc,z,1) → BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x))) ∧ (BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x)) → BetaAt(vb,vc,z,1))Definitions: BetaAt(vb,vc,z,1)BetaAt(d,e,z,1)ModularSetMember(b,c,p,x)ModEq(p,z + t,x)Original native command in the exact edition
  2. L31
    specialize hdyson_right z
  3. L32
    apply hdyson_right
  4. L33
    exact hz
08Separate the logical casesL34–34

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

  1. L34
    cases hlower
09Establish hbothL35–37

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

  1. L35
    have hboth : BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x))Definitions: BetaAt(d,e,z,1)ModularSetMember(b,c,p,x)ModEq(p,z + t,x)Original native command in the exact edition
  2. L36
    apply hlower_left
  3. L37
    exact hV
10Separate the logical casesL38–38

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

  1. L38
    cases hboth
11Establish hcaseL39–41

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

  1. L39
    have hcase : BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a))Definitions: BetaAt(b,c,a,1)ModularSetMember(d,e,p,x)ModEq(p,x + t,a)Original native command in the exact edition
  2. L40
    apply hupper_left
  3. L41
    exact hU
12Separate the logical casesL42–42

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

  1. L42
    cases hcase
13Use earlier factsL43–52

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

  1. L43
    specialize hcover a
  2. L44
    specialize hcover z
  3. L45
    specialize hcover w
  4. L46
    apply hcover
  5. L47
    exact ha
  6. L48
    exact hz
  7. L49
    exact hw
  8. L50
    exact hcase_left
  9. L51
    exact hboth_left
  10. L52
    exact hmod
14Separate the logical casesL53–58

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

  1. L53
    cases hcase_right
  2. L54
    cases hcase_right_witness
  3. L55
    cases hcase_right_witness_left
  4. L56
    cases hboth_right
  5. L57
    cases hboth_right_witness
  6. L58
    cases hboth_right_witness_left
15Use earlier factsL59–67

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

  1. L59
    specialize hcover x1
  2. L60
    specialize hcover x
  3. L61
    specialize hcover w
  4. L62
    apply hcover
  5. L63
    exact hboth_right_witness_left_left
  6. L64
    exact hcase_right_witness_left_left
  7. L65
    exact hw
  8. L66
    exact hboth_right_witness_left_right
  9. L67
    exact hcase_right_witness_left_right
16Establish hcommL68–77

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

  1. L68
    have hcomm : x1+x=x+x1
  2. L69
    specialize add_comm x1
  3. L70
    specialize add_comm x
  4. L71
    apply add_comm
  5. L72
    rewrite hcomm
  6. L73
    specialize mod_eq_trans p
  7. L74
    specialize mod_eq_trans x+x1
  8. L75
    specialize mod_eq_trans a+z
  9. L76
    specialize mod_eq_trans w
  10. L77
    apply mod_eq_trans
17Use earlier factsL78–87

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

  1. L78
    specialize finite_modular_shifted_sum_congruence p
  2. L79
    specialize finite_modular_shifted_sum_congruence x
  3. L80
    specialize finite_modular_shifted_sum_congruence x1
  4. L81
    specialize finite_modular_shifted_sum_congruence a
  5. L82
    specialize finite_modular_shifted_sum_congruence z
  6. L83
    specialize finite_modular_shifted_sum_congruence t
  7. L84
    apply finite_modular_shifted_sum_congruence
  8. L85
    exact hcase_right_witness_right
  9. L86
    exact hboth_right_witness_right
  10. L87
    exact hmod

Library-wide reading audit

Original defined command ledger · 87 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro ub
  6. 0006intro uc
  7. 0007intro vb
  8. 0008intro vc
  9. 0009intro sb
  10. 0010intro sc
  11. 0011intro p
  12. 0012intro t
  13. 0013intro hdyson
  14. 0014intro hcover
  15. 0015cases hdyson
  16. 0016intro a
  17. 0017intro z
  18. 0018intro w
  19. 0019intro ha
  20. 0020intro hz
  21. 0021intro hw
  22. 0022intro hU
  23. 0023intro hV
  24. 0024intro hmod
  25. 0025have hupper : (BetaAt(ub,uc,a,1) → BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a))) ∧ (BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a)) → BetaAt(ub,uc,a,1))
  26. 0026specialize hdyson_left a
  27. 0027apply hdyson_left
  28. 0028exact ha
  29. 0029cases hupper
  30. 0030have hlower : (BetaAt(vb,vc,z,1) → BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x))) ∧ (BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x)) → BetaAt(vb,vc,z,1))
  31. 0031specialize hdyson_right z
  32. 0032apply hdyson_right
  33. 0033exact hz
  34. 0034cases hlower
  35. 0035have hboth : BetaAt(d,e,z,1) ∧ (∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,z + t,x))
  36. 0036apply hlower_left
  37. 0037exact hV
  38. 0038cases hboth
  39. 0039have hcase : BetaAt(b,c,a,1) ∨ (∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,a))
  40. 0040apply hupper_left
  41. 0041exact hU
  42. 0042cases hcase
  43. 0043specialize hcover a
  44. 0044specialize hcover z
  45. 0045specialize hcover w
  46. 0046apply hcover
  47. 0047exact ha
  48. 0048exact hz
  49. 0049exact hw
  50. 0050exact hcase_left
  51. 0051exact hboth_left
  52. 0052exact hmod
  53. 0053cases hcase_right
  54. 0054cases hcase_right_witness
  55. 0055cases hcase_right_witness_left
  56. 0056cases hboth_right
  57. 0057cases hboth_right_witness
  58. 0058cases hboth_right_witness_left
  59. 0059specialize hcover x1
  60. 0060specialize hcover x
  61. 0061specialize hcover w
  62. 0062apply hcover
  63. 0063exact hboth_right_witness_left_left
  64. 0064exact hcase_right_witness_left_left
  65. 0065exact hw
  66. 0066exact hboth_right_witness_left_right
  67. 0067exact hcase_right_witness_left_right
  68. 0068have hcomm : x1+x=x+x1
  69. 0069specialize add_comm x1
  70. 0070specialize add_comm x
  71. 0071apply add_comm
  72. 0072rewrite hcomm
  73. 0073specialize mod_eq_trans p
  74. 0074specialize mod_eq_trans x+x1
  75. 0075specialize mod_eq_trans a+z
  76. 0076specialize mod_eq_trans w
  77. 0077apply mod_eq_trans
  78. 0078specialize finite_modular_shifted_sum_congruence p
  79. 0079specialize finite_modular_shifted_sum_congruence x
  80. 0080specialize finite_modular_shifted_sum_congruence x1
  81. 0081specialize finite_modular_shifted_sum_congruence a
  82. 0082specialize finite_modular_shifted_sum_congruence z
  83. 0083specialize finite_modular_shifted_sum_congruence t
  84. 0084apply finite_modular_shifted_sum_congruence
  85. 0085exact hcase_right_witness_right
  86. 0086exact hboth_right_witness_right
  87. 0087exact hmod