AF0014

factor_permutation_swap_all_prime

A genuine index swap retains every prime factor, including duplicate equal primes; no distinct-factor hypothesis is required.

Alpha v34 checked-use · first admitted v28 · 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.

The original division, gcd, cancellation, and factor-existence foundations are exposed through checked wrappers. Unordered uniqueness adds an actual bounded, injective, surjective index map matching repeated prime occurrences. The empty factor list represents one, not zero.

Exact theorem in conservative defined notation

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ i. ∀ p. ∀ q. Lt(i,l) → AllPrime(b,c,S l) → BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))))) → AllPrime(d,e,S l)

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

Definition DAG

Lt(a,b) · 3BetaAt(b,c,i,x) · 13AllPrime(b,c,l) · 2

Actual proof prerequisites

eq_decidable · checked external prerequisitebeta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisitefactor_permutation_all_prime_entryfactor_permutation_swap_reflect_unchangedle_refl · checked external prerequisitele_succ · checked external prerequisite
Original expanded first-order statement 
forall b c d e l i p q. (exists pfp_gap_prime_swap_index. pfp_gap_prime_swap_index + S (i) = (l)) -> (forall ftsf_index_fsat_prime_swap_old. (exists ftsf_gap_fsat_prime_swap_old_bound. ftsf_gap_fsat_prime_swap_old_bound + S ftsf_index_fsat_prime_swap_old = (S l)) -> exists ftsf_factor_fsat_prime_swap_old. ((((exists ff_h_ftsf_fsat_prime_swap_old_entry. ff_h_ftsf_fsat_prime_swap_old_entry + S (ftsf_factor_fsat_prime_swap_old) = S ((S (ftsf_index_fsat_prime_swap_old)) * c)) /\ exists ff_q_ftsf_fsat_prime_swap_old_entry. b = ff_q_ftsf_fsat_prime_swap_old_entry * S ((S (ftsf_index_fsat_prime_swap_old)) * c) + (ftsf_factor_fsat_prime_swap_old))) /\ ((~(ftsf_factor_fsat_prime_swap_old = 1) /\ forall frm_prime_left_ftsf_fsat_prime_swap_old_prime frm_prime_right_ftsf_fsat_prime_swap_old_prime. ftsf_factor_fsat_prime_swap_old = frm_prime_left_ftsf_fsat_prime_swap_old_prime * frm_prime_right_ftsf_fsat_prime_swap_old_prime -> frm_prime_left_ftsf_fsat_prime_swap_old_prime = 1 \/ frm_prime_right_ftsf_fsat_prime_swap_old_prime = 1)))) -> (((((exists ff_h_pfp_swapoldi. ff_h_pfp_swapoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swapoldi. b = ff_q_pfp_swapoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swapoldlast. ff_h_pfp_swapoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swapoldlast. b = ff_q_pfp_swapoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swapnewi. ff_h_pfp_swapnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swapnewi. d = ff_q_pfp_swapnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swapnewlast. ff_h_pfp_swapnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swapnewlast. d = ff_q_pfp_swapnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap pfp_a_swap. (exists pfp_gap_swapbound. pfp_gap_swapbound + S (pfp_j_swap) = (S (l))) -> ~(pfp_j_swap = i) -> ~(pfp_j_swap = l) -> (((exists ff_h_pfp_swapold. ff_h_pfp_swapold + S (pfp_a_swap) = S ((S (pfp_j_swap)) * c)) /\ exists ff_q_pfp_swapold. b = ff_q_pfp_swapold * S ((S (pfp_j_swap)) * c) + (pfp_a_swap))) -> (((exists ff_h_pfp_swapnew. ff_h_pfp_swapnew + S (pfp_a_swap) = S ((S (pfp_j_swap)) * e)) /\ exists ff_q_pfp_swapnew. d = ff_q_pfp_swapnew * S ((S (pfp_j_swap)) * e) + (pfp_a_swap)))))))))))) -> (forall ftsf_index_fsat_prime_swap_new. (exists ftsf_gap_fsat_prime_swap_new_bound. ftsf_gap_fsat_prime_swap_new_bound + S ftsf_index_fsat_prime_swap_new = (S l)) -> exists ftsf_factor_fsat_prime_swap_new. ((((exists ff_h_ftsf_fsat_prime_swap_new_entry. ff_h_ftsf_fsat_prime_swap_new_entry + S (ftsf_factor_fsat_prime_swap_new) = S ((S (ftsf_index_fsat_prime_swap_new)) * e)) /\ exists ff_q_ftsf_fsat_prime_swap_new_entry. d = ff_q_ftsf_fsat_prime_swap_new_entry * S ((S (ftsf_index_fsat_prime_swap_new)) * e) + (ftsf_factor_fsat_prime_swap_new))) /\ ((~(ftsf_factor_fsat_prime_swap_new = 1) /\ forall frm_prime_left_ftsf_fsat_prime_swap_new_prime frm_prime_right_ftsf_fsat_prime_swap_new_prime. ftsf_factor_fsat_prime_swap_new = frm_prime_left_ftsf_fsat_prime_swap_new_prime * frm_prime_right_ftsf_fsat_prime_swap_new_prime -> frm_prime_left_ftsf_fsat_prime_swap_new_prime = 1 \/ frm_prime_right_ftsf_fsat_prime_swap_new_prime = 1))))

Complete tactic proof in conservative notation

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

110 script commands · 25 reading checkpoints · 6 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)
factor permutation all prime entryfactor permutation swap reflect unchanged
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 l
  6. L6
    intro i
  7. L7
    intro p
  8. L8
    intro q
  9. L9
    intro hi
  10. L10
    intro hp
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hs
03Establish hcopyL12–13

Establish this local claim before using it. It is not an additional assumption.

  1. L12
    have hcopy : BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)))))Definitions: BetaAt(b,c,i,p)BetaAt(b,c,l,q)BetaAt(d,e,i,q)BetaAt(d,e,l,p)Lt(x,S l)BetaAt(b,c,x,y)BetaAt(d,e,x,y)Original native command in the exact edition
  2. L13
    exact hs
04Separate the logical casesL14–17

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

  1. L14
    cases hcopy
  2. L15
    cases hcopy_right
  3. L16
    cases hcopy_right_right
  4. L17
    cases hcopy_right_right_right
05Fix variables and assumptionsL18–19

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

  1. L18
    intro k
  2. L19
    intro hk
06Establish hvalueL20–24

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

  1. L20
    have hvalue : ∃ a. BetaAt(d,e,k,a)Definitions: BetaAt(d,e,k,a)Original native command in the exact edition
  2. L21
    specialize beta_at_exists (d)
  3. L22
    specialize beta_at_exists (e)
  4. L23
    specialize beta_at_exists (k)
  5. L24
    apply beta_at_exists
07Separate the logical casesL25–25

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

  1. L25
    cases hvalue
08Construct an explicit witnessL26–26

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

  1. L26
    exists x
09Separate the logical casesL27–27

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

  1. L27
    split
10Use earlier factsL28–28

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

  1. L28
    exact hvalue_witness
11Establish hcaseL29–32

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

  1. L29
    have hcase : k = i \/ ~(k = i)
  2. L30
    specialize eq_decidable (k)
  3. L31
    specialize eq_decidable (i)
  4. L32
    apply eq_decidable
12Separate the logical casesL33–33

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

  1. L33
    cases hcase
13Establish heqL34–43

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

  1. L34
    have heq : x = q
  2. L35
    specialize beta_at_unique (d)
  3. L36
    specialize beta_at_unique (e)
  4. L37
    specialize beta_at_unique (i)
  5. L38
    specialize beta_at_unique (x)
  6. L39
    specialize beta_at_unique (q)
  7. L40
    apply beta_at_unique
  8. L41
    rewrite hcase_left at hvalue_witness
  9. L42
    rewrite hcase_left at hvalue_witness
  10. L43
    exact hvalue_witness
14Use earlier factsL44–44

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

  1. L44
    exact hcopy_right_right_left
15Calculate and transport equalitiesL45–46

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

  1. L45
    rewrite heq
  2. L46
    rewrite heq
16Use earlier factsL47–56

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

  1. L47
    specialize factor_permutation_all_prime_entry (b)
  2. L48
    specialize factor_permutation_all_prime_entry (c)
  3. L49
    specialize factor_permutation_all_prime_entry (S l)
  4. L50
    specialize factor_permutation_all_prime_entry (l)
  5. L51
    specialize factor_permutation_all_prime_entry (q)
  6. L52
    apply factor_permutation_all_prime_entry
  7. L53
    exact hp
  8. L54
    specialize le_refl (S l)
  9. L55
    apply le_refl
  10. L56
    exact hcopy_right_left
17Establish hlastL57–60

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

  1. L57
    have hlast : k = l \/ ~(k = l)
  2. L58
    specialize eq_decidable (k)
  3. L59
    specialize eq_decidable (l)
  4. L60
    apply eq_decidable
18Separate the logical casesL61–61

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

  1. L61
    cases hlast
19Establish heqL62–71

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

  1. L62
    have heq : x = p
  2. L63
    specialize beta_at_unique (d)
  3. L64
    specialize beta_at_unique (e)
  4. L65
    specialize beta_at_unique (l)
  5. L66
    specialize beta_at_unique (x)
  6. L67
    specialize beta_at_unique (p)
  7. L68
    apply beta_at_unique
  8. L69
    rewrite hlast_left at hvalue_witness
  9. L70
    rewrite hlast_left at hvalue_witness
  10. L71
    exact hvalue_witness
20Use earlier factsL72–72

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

  1. L72
    exact hcopy_right_right_right_left
21Calculate and transport equalitiesL73–74

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

  1. L73
    rewrite heq
  2. L74
    rewrite heq
22Use earlier factsL75–84

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

  1. L75
    specialize factor_permutation_all_prime_entry (b)
  2. L76
    specialize factor_permutation_all_prime_entry (c)
  3. L77
    specialize factor_permutation_all_prime_entry (S l)
  4. L78
    specialize factor_permutation_all_prime_entry (i)
  5. L79
    specialize factor_permutation_all_prime_entry (p)
  6. L80
    apply factor_permutation_all_prime_entry
  7. L81
    exact hp
  8. L82
    specialize le_succ (S i)
  9. L83
    specialize le_succ (l)
  10. L84
    apply le_succ
23Use earlier factsL85–94

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

  1. L85
    exact hi
  2. L86
    exact hcopy_left
  3. L87
    specialize factor_permutation_all_prime_entry (b)
  4. L88
    specialize factor_permutation_all_prime_entry (c)
  5. L89
    specialize factor_permutation_all_prime_entry (S l)
  6. L90
    specialize factor_permutation_all_prime_entry (k)
  7. L91
    specialize factor_permutation_all_prime_entry (x)
  8. L92
    apply factor_permutation_all_prime_entry
  9. L93
    exact hp
  10. L94
    exact hk
24Use earlier factsL95–104

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

  1. L95
    specialize factor_permutation_swap_reflect_unchanged (b)
  2. L96
    specialize factor_permutation_swap_reflect_unchanged (c)
  3. L97
    specialize factor_permutation_swap_reflect_unchanged (d)
  4. L98
    specialize factor_permutation_swap_reflect_unchanged (e)
  5. L99
    specialize factor_permutation_swap_reflect_unchanged (l)
  6. L100
    specialize factor_permutation_swap_reflect_unchanged (i)
  7. L101
    specialize factor_permutation_swap_reflect_unchanged (p)
  8. L102
    specialize factor_permutation_swap_reflect_unchanged (q)
  9. L103
    specialize factor_permutation_swap_reflect_unchanged (k)
  10. L104
    specialize factor_permutation_swap_reflect_unchanged (x)
25Use earlier factsL105–110

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

  1. L105
    apply factor_permutation_swap_reflect_unchanged
  2. L106
    exact hs
  3. L107
    exact hk
  4. L108
    exact hcase_right
  5. L109
    exact hlast_right
  6. L110
    exact hvalue_witness

Library-wide reading audit

Original defined command ledger · 110 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro i
  7. 0007intro p
  8. 0008intro q
  9. 0009intro hi
  10. 0010intro hp
  11. 0011intro hs
  12. 0012have hcopy : BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y)))))
  13. 0013exact hs
  14. 0014cases hcopy
  15. 0015cases hcopy_right
  16. 0016cases hcopy_right_right
  17. 0017cases hcopy_right_right_right
  18. 0018intro k
  19. 0019intro hk
  20. 0020have hvalue : ∃ a. BetaAt(d,e,k,a)
  21. 0021specialize beta_at_exists (d)
  22. 0022specialize beta_at_exists (e)
  23. 0023specialize beta_at_exists (k)
  24. 0024apply beta_at_exists
  25. 0025cases hvalue
  26. 0026exists x
  27. 0027split
  28. 0028exact hvalue_witness
  29. 0029have hcase : k = i \/ ~(k = i)
  30. 0030specialize eq_decidable (k)
  31. 0031specialize eq_decidable (i)
  32. 0032apply eq_decidable
  33. 0033cases hcase
  34. 0034have heq : x = q
  35. 0035specialize beta_at_unique (d)
  36. 0036specialize beta_at_unique (e)
  37. 0037specialize beta_at_unique (i)
  38. 0038specialize beta_at_unique (x)
  39. 0039specialize beta_at_unique (q)
  40. 0040apply beta_at_unique
  41. 0041rewrite hcase_left at hvalue_witness
  42. 0042rewrite hcase_left at hvalue_witness
  43. 0043exact hvalue_witness
  44. 0044exact hcopy_right_right_left
  45. 0045rewrite heq
  46. 0046rewrite heq
  47. 0047specialize factor_permutation_all_prime_entry (b)
  48. 0048specialize factor_permutation_all_prime_entry (c)
  49. 0049specialize factor_permutation_all_prime_entry (S l)
  50. 0050specialize factor_permutation_all_prime_entry (l)
  51. 0051specialize factor_permutation_all_prime_entry (q)
  52. 0052apply factor_permutation_all_prime_entry
  53. 0053exact hp
  54. 0054specialize le_refl (S l)
  55. 0055apply le_refl
  56. 0056exact hcopy_right_left
  57. 0057have hlast : k = l \/ ~(k = l)
  58. 0058specialize eq_decidable (k)
  59. 0059specialize eq_decidable (l)
  60. 0060apply eq_decidable
  61. 0061cases hlast
  62. 0062have heq : x = p
  63. 0063specialize beta_at_unique (d)
  64. 0064specialize beta_at_unique (e)
  65. 0065specialize beta_at_unique (l)
  66. 0066specialize beta_at_unique (x)
  67. 0067specialize beta_at_unique (p)
  68. 0068apply beta_at_unique
  69. 0069rewrite hlast_left at hvalue_witness
  70. 0070rewrite hlast_left at hvalue_witness
  71. 0071exact hvalue_witness
  72. 0072exact hcopy_right_right_right_left
  73. 0073rewrite heq
  74. 0074rewrite heq
  75. 0075specialize factor_permutation_all_prime_entry (b)
  76. 0076specialize factor_permutation_all_prime_entry (c)
  77. 0077specialize factor_permutation_all_prime_entry (S l)
  78. 0078specialize factor_permutation_all_prime_entry (i)
  79. 0079specialize factor_permutation_all_prime_entry (p)
  80. 0080apply factor_permutation_all_prime_entry
  81. 0081exact hp
  82. 0082specialize le_succ (S i)
  83. 0083specialize le_succ (l)
  84. 0084apply le_succ
  85. 0085exact hi
  86. 0086exact hcopy_left
  87. 0087specialize factor_permutation_all_prime_entry (b)
  88. 0088specialize factor_permutation_all_prime_entry (c)
  89. 0089specialize factor_permutation_all_prime_entry (S l)
  90. 0090specialize factor_permutation_all_prime_entry (k)
  91. 0091specialize factor_permutation_all_prime_entry (x)
  92. 0092apply factor_permutation_all_prime_entry
  93. 0093exact hp
  94. 0094exact hk
  95. 0095specialize factor_permutation_swap_reflect_unchanged (b)
  96. 0096specialize factor_permutation_swap_reflect_unchanged (c)
  97. 0097specialize factor_permutation_swap_reflect_unchanged (d)
  98. 0098specialize factor_permutation_swap_reflect_unchanged (e)
  99. 0099specialize factor_permutation_swap_reflect_unchanged (l)
  100. 0100specialize factor_permutation_swap_reflect_unchanged (i)
  101. 0101specialize factor_permutation_swap_reflect_unchanged (p)
  102. 0102specialize factor_permutation_swap_reflect_unchanged (q)
  103. 0103specialize factor_permutation_swap_reflect_unchanged (k)
  104. 0104specialize factor_permutation_swap_reflect_unchanged (x)
  105. 0105apply factor_permutation_swap_reflect_unchanged
  106. 0106exact hs
  107. 0107exact hk
  108. 0108exact hcase_right
  109. 0109exact hlast_right
  110. 0110exact hvalue_witness