CD0027

finite_modular_pullback_membership_witness

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

Exact pullback membership constructs and reflects an actual canonical source member.

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 z d p t i. ~(p=0) -> (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)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1))) -> (((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1)))) /\ ((((exists fs_h_fms_pullback_source. fs_h_fms_pullback_source + S (1) = S ((S (fms_j_pullback)) * c)) /\ exists fs_q_fms_pullback_source. b = fs_q_fms_pullback_source * S ((S (fms_j_pullback)) * c) + (1))) -> (((exists fs_h_fms_pullback_target. fs_h_fms_pullback_target + S (1) = S ((S (fms_i_pullback)) * d)) /\ exists fs_q_fms_pullback_target. z = fs_q_fms_pullback_target * S ((S (fms_i_pullback)) * d) + (1))))))) -> (exists fms_gap_lt. fms_gap_lt + S (i) = (p)) -> ((((((exists fs_h_fms_pull_member. fs_h_fms_pull_member + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_member. z = fs_q_fms_pull_member * S ((S (i)) * d) + (1))) -> (exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod))) /\ ((exists j. (((exists fms_gap_member. fms_gap_member + S (j) = (p)) /\ (((exists fs_h_fms_member. fs_h_fms_member + S (1) = S ((S (j)) * c)) /\ exists fs_q_fms_member. b = fs_q_fms_member * S ((S (j)) * c) + (1))))) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)) -> (((exists fs_h_fms_pull_member. fs_h_fms_pull_member + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_member. z = fs_q_fms_pull_member * S ((S (i)) * d) + (1))))))

Constructive proof overview

Generated structural guide

Exact pullback membership constructs and reflects an actual canonical source member.

The unchanged tactic script uses 1 declared prerequisite and contains 48 exact native proof lines.

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

Proof neighborhood

Direct dependencies

CD0024 finite_modular_residue_exists

Direct dependents

CD0028 finite_modular_pushforward_membership_witness CD0037 finite_modular_dyson_lower_from_pullback CD0045 finite_modular_opposite_translates_sum_cover

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

48 script commands · 15 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 residue exists

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 z
  4. L4
    intro d
  5. L5
    intro p
  6. L6
    intro t
  7. L7
    intro i
  8. L8
    intro hp
  9. L9
    intro hpull
  10. L10
    intro hi
02Separate the logical casesL11–11

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

  1. L11
    split
03Fix variables and assumptionsL12–12

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

  1. L12
    intro ht
04Establish hjL13–17

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

  1. L13
    have hj : exists j. (exists fms_gap_lt. fms_gap_lt + S (j) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  2. L14
    specialize finite_modular_residue_exists p
  3. L15
    specialize finite_modular_residue_exists i+t
  4. L16
    apply finite_modular_residue_exists
  5. L17
    exact hp
05Separate the logical casesL18–19

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

  1. L18
    cases hj
  2. L19
    cases hj_witness
06Establish heL20–26

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

  1. L20
    have he : (((((exists fs_h_fms_pull_t. fs_h_fms_pull_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_t. z = fs_q_fms_pull_t * S ((S (i)) * d) + (1))) -> (((exists fs_h_fms_pull_s. fs_h_fms_pull_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_s. b = fs_q_fms_pull_s * S ((S (x)) * c) + (1)))) /\ ((((exists fs_h_fms_pull_s. fs_h_fms_pull_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_s. b = fs_q_fms_pull_s * S ((S (x)) * c) + (1))) -> (((exists fs_h_fms_pull_t. fs_h_fms_pull_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_t. z = fs_q_fms_pull_t * S ((S (i)) * d) + (1)))))
  2. L21
    specialize hpull i
  3. L22
    specialize hpull x
  4. L23
    apply hpull
  5. L24
    exact hi
  6. L25
    exact hj_witness_left
  7. L26
    exact hj_witness_right
07Separate the logical casesL27–27

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

  1. L27
    cases he
08Construct an explicit witnessL28–28

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

  1. L28
    exists x
09Separate the logical casesL29–30

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

  1. L29
    split
  2. L30
    split
10Use earlier factsL31–34

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

  1. L31
    exact hj_witness_left
  2. L32
    apply he_left
  3. L33
    exact ht
  4. L34
    exact hj_witness_right
11Fix variables and assumptionsL35–35

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

  1. L35
    intro hw
12Separate the logical casesL36–38

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

  1. L36
    cases hw
  2. L37
    cases hw_witness
  3. L38
    cases hw_witness_left
13Establish heL39–45

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

  1. L39
    have he : (BetaAt(z,d,i,1) → BetaAt(b,c,x,1)) ∧ (BetaAt(b,c,x,1) → BetaAt(z,d,i,1))Definitions: BetaAt
  2. L40
    specialize hpull i
  3. L41
    specialize hpull x
  4. L42
    apply hpull
  5. L43
    exact hi
  6. L44
    exact hw_witness_left_left
  7. L45
    exact hw_witness_right
14Separate the logical casesL46–46

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

  1. L46
    cases he
15Use earlier factsL47–48

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

  1. L47
    apply he_right
  2. L48
    exact hw_witness_left_right

Library-wide reading audit

Original exact command ledger · 48 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro p
  6. 0006intro t
  7. 0007intro i
  8. 0008intro hp
  9. 0009intro hpull
  10. 0010intro hi
  11. 0011split
  12. 0012intro ht
  13. 0013have hj : exists j. (exists fms_gap_lt. fms_gap_lt + S (j) = (p)) /\ (exists fms_u_mod fms_v_mod. (i+t) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  14. 0014specialize finite_modular_residue_exists p
  15. 0015specialize finite_modular_residue_exists i+t
  16. 0016apply finite_modular_residue_exists
  17. 0017exact hp
  18. 0018cases hj
  19. 0019cases hj_witness
  20. 0020have he : (((((exists fs_h_fms_pull_t. fs_h_fms_pull_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_t. z = fs_q_fms_pull_t * S ((S (i)) * d) + (1))) -> (((exists fs_h_fms_pull_s. fs_h_fms_pull_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_s. b = fs_q_fms_pull_s * S ((S (x)) * c) + (1)))) /\ ((((exists fs_h_fms_pull_s. fs_h_fms_pull_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_s. b = fs_q_fms_pull_s * S ((S (x)) * c) + (1))) -> (((exists fs_h_fms_pull_t. fs_h_fms_pull_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_t. z = fs_q_fms_pull_t * S ((S (i)) * d) + (1)))))
  21. 0021specialize hpull i
  22. 0022specialize hpull x
  23. 0023apply hpull
  24. 0024exact hi
  25. 0025exact hj_witness_left
  26. 0026exact hj_witness_right
  27. 0027cases he
  28. 0028exists x
  29. 0029split
  30. 0030split
  31. 0031exact hj_witness_left
  32. 0032apply he_left
  33. 0033exact ht
  34. 0034exact hj_witness_right
  35. 0035intro hw
  36. 0036cases hw
  37. 0037cases hw_witness
  38. 0038cases hw_witness_left
  39. 0039have he : (((((exists fs_h_fms_pull_back_t. fs_h_fms_pull_back_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_back_t. z = fs_q_fms_pull_back_t * S ((S (i)) * d) + (1))) -> (((exists fs_h_fms_pull_back_s. fs_h_fms_pull_back_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_back_s. b = fs_q_fms_pull_back_s * S ((S (x)) * c) + (1)))) /\ ((((exists fs_h_fms_pull_back_s. fs_h_fms_pull_back_s + S (1) = S ((S (x)) * c)) /\ exists fs_q_fms_pull_back_s. b = fs_q_fms_pull_back_s * S ((S (x)) * c) + (1))) -> (((exists fs_h_fms_pull_back_t. fs_h_fms_pull_back_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_pull_back_t. z = fs_q_fms_pull_back_t * S ((S (i)) * d) + (1)))))
  40. 0040specialize hpull i
  41. 0041specialize hpull x
  42. 0042apply hpull
  43. 0043exact hi
  44. 0044exact hw_witness_left_left
  45. 0045exact hw_witness_right
  46. 0046cases he
  47. 0047apply he_right
  48. 0048exact hw_witness_left_right