CD0027

finite_modular_pullback_membership_witness

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

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

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

Definition DAG

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

Actual proof prerequisites

finite_modular_residue_exists
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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 (1)
finite modular residue exists
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 : ∃ j. Lt(j,p) ∧ ModEq(p,i + t,j)Definitions: Lt(j,p)ModEq(p,i + t,j)Original native command in the exact edition
  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 : (BetaAt(z,d,i,1) → BetaAt(b,c,x,1)) ∧ (BetaAt(b,c,x,1) → BetaAt(z,d,i,1))Definitions: BetaAt(z,d,i,1)BetaAt(b,c,x,1)Original native command in the exact edition
  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(z,d,i,1)BetaAt(b,c,x,1)Original native command in the exact edition
  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 defined 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 : ∃ j. Lt(j,p) ∧ ModEq(p,i + t,j)
  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 : (BetaAt(z,d,i,1) → BetaAt(b,c,x,1)) ∧ (BetaAt(b,c,x,1) → BetaAt(z,d,i,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 : (BetaAt(z,d,i,1) → BetaAt(b,c,x,1)) ∧ (BetaAt(b,c,x,1) → BetaAt(z,d,i,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