CD0028

finite_modular_pushforward_membership_witness

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

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. ∀ z. ∀ d. ∀ p. ∀ t. ∀ v. ∀ i. ¬p = 0 → t + v = p → ModularSetPullback(b,c,z,d,p,v) → Lt(i,p) → (BetaAt(z,d,i,1) → ∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + t,i)) ∧ ((∃ x. ModularSetMember(b,c,p,x) ∧ ModEq(p,x + t,i)) → BetaAt(z,d,i,1))

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

Definition DAG

ModularSetMember(b,c,p,x) · 5ModularSetPullback(b,c,d,e,p,t) · 1Lt(a,b) · 1ModEq(m,a,b) · 5BetaAt(b,c,i,x) · 4

Actual proof prerequisites

finite_modular_pullback_membership_witnessfinite_modular_inverse_shiftadd_comm · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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 (2)
finite modular pullback membership witnessfinite modular inverse shift
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: BetaAt(z,d,i,1)ModularSetMember(b,c,p,x)ModEq(p,i + v,x)Original native command in the exact edition
  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 : ∃ j. ModularSetMember(b,c,p,j) ∧ ModEq(p,i + v,j)Definitions: ModularSetMember(b,c,p,j)ModEq(p,i + v,j)Original native command in the exact edition
  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 defined 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 : (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))
  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 : ∃ j. ModularSetMember(b,c,p,j) ∧ ModEq(p,i + v,j)
  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