CD0028

finite_modular_pushforward_membership_witness

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

A coded inverse pullback is exactly the forward translate, with actual source-member 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 z d p t v i. ~(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)) * 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_push_member. fs_h_fms_push_member + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_push_member. z = fs_q_fms_push_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. (j+t) + (p) * fms_u_mod = (i) + (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. (j+t) + (p) * fms_u_mod = (i) + (p) * fms_v_mod)) -> (((exists fs_h_fms_push_member. fs_h_fms_push_member + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_push_member. z = fs_q_fms_push_member * S ((S (i)) * d) + (1))))))

Constructive proof overview

Generated structural guide

A coded inverse pullback is exactly the forward translate, with actual source-member witnesses.

The unchanged tactic script uses 3 declared prerequisites and contains 62 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 add_comm Stable theorem; checked-use authorized

Direct dependents

CD002E finite_partial_sumset_succ_present CD0036 finite_modular_dyson_upper_from_union 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

62 script commands · 19 reading checkpoints · 2 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 z
  4. L4
    intro d
  5. L5
    intro p
  6. L6
    intro t
  7. L7
    intro v
  8. L8
    intro i
  9. L9
    intro hp
  10. L10
    intro htv
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hpull
  2. L12
    intro hi
03Establish heL13–22

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

  1. L13
    have he : (BetaAt(z,d,i,1) → ∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,i + v,x)) ∧ ((∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,i + v,x)) → BetaAt(z,d,i,1))Definitions: ModularSetMemberModEqBetaAt
  2. L14
    specialize finite_modular_pullback_membership_witness b
  3. L15
    specialize finite_modular_pullback_membership_witness c
  4. L16
    specialize finite_modular_pullback_membership_witness z
  5. L17
    specialize finite_modular_pullback_membership_witness d
  6. L18
    specialize finite_modular_pullback_membership_witness p
  7. L19
    specialize finite_modular_pullback_membership_witness v
  8. L20
    specialize finite_modular_pullback_membership_witness i
  9. L21
    apply finite_modular_pullback_membership_witness
  10. L22
    exact hp
04Use earlier factsL23–24

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

  1. L23
    exact hpull
  2. L24
    exact hi
05Separate the logical casesL25–26

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

  1. L25
    cases he
  2. L26
    split
06Fix variables and assumptionsL27–27

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

  1. L27
    intro ht
07Establish hwL28–30

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

  1. L28
    have hw : 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+v) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  2. L29
    apply he_left
  3. L30
    exact ht
08Separate the logical casesL31–32

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

  1. L31
    cases hw
  2. L32
    cases hw_witness
09Construct an explicit witnessL33–33

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

  1. L33
    exists x
10Separate the logical casesL34–34

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

  1. L34
    split
11Use earlier factsL35–41

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

  1. L35
    exact hw_witness_left
  2. L36
    specialize finite_modular_inverse_shift p
  3. L37
    specialize finite_modular_inverse_shift v
  4. L38
    specialize finite_modular_inverse_shift t
  5. L39
    specialize finite_modular_inverse_shift i
  6. L40
    specialize finite_modular_inverse_shift x
  7. L41
    apply finite_modular_inverse_shift
12Calculate and transport equalitiesL42–42

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L42
    trans t+v
13Use earlier factsL43–47

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

  1. L43
    specialize add_comm v
  2. L44
    specialize add_comm t
  3. L45
    apply add_comm
  4. L46
    exact htv
  5. L47
    exact hw_witness_right
14Fix variables and assumptionsL48–48

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

  1. L48
    intro hw
15Separate the logical casesL49–50

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

  1. L49
    cases hw
  2. L50
    cases hw_witness
16Use earlier factsL51–51

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

  1. L51
    apply he_right
17Construct an explicit witnessL52–52

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

  1. L52
    exists x
18Separate the logical casesL53–53

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

  1. L53
    split
19Use earlier factsL54–62

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

  1. L54
    exact hw_witness_left
  2. L55
    specialize finite_modular_inverse_shift p
  3. L56
    specialize finite_modular_inverse_shift t
  4. L57
    specialize finite_modular_inverse_shift v
  5. L58
    specialize finite_modular_inverse_shift x
  6. L59
    specialize finite_modular_inverse_shift i
  7. L60
    apply finite_modular_inverse_shift
  8. L61
    exact htv
  9. L62
    exact hw_witness_right

Library-wide reading audit

Original exact command ledger · 62 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro z
  4. 0004intro d
  5. 0005intro p
  6. 0006intro t
  7. 0007intro v
  8. 0008intro i
  9. 0009intro hp
  10. 0010intro htv
  11. 0011intro hpull
  12. 0012intro hi
  13. 0013have he : (((((exists fs_h_fms_push_t. fs_h_fms_push_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_push_t. z = fs_q_fms_push_t * 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+v) + (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+v) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)) -> (((exists fs_h_fms_push_t. fs_h_fms_push_t + S (1) = S ((S (i)) * d)) /\ exists fs_q_fms_push_t. z = fs_q_fms_push_t * S ((S (i)) * d) + (1)))))
  14. 0014specialize finite_modular_pullback_membership_witness b
  15. 0015specialize finite_modular_pullback_membership_witness c
  16. 0016specialize finite_modular_pullback_membership_witness z
  17. 0017specialize finite_modular_pullback_membership_witness d
  18. 0018specialize finite_modular_pullback_membership_witness p
  19. 0019specialize finite_modular_pullback_membership_witness v
  20. 0020specialize finite_modular_pullback_membership_witness i
  21. 0021apply finite_modular_pullback_membership_witness
  22. 0022exact hp
  23. 0023exact hpull
  24. 0024exact hi
  25. 0025cases he
  26. 0026split
  27. 0027intro ht
  28. 0028have hw : 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+v) + (p) * fms_u_mod = (j) + (p) * fms_v_mod)
  29. 0029apply he_left
  30. 0030exact ht
  31. 0031cases hw
  32. 0032cases hw_witness
  33. 0033exists x
  34. 0034split
  35. 0035exact hw_witness_left
  36. 0036specialize finite_modular_inverse_shift p
  37. 0037specialize finite_modular_inverse_shift v
  38. 0038specialize finite_modular_inverse_shift t
  39. 0039specialize finite_modular_inverse_shift i
  40. 0040specialize finite_modular_inverse_shift x
  41. 0041apply finite_modular_inverse_shift
  42. 0042trans t+v
  43. 0043specialize add_comm v
  44. 0044specialize add_comm t
  45. 0045apply add_comm
  46. 0046exact htv
  47. 0047exact hw_witness_right
  48. 0048intro hw
  49. 0049cases hw
  50. 0050cases hw_witness
  51. 0051apply he_right
  52. 0052exists x
  53. 0053split
  54. 0054exact hw_witness_left
  55. 0055specialize finite_modular_inverse_shift p
  56. 0056specialize finite_modular_inverse_shift t
  57. 0057specialize finite_modular_inverse_shift v
  58. 0058specialize finite_modular_inverse_shift x
  59. 0059specialize finite_modular_inverse_shift i
  60. 0060apply finite_modular_inverse_shift
  61. 0061exact htv
  62. 0062exact hw_witness_right