CD0037

finite_modular_dyson_lower_from_pullback

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

The genuine pullback of A intersection (B+e) is exactly B intersection (A-e), with actual canonical witnesses.

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 ib ic vb vc 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)) * ic)) /\ exists fs_q_fms_binary_result. ib = fs_q_fms_binary_result * S ((S (fms_i_binary)) * ic) + (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)) * ic)) /\ exists fs_q_fms_binary_result. ib = fs_q_fms_binary_result * S ((S (fms_i_binary)) * ic) + (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)) * vc)) /\ exists fs_q_fms_pullback_target. vb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * vc) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * ic)) /\ exists fs_q_fms_pullback_source. ib = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * ic) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * ic)) /\ exists fs_q_fms_pullback_source. ib = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * ic) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * vc)) /\ exists fs_q_fms_pullback_target. vb = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * vc) + (1))))))) -> (forall cd_output_lower. (exists fms_gap_cd_lower_bound. fms_gap_cd_lower_bound + S (cd_output_lower) = (p)) -> ((((((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * vc)) /\ exists fs_q_cd_lower_result. vb = fs_q_cd_lower_result * S ((S (cd_output_lower)) * vc) + (1))) -> ((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod)))) /\ (((((exists fs_h_cd_lower_old. fs_h_cd_lower_old + S (1) = S ((S (cd_output_lower)) * e)) /\ exists fs_q_cd_lower_old. d = fs_q_cd_lower_old * S ((S (cd_output_lower)) * e) + (1))) /\ (exists cd_source_lower. (((exists fms_gap_cd_lower_member. fms_gap_cd_lower_member + S (cd_source_lower) = (p)) /\ (((exists fs_h_fms_cd_lower_member. fs_h_fms_cd_lower_member + S (1) = S ((S (cd_source_lower)) * c)) /\ exists fs_q_fms_cd_lower_member. b = fs_q_fms_cd_lower_member * S ((S (cd_source_lower)) * c) + (1))))) /\ (exists fms_u_cd_lower_mod fms_v_cd_lower_mod. (cd_output_lower+t) + (p) * fms_u_cd_lower_mod = (cd_source_lower) + (p) * fms_v_cd_lower_mod))) -> (((exists fs_h_cd_lower_result. fs_h_cd_lower_result + S (1) = S ((S (cd_output_lower)) * vc)) /\ exists fs_q_cd_lower_result. vb = fs_q_cd_lower_result * S ((S (cd_output_lower)) * vc) + (1)))))))

Constructive proof overview

Generated structural guide

The genuine pullback of A intersection (B+e) is exactly B intersection (A-e), with actual canonical witnesses.

The unchanged tactic script uses 2 declared prerequisites and contains 110 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD0027 finite_modular_pullback_membership_witness CD0026 finite_modular_inverse_shift

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

110 script commands · 32 reading checkpoints · 7 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 (2)
finite modular pullback membership witnessfinite modular inverse shift

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 ib
  8. L8
    intro ic
  9. L9
    intro vb
  10. L10
    intro vc
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 hT
  7. L17
    intro hI
  8. L18
    intro hV
  9. L19
    intro z
  10. L20
    intro hz
03Establish hsourceL21–30

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

  1. L21
    have hsource : (BetaAt(vb,vc,z,1) → ∃ x. ModularSetMember(ib,ic,p,x) ∧ ModEq(p,z + t,x)) ∧ ((∃ x. ModularSetMember(ib,ic,p,x) ∧ ModEq(p,z + t,x)) → BetaAt(vb,vc,z,1))Definitions: ModularSetMemberModEqBetaAt
  2. L22
    specialize finite_modular_pullback_membership_witness ib
  3. L23
    specialize finite_modular_pullback_membership_witness ic
  4. L24
    specialize finite_modular_pullback_membership_witness vb
  5. L25
    specialize finite_modular_pullback_membership_witness vc
  6. L26
    specialize finite_modular_pullback_membership_witness p
  7. L27
    specialize finite_modular_pullback_membership_witness t
  8. L28
    specialize finite_modular_pullback_membership_witness z
  9. L29
    apply finite_modular_pullback_membership_witness
  10. L30
    exact hp
04Use earlier factsL31–32

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

  1. L31
    exact hV
  2. L32
    exact hz
05Separate the logical casesL33–34

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

  1. L33
    cases hsource
  2. L34
    split
06Fix variables and assumptionsL35–35

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

  1. L35
    intro hmember
07Establish hwL36–38

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

  1. L36
    have hw : 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)) * ic)) /\ exists fs_q_fms_member. ib = fs_q_fms_member * S ((S (a)) * ic) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)
  2. L37
    apply hsource_left
  3. L38
    exact hmember
08Separate the logical casesL39–41

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

  1. L39
    cases hw
  2. L40
    cases hw_witness
  3. L41
    cases hw_witness_left
09Establish hinterL42–45

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

  1. L42
    have hinter : (BetaAt(ib,ic,x,1) → BetaAt(b,c,x,1) ∧ BetaAt(tb,tc,x,1)) ∧ (BetaAt(b,c,x,1) ∧ BetaAt(tb,tc,x,1) → BetaAt(ib,ic,x,1))Definitions: BetaAt
  2. L43
    specialize hI x
  3. L44
    apply hI
  4. L45
    exact hw_witness_left_left
10Separate the logical casesL46–46

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

  1. L46
    cases hinter
11Establish hbothL47–49

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

  1. L47
    have hboth : (((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1)))
  2. L48
    apply hinter_left
  3. L49
    exact hw_witness_left_right
12Separate the logical casesL50–50

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

  1. L50
    cases hboth
13Establish hbackL51–60

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

  1. L51
    have hback : (BetaAt(tb,tc,x,1) → BetaAt(d,e,z,1)) ∧ (BetaAt(d,e,z,1) → BetaAt(tb,tc,x,1))Definitions: BetaAt
  2. L52
    specialize hT x
  3. L53
    specialize hT z
  4. L54
    apply hT
  5. L55
    exact hw_witness_left_left
  6. L56
    exact hz
  7. L57
    specialize finite_modular_inverse_shift p
  8. L58
    specialize finite_modular_inverse_shift t
  9. L59
    specialize finite_modular_inverse_shift v
  10. L60
    specialize finite_modular_inverse_shift z
14Use earlier factsL61–64

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

  1. L61
    specialize finite_modular_inverse_shift x
  2. L62
    apply finite_modular_inverse_shift
  3. L63
    exact htv
  4. L64
    exact hw_witness_right
15Separate the logical casesL65–66

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

  1. L65
    cases hback
  2. L66
    split
16Use earlier factsL67–68

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

  1. L67
    apply hback_left
  2. L68
    exact hboth_right
17Construct an explicit witnessL69–69

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

  1. L69
    exists x
18Separate the logical casesL70–71

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

  1. L70
    split
  2. L71
    split
19Use earlier factsL72–74

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

  1. L72
    exact hw_witness_left_left
  2. L73
    exact hboth_left
  3. L74
    exact hw_witness_right
20Fix variables and assumptionsL75–75

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

  1. L75
    intro hmember
21Separate the logical casesL76–79

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

  1. L76
    cases hmember
  2. L77
    cases hmember_right
  3. L78
    cases hmember_right_witness
  4. L79
    cases hmember_right_witness_left
22Establish hinterL80–83

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

  1. L80
    have hinter : (BetaAt(ib,ic,x,1) → BetaAt(b,c,x,1) ∧ BetaAt(tb,tc,x,1)) ∧ (BetaAt(b,c,x,1) ∧ BetaAt(tb,tc,x,1) → BetaAt(ib,ic,x,1))Definitions: BetaAt
  2. L81
    specialize hI x
  3. L82
    apply hI
  4. L83
    exact hmember_right_witness_left_left
23Separate the logical casesL84–84

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

  1. L84
    cases hinter
24Establish hbackL85–94

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

  1. L85
    have hback : (BetaAt(tb,tc,x,1) → BetaAt(d,e,z,1)) ∧ (BetaAt(d,e,z,1) → BetaAt(tb,tc,x,1))Definitions: BetaAt
  2. L86
    specialize hT x
  3. L87
    specialize hT z
  4. L88
    apply hT
  5. L89
    exact hmember_right_witness_left_left
  6. L90
    exact hz
  7. L91
    specialize finite_modular_inverse_shift p
  8. L92
    specialize finite_modular_inverse_shift t
  9. L93
    specialize finite_modular_inverse_shift v
  10. L94
    specialize finite_modular_inverse_shift z
25Use earlier factsL95–98

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

  1. L95
    specialize finite_modular_inverse_shift x
  2. L96
    apply finite_modular_inverse_shift
  3. L97
    exact htv
  4. L98
    exact hmember_right_witness_right
26Separate the logical casesL99–99

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

  1. L99
    cases hback
27Use earlier factsL100–100

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

  1. L100
    apply hsource_right
28Construct an explicit witnessL101–101

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

  1. L101
    exists x
29Separate the logical casesL102–103

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

  1. L102
    split
  2. L103
    split
30Use earlier factsL104–105

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

  1. L104
    exact hmember_right_witness_left_left
  2. L105
    apply hinter_right
31Separate the logical casesL106–106

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

  1. L106
    split
32Use earlier factsL107–110

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

  1. L107
    exact hmember_right_witness_left_right
  2. L108
    apply hback_right
  3. L109
    exact hmember_left
  4. L110
    exact hmember_right_witness_right

Library-wide reading audit

Original exact command ledger · 110 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro tb
  6. 0006intro tc
  7. 0007intro ib
  8. 0008intro ic
  9. 0009intro vb
  10. 0010intro vc
  11. 0011intro p
  12. 0012intro t
  13. 0013intro v
  14. 0014intro hp
  15. 0015intro htv
  16. 0016intro hT
  17. 0017intro hI
  18. 0018intro hV
  19. 0019intro z
  20. 0020intro hz
  21. 0021have hsource : (((((exists fs_h_cd_lower_V. fs_h_cd_lower_V + S (1) = S ((S (z)) * vc)) /\ exists fs_q_cd_lower_V. vb = fs_q_cd_lower_V * S ((S (z)) * vc) + (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)) * ic)) /\ exists fs_q_fms_member. ib = fs_q_fms_member * S ((S (a)) * ic) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (a) + (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)) * ic)) /\ exists fs_q_fms_member. ib = fs_q_fms_member * S ((S (a)) * ic) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)) -> (((exists fs_h_cd_lower_V. fs_h_cd_lower_V + S (1) = S ((S (z)) * vc)) /\ exists fs_q_cd_lower_V. vb = fs_q_cd_lower_V * S ((S (z)) * vc) + (1)))))
  22. 0022specialize finite_modular_pullback_membership_witness ib
  23. 0023specialize finite_modular_pullback_membership_witness ic
  24. 0024specialize finite_modular_pullback_membership_witness vb
  25. 0025specialize finite_modular_pullback_membership_witness vc
  26. 0026specialize finite_modular_pullback_membership_witness p
  27. 0027specialize finite_modular_pullback_membership_witness t
  28. 0028specialize finite_modular_pullback_membership_witness z
  29. 0029apply finite_modular_pullback_membership_witness
  30. 0030exact hp
  31. 0031exact hV
  32. 0032exact hz
  33. 0033cases hsource
  34. 0034split
  35. 0035intro hmember
  36. 0036have hw : 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)) * ic)) /\ exists fs_q_fms_member. ib = fs_q_fms_member * S ((S (a)) * ic) + (1))))) /\ (exists fms_u_mod fms_v_mod. (z+t) + (p) * fms_u_mod = (a) + (p) * fms_v_mod)
  37. 0037apply hsource_left
  38. 0038exact hmember
  39. 0039cases hw
  40. 0040cases hw_witness
  41. 0041cases hw_witness_left
  42. 0042have hinter : (((((exists fs_h_cd_lower_I. fs_h_cd_lower_I + S (1) = S ((S (x)) * ic)) /\ exists fs_q_cd_lower_I. ib = fs_q_cd_lower_I * S ((S (x)) * ic) + (1))) -> ((((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1))))) /\ (((((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1)))) -> (((exists fs_h_cd_lower_I. fs_h_cd_lower_I + S (1) = S ((S (x)) * ic)) /\ exists fs_q_cd_lower_I. ib = fs_q_cd_lower_I * S ((S (x)) * ic) + (1)))))
  43. 0043specialize hI x
  44. 0044apply hI
  45. 0045exact hw_witness_left_left
  46. 0046cases hinter
  47. 0047have hboth : (((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1)))
  48. 0048apply hinter_left
  49. 0049exact hw_witness_left_right
  50. 0050cases hboth
  51. 0051have hback : (((((exists fs_h_cd_lower_T. fs_h_cd_lower_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_lower_T. tb = fs_q_cd_lower_T * S ((S (x)) * tc) + (1))) -> (((exists fs_h_cd_lower_B. fs_h_cd_lower_B + S (1) = S ((S (z)) * e)) /\ exists fs_q_cd_lower_B. d = fs_q_cd_lower_B * S ((S (z)) * e) + (1)))) /\ ((((exists fs_h_cd_lower_B. fs_h_cd_lower_B + S (1) = S ((S (z)) * e)) /\ exists fs_q_cd_lower_B. d = fs_q_cd_lower_B * S ((S (z)) * e) + (1))) -> (((exists fs_h_cd_lower_T. fs_h_cd_lower_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_lower_T. tb = fs_q_cd_lower_T * S ((S (x)) * tc) + (1)))))
  52. 0052specialize hT x
  53. 0053specialize hT z
  54. 0054apply hT
  55. 0055exact hw_witness_left_left
  56. 0056exact hz
  57. 0057specialize finite_modular_inverse_shift p
  58. 0058specialize finite_modular_inverse_shift t
  59. 0059specialize finite_modular_inverse_shift v
  60. 0060specialize finite_modular_inverse_shift z
  61. 0061specialize finite_modular_inverse_shift x
  62. 0062apply finite_modular_inverse_shift
  63. 0063exact htv
  64. 0064exact hw_witness_right
  65. 0065cases hback
  66. 0066split
  67. 0067apply hback_left
  68. 0068exact hboth_right
  69. 0069exists x
  70. 0070split
  71. 0071split
  72. 0072exact hw_witness_left_left
  73. 0073exact hboth_left
  74. 0074exact hw_witness_right
  75. 0075intro hmember
  76. 0076cases hmember
  77. 0077cases hmember_right
  78. 0078cases hmember_right_witness
  79. 0079cases hmember_right_witness_left
  80. 0080have hinter : (((((exists fs_h_cd_lower_back_I. fs_h_cd_lower_back_I + S (1) = S ((S (x)) * ic)) /\ exists fs_q_cd_lower_back_I. ib = fs_q_cd_lower_back_I * S ((S (x)) * ic) + (1))) -> ((((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1))))) /\ (((((exists fs_h_cd_I_A. fs_h_cd_I_A + S (1) = S ((S (x)) * c)) /\ exists fs_q_cd_I_A. b = fs_q_cd_I_A * S ((S (x)) * c) + (1))) /\ (((exists fs_h_cd_I_T. fs_h_cd_I_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_I_T. tb = fs_q_cd_I_T * S ((S (x)) * tc) + (1)))) -> (((exists fs_h_cd_lower_back_I. fs_h_cd_lower_back_I + S (1) = S ((S (x)) * ic)) /\ exists fs_q_cd_lower_back_I. ib = fs_q_cd_lower_back_I * S ((S (x)) * ic) + (1)))))
  81. 0081specialize hI x
  82. 0082apply hI
  83. 0083exact hmember_right_witness_left_left
  84. 0084cases hinter
  85. 0085have hback : (((((exists fs_h_cd_lower_back_T. fs_h_cd_lower_back_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_lower_back_T. tb = fs_q_cd_lower_back_T * S ((S (x)) * tc) + (1))) -> (((exists fs_h_cd_lower_back_B. fs_h_cd_lower_back_B + S (1) = S ((S (z)) * e)) /\ exists fs_q_cd_lower_back_B. d = fs_q_cd_lower_back_B * S ((S (z)) * e) + (1)))) /\ ((((exists fs_h_cd_lower_back_B. fs_h_cd_lower_back_B + S (1) = S ((S (z)) * e)) /\ exists fs_q_cd_lower_back_B. d = fs_q_cd_lower_back_B * S ((S (z)) * e) + (1))) -> (((exists fs_h_cd_lower_back_T. fs_h_cd_lower_back_T + S (1) = S ((S (x)) * tc)) /\ exists fs_q_cd_lower_back_T. tb = fs_q_cd_lower_back_T * S ((S (x)) * tc) + (1)))))
  86. 0086specialize hT x
  87. 0087specialize hT z
  88. 0088apply hT
  89. 0089exact hmember_right_witness_left_left
  90. 0090exact hz
  91. 0091specialize finite_modular_inverse_shift p
  92. 0092specialize finite_modular_inverse_shift t
  93. 0093specialize finite_modular_inverse_shift v
  94. 0094specialize finite_modular_inverse_shift z
  95. 0095specialize finite_modular_inverse_shift x
  96. 0096apply finite_modular_inverse_shift
  97. 0097exact htv
  98. 0098exact hmember_right_witness_right
  99. 0099cases hback
  100. 0100apply hsource_right
  101. 0101exists x
  102. 0102split
  103. 0103split
  104. 0104exact hmember_right_witness_left_left
  105. 0105apply hinter_right
  106. 0106split
  107. 0107exact hmember_right_witness_left_right
  108. 0108apply hback_right
  109. 0109exact hmember_left
  110. 0110exact hmember_right_witness_right