CD0036

finite_modular_dyson_upper_from_union

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

The actual union with a genuine forward translate has exactly the upper Dyson-transform membership.

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 tb tc ub uc 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)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (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)) * tc)) /\ exists fs_q_fms_pullback_target. tb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * tc) + (1))))))) -> (forall fms_i_binary. (exists fms_gap_binary. fms_gap_binary + S (fms_i_binary) = (p)) -> ((((((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (1))) -> (((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1)))))) /\ ((((((exists fs_h_fms_binary_left. fs_h_fms_binary_left + S (1) = S ((S (fms_i_binary)) * c)) /\ exists fs_q_fms_binary_left. b = fs_q_fms_binary_left * S ((S (fms_i_binary)) * c) + (1))) \/ (((exists fs_h_fms_binary_right. fs_h_fms_binary_right + S (1) = S ((S (fms_i_binary)) * tc)) /\ exists fs_q_fms_binary_right. tb = fs_q_fms_binary_right * S ((S (fms_i_binary)) * tc) + (1))))) -> (((exists fs_h_fms_binary_result. fs_h_fms_binary_result + S (1) = S ((S (fms_i_binary)) * uc)) /\ exists fs_q_fms_binary_result. ub = fs_q_fms_binary_result * S ((S (fms_i_binary)) * uc) + (1))))))) -> (forall cd_output_upper. (exists fms_gap_cd_upper_bound. fms_gap_cd_upper_bound + S (cd_output_upper) = (p)) -> ((((((exists fs_h_cd_upper_result. fs_h_cd_upper_result + S (1) = S ((S (cd_output_upper)) * uc)) /\ exists fs_q_cd_upper_result. ub = fs_q_cd_upper_result * S ((S (cd_output_upper)) * uc) + (1))) -> ((((exists fs_h_cd_upper_old. fs_h_cd_upper_old + S (1) = S ((S (cd_output_upper)) * c)) /\ exists fs_q_cd_upper_old. b = fs_q_cd_upper_old * S ((S (cd_output_upper)) * c) + (1))) \/ (exists cd_source_upper. (((exists fms_gap_cd_upper_member. fms_gap_cd_upper_member + S (cd_source_upper) = (p)) /\ (((exists fs_h_fms_cd_upper_member. fs_h_fms_cd_upper_member + S (1) = S ((S (cd_source_upper)) * e)) /\ exists fs_q_fms_cd_upper_member. d = fs_q_fms_cd_upper_member * S ((S (cd_source_upper)) * e) + (1))))) /\ (exists fms_u_cd_upper_mod fms_v_cd_upper_mod. (cd_source_upper+t) + (p) * fms_u_cd_upper_mod = (cd_output_upper) + (p) * fms_v_cd_upper_mod)))) /\ (((((exists fs_h_cd_upper_old. fs_h_cd_upper_old + S (1) = S ((S (cd_output_upper)) * c)) /\ exists fs_q_cd_upper_old. b = fs_q_cd_upper_old * S ((S (cd_output_upper)) * c) + (1))) \/ (exists cd_source_upper. (((exists fms_gap_cd_upper_member. fms_gap_cd_upper_member + S (cd_source_upper) = (p)) /\ (((exists fs_h_fms_cd_upper_member. fs_h_fms_cd_upper_member + S (1) = S ((S (cd_source_upper)) * e)) /\ exists fs_q_fms_cd_upper_member. d = fs_q_fms_cd_upper_member * S ((S (cd_source_upper)) * e) + (1))))) /\ (exists fms_u_cd_upper_mod fms_v_cd_upper_mod. (cd_source_upper+t) + (p) * fms_u_cd_upper_mod = (cd_output_upper) + (p) * fms_v_cd_upper_mod))) -> (((exists fs_h_cd_upper_result. fs_h_cd_upper_result + S (1) = S ((S (cd_output_upper)) * uc)) /\ exists fs_q_cd_upper_result. ub = fs_q_cd_upper_result * S ((S (cd_output_upper)) * uc) + (1)))))))

Constructive proof overview

Generated structural guide

The actual union with a genuine forward translate has exactly the upper Dyson-transform membership.

The unchanged tactic script uses 1 declared prerequisite and contains 56 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

Direct dependents

CD0038 finite_modular_dyson_transform_exists

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

56 script commands · 19 reading checkpoints · 3 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 (1)
finite modular pushforward membership witness

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 tb
  6. L6
    intro tc
  7. L7
    intro ub
  8. L8
    intro uc
  9. L9
    intro p
  10. L10
    intro t
02Fix variables and assumptionsL11–17

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

  1. L11
    intro v
  2. L12
    intro hp
  3. L13
    intro htv
  4. L14
    intro hpull
  5. L15
    intro hunion
  6. L16
    intro z
  7. L17
    intro hz
03Establish hshiftL18–27

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

  1. L18
    have hshift : (BetaAt(tb,tc,z,1) → ∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,z)) ∧ ((∃ x. ModularSetMember(d,e,p,x) ∧ ModEq(p,x + t,z)) → BetaAt(tb,tc,z,1))Definitions: ModularSetMemberModEqBetaAt
  2. L19
    specialize finite_modular_pushforward_membership_witness d
  3. L20
    specialize finite_modular_pushforward_membership_witness e
  4. L21
    specialize finite_modular_pushforward_membership_witness tb
  5. L22
    specialize finite_modular_pushforward_membership_witness tc
  6. L23
    specialize finite_modular_pushforward_membership_witness p
  7. L24
    specialize finite_modular_pushforward_membership_witness t
  8. L25
    specialize finite_modular_pushforward_membership_witness v
  9. L26
    specialize finite_modular_pushforward_membership_witness z
  10. L27
    apply finite_modular_pushforward_membership_witness
04Use earlier factsL28–31

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

  1. L28
    exact hp
  2. L29
    exact htv
  3. L30
    exact hpull
  4. L31
    exact hz
05Separate the logical casesL32–32

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

  1. L32
    cases hshift
06Establish hunL33–36

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

  1. L33
    have hun : (BetaAt(ub,uc,z,1) → BetaAt(b,c,z,1) ∨ BetaAt(tb,tc,z,1)) ∧ (BetaAt(b,c,z,1) ∨ BetaAt(tb,tc,z,1) → BetaAt(ub,uc,z,1))Definitions: BetaAt
  2. L34
    specialize hunion z
  3. L35
    apply hunion
  4. L36
    exact hz
07Separate the logical casesL37–38

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

  1. L37
    cases hun
  2. L38
    split
08Fix variables and assumptionsL39–39

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

  1. L39
    intro hu
09Establish hcaseL40–42

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

  1. L40
    have hcase : (((exists fs_h_cd_U_A. fs_h_cd_U_A + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_U_A. b = fs_q_cd_U_A * S ((S (z)) * c) + (1))) \/ (((exists fs_h_cd_U_T. fs_h_cd_U_T + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_U_T. tb = fs_q_cd_U_T * S ((S (z)) * tc) + (1)))
  2. L41
    apply hun_left
  3. L42
    exact hu
10Separate the logical casesL43–44

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

  1. L43
    cases hcase
  2. L44
    left
11Use earlier factsL45–45

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

  1. L45
    exact hcase_left
12Separate the logical casesL46–46

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

  1. L46
    right
13Use earlier factsL47–48

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

  1. L47
    apply hshift_left
  2. L48
    exact hcase_right
14Fix variables and assumptionsL49–49

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

  1. L49
    intro hcase
15Use earlier factsL50–50

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

  1. L50
    apply hun_right
16Separate the logical casesL51–52

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

  1. L51
    cases hcase
  2. L52
    left
17Use earlier factsL53–53

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

  1. L53
    exact hcase_left
18Separate the logical casesL54–54

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

  1. L54
    right
19Use earlier factsL55–56

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

  1. L55
    apply hshift_right
  2. L56
    exact hcase_right

Library-wide reading audit

Original exact command ledger · 56 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro ub
  8. 0008intro uc
  9. 0009intro p
  10. 0010intro t
  11. 0011intro v
  12. 0012intro hp
  13. 0013intro htv
  14. 0014intro hpull
  15. 0015intro hunion
  16. 0016intro z
  17. 0017intro hz
  18. 0018have hshift : (((((exists fs_h_cd_upper_shift. fs_h_cd_upper_shift + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_upper_shift. tb = fs_q_cd_upper_shift * S ((S (z)) * tc) + (1))) -> (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)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (a)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (a+t) + (p) * fms_u_mod = (z) + (p) * fms_v_mod))) /\ ((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)) * e)) /\ exists fs_q_fms_member. d = fs_q_fms_member * S ((S (a)) * e) + (1))))) /\ (exists fms_u_mod fms_v_mod. (a+t) + (p) * fms_u_mod = (z) + (p) * fms_v_mod)) -> (((exists fs_h_cd_upper_shift. fs_h_cd_upper_shift + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_upper_shift. tb = fs_q_cd_upper_shift * S ((S (z)) * tc) + (1)))))
  19. 0019specialize finite_modular_pushforward_membership_witness d
  20. 0020specialize finite_modular_pushforward_membership_witness e
  21. 0021specialize finite_modular_pushforward_membership_witness tb
  22. 0022specialize finite_modular_pushforward_membership_witness tc
  23. 0023specialize finite_modular_pushforward_membership_witness p
  24. 0024specialize finite_modular_pushforward_membership_witness t
  25. 0025specialize finite_modular_pushforward_membership_witness v
  26. 0026specialize finite_modular_pushforward_membership_witness z
  27. 0027apply finite_modular_pushforward_membership_witness
  28. 0028exact hp
  29. 0029exact htv
  30. 0030exact hpull
  31. 0031exact hz
  32. 0032cases hshift
  33. 0033have hun : (((((exists fs_h_cd_upper_new. fs_h_cd_upper_new + S (1) = S ((S (z)) * uc)) /\ exists fs_q_cd_upper_new. ub = fs_q_cd_upper_new * S ((S (z)) * uc) + (1))) -> ((((exists fs_h_cd_U_A. fs_h_cd_U_A + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_U_A. b = fs_q_cd_U_A * S ((S (z)) * c) + (1))) \/ (((exists fs_h_cd_U_T. fs_h_cd_U_T + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_U_T. tb = fs_q_cd_U_T * S ((S (z)) * tc) + (1))))) /\ (((((exists fs_h_cd_U_A. fs_h_cd_U_A + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_U_A. b = fs_q_cd_U_A * S ((S (z)) * c) + (1))) \/ (((exists fs_h_cd_U_T. fs_h_cd_U_T + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_U_T. tb = fs_q_cd_U_T * S ((S (z)) * tc) + (1)))) -> (((exists fs_h_cd_upper_new. fs_h_cd_upper_new + S (1) = S ((S (z)) * uc)) /\ exists fs_q_cd_upper_new. ub = fs_q_cd_upper_new * S ((S (z)) * uc) + (1)))))
  34. 0034specialize hunion z
  35. 0035apply hunion
  36. 0036exact hz
  37. 0037cases hun
  38. 0038split
  39. 0039intro hu
  40. 0040have hcase : (((exists fs_h_cd_U_A. fs_h_cd_U_A + S (1) = S ((S (z)) * c)) /\ exists fs_q_cd_U_A. b = fs_q_cd_U_A * S ((S (z)) * c) + (1))) \/ (((exists fs_h_cd_U_T. fs_h_cd_U_T + S (1) = S ((S (z)) * tc)) /\ exists fs_q_cd_U_T. tb = fs_q_cd_U_T * S ((S (z)) * tc) + (1)))
  41. 0041apply hun_left
  42. 0042exact hu
  43. 0043cases hcase
  44. 0044left
  45. 0045exact hcase_left
  46. 0046right
  47. 0047apply hshift_left
  48. 0048exact hcase_right
  49. 0049intro hcase
  50. 0050apply hun_right
  51. 0051cases hcase
  52. 0052left
  53. 0053exact hcase_left
  54. 0054right
  55. 0055apply hshift_right
  56. 0056exact hcase_right