AF0015

factor_permutation_swap_factorization

The swapped prime list has an actual product trace with the identical nonzero product, not merely a proposed rearrangement equality.

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

∀ N. ∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ i. ∀ p. ∀ q. PrimeFactorList(N,b,c,S l) → Lt(i,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))))) → PrimeFactorList(N,d,e,S l)

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

Definition DAG

PrimeFactorList(n,b,c,l) · 2Lt(a,b) · 2BetaAt(b,c,i,x) · 6Product(b,c,l,z) · 1

Actual proof prerequisites

factor_permutation_product_existsbeta_product_swap_last_invariant · checked external prerequisitefactor_permutation_swap_all_prime
Original expanded first-order statement 
forall N b c d e l i p q. ((~(N = 0) /\ ((exists ff_u_fsat_swap_factor_old_product ff_v_fsat_swap_factor_old_product. ((((exists ff_h_fsat_swap_factor_old_product_start. ff_h_fsat_swap_factor_old_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_factor_old_product)) /\ exists ff_q_fsat_swap_factor_old_product_start. ff_u_fsat_swap_factor_old_product = ff_q_fsat_swap_factor_old_product_start * S ((S (0)) * ff_v_fsat_swap_factor_old_product) + (1))) /\ ((((exists ff_h_fsat_swap_factor_old_product_terminal. ff_h_fsat_swap_factor_old_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_factor_old_product)) /\ exists ff_q_fsat_swap_factor_old_product_terminal. ff_u_fsat_swap_factor_old_product = ff_q_fsat_swap_factor_old_product_terminal * S ((S (S l)) * ff_v_fsat_swap_factor_old_product) + (N))) /\ forall ff_i_fsat_swap_factor_old_product. (exists ff_lt_fsat_swap_factor_old_product_bound. ff_lt_fsat_swap_factor_old_product_bound + S ff_i_fsat_swap_factor_old_product = S l) -> exists ff_p_fsat_swap_factor_old_product ff_r_fsat_swap_factor_old_product ff_s_fsat_swap_factor_old_product. ((((exists ff_h_fsat_swap_factor_old_product_factor. ff_h_fsat_swap_factor_old_product_factor + S (ff_p_fsat_swap_factor_old_product) = S ((S (ff_i_fsat_swap_factor_old_product)) * c)) /\ exists ff_q_fsat_swap_factor_old_product_factor. b = ff_q_fsat_swap_factor_old_product_factor * S ((S (ff_i_fsat_swap_factor_old_product)) * c) + (ff_p_fsat_swap_factor_old_product))) /\ ((((exists ff_h_fsat_swap_factor_old_product_partial. ff_h_fsat_swap_factor_old_product_partial + S (ff_r_fsat_swap_factor_old_product) = S ((S (ff_i_fsat_swap_factor_old_product)) * ff_v_fsat_swap_factor_old_product)) /\ exists ff_q_fsat_swap_factor_old_product_partial. ff_u_fsat_swap_factor_old_product = ff_q_fsat_swap_factor_old_product_partial * S ((S (ff_i_fsat_swap_factor_old_product)) * ff_v_fsat_swap_factor_old_product) + (ff_r_fsat_swap_factor_old_product))) /\ ((((exists ff_h_fsat_swap_factor_old_product_successor. ff_h_fsat_swap_factor_old_product_successor + S (ff_s_fsat_swap_factor_old_product) = S ((S (S ff_i_fsat_swap_factor_old_product)) * ff_v_fsat_swap_factor_old_product)) /\ exists ff_q_fsat_swap_factor_old_product_successor. ff_u_fsat_swap_factor_old_product = ff_q_fsat_swap_factor_old_product_successor * S ((S (S ff_i_fsat_swap_factor_old_product)) * ff_v_fsat_swap_factor_old_product) + (ff_s_fsat_swap_factor_old_product))) /\ ff_s_fsat_swap_factor_old_product = ff_r_fsat_swap_factor_old_product * ff_p_fsat_swap_factor_old_product)))))) /\ (forall ftsf_index_fsat_swap_factor_old_primes. (exists ftsf_gap_fsat_swap_factor_old_primes_bound. ftsf_gap_fsat_swap_factor_old_primes_bound + S ftsf_index_fsat_swap_factor_old_primes = (S l)) -> exists ftsf_factor_fsat_swap_factor_old_primes. ((((exists ff_h_ftsf_fsat_swap_factor_old_primes_entry. ff_h_ftsf_fsat_swap_factor_old_primes_entry + S (ftsf_factor_fsat_swap_factor_old_primes) = S ((S (ftsf_index_fsat_swap_factor_old_primes)) * c)) /\ exists ff_q_ftsf_fsat_swap_factor_old_primes_entry. b = ff_q_ftsf_fsat_swap_factor_old_primes_entry * S ((S (ftsf_index_fsat_swap_factor_old_primes)) * c) + (ftsf_factor_fsat_swap_factor_old_primes))) /\ ((~(ftsf_factor_fsat_swap_factor_old_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_factor_old_primes_prime frm_prime_right_ftsf_fsat_swap_factor_old_primes_prime. ftsf_factor_fsat_swap_factor_old_primes = frm_prime_left_ftsf_fsat_swap_factor_old_primes_prime * frm_prime_right_ftsf_fsat_swap_factor_old_primes_prime -> frm_prime_left_ftsf_fsat_swap_factor_old_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_factor_old_primes_prime = 1))))))) -> (exists pfp_gap_swap_factor_index. pfp_gap_swap_factor_index + S (i) = (l)) -> (((((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)))))))))))) -> ((~(N = 0) /\ ((exists ff_u_fsat_swap_factor_new_product ff_v_fsat_swap_factor_new_product. ((((exists ff_h_fsat_swap_factor_new_product_start. ff_h_fsat_swap_factor_new_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_factor_new_product)) /\ exists ff_q_fsat_swap_factor_new_product_start. ff_u_fsat_swap_factor_new_product = ff_q_fsat_swap_factor_new_product_start * S ((S (0)) * ff_v_fsat_swap_factor_new_product) + (1))) /\ ((((exists ff_h_fsat_swap_factor_new_product_terminal. ff_h_fsat_swap_factor_new_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_factor_new_product)) /\ exists ff_q_fsat_swap_factor_new_product_terminal. ff_u_fsat_swap_factor_new_product = ff_q_fsat_swap_factor_new_product_terminal * S ((S (S l)) * ff_v_fsat_swap_factor_new_product) + (N))) /\ forall ff_i_fsat_swap_factor_new_product. (exists ff_lt_fsat_swap_factor_new_product_bound. ff_lt_fsat_swap_factor_new_product_bound + S ff_i_fsat_swap_factor_new_product = S l) -> exists ff_p_fsat_swap_factor_new_product ff_r_fsat_swap_factor_new_product ff_s_fsat_swap_factor_new_product. ((((exists ff_h_fsat_swap_factor_new_product_factor. ff_h_fsat_swap_factor_new_product_factor + S (ff_p_fsat_swap_factor_new_product) = S ((S (ff_i_fsat_swap_factor_new_product)) * e)) /\ exists ff_q_fsat_swap_factor_new_product_factor. d = ff_q_fsat_swap_factor_new_product_factor * S ((S (ff_i_fsat_swap_factor_new_product)) * e) + (ff_p_fsat_swap_factor_new_product))) /\ ((((exists ff_h_fsat_swap_factor_new_product_partial. ff_h_fsat_swap_factor_new_product_partial + S (ff_r_fsat_swap_factor_new_product) = S ((S (ff_i_fsat_swap_factor_new_product)) * ff_v_fsat_swap_factor_new_product)) /\ exists ff_q_fsat_swap_factor_new_product_partial. ff_u_fsat_swap_factor_new_product = ff_q_fsat_swap_factor_new_product_partial * S ((S (ff_i_fsat_swap_factor_new_product)) * ff_v_fsat_swap_factor_new_product) + (ff_r_fsat_swap_factor_new_product))) /\ ((((exists ff_h_fsat_swap_factor_new_product_successor. ff_h_fsat_swap_factor_new_product_successor + S (ff_s_fsat_swap_factor_new_product) = S ((S (S ff_i_fsat_swap_factor_new_product)) * ff_v_fsat_swap_factor_new_product)) /\ exists ff_q_fsat_swap_factor_new_product_successor. ff_u_fsat_swap_factor_new_product = ff_q_fsat_swap_factor_new_product_successor * S ((S (S ff_i_fsat_swap_factor_new_product)) * ff_v_fsat_swap_factor_new_product) + (ff_s_fsat_swap_factor_new_product))) /\ ff_s_fsat_swap_factor_new_product = ff_r_fsat_swap_factor_new_product * ff_p_fsat_swap_factor_new_product)))))) /\ (forall ftsf_index_fsat_swap_factor_new_primes. (exists ftsf_gap_fsat_swap_factor_new_primes_bound. ftsf_gap_fsat_swap_factor_new_primes_bound + S ftsf_index_fsat_swap_factor_new_primes = (S l)) -> exists ftsf_factor_fsat_swap_factor_new_primes. ((((exists ff_h_ftsf_fsat_swap_factor_new_primes_entry. ff_h_ftsf_fsat_swap_factor_new_primes_entry + S (ftsf_factor_fsat_swap_factor_new_primes) = S ((S (ftsf_index_fsat_swap_factor_new_primes)) * e)) /\ exists ff_q_ftsf_fsat_swap_factor_new_primes_entry. d = ff_q_ftsf_fsat_swap_factor_new_primes_entry * S ((S (ftsf_index_fsat_swap_factor_new_primes)) * e) + (ftsf_factor_fsat_swap_factor_new_primes))) /\ ((~(ftsf_factor_fsat_swap_factor_new_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_factor_new_primes_prime frm_prime_right_ftsf_fsat_swap_factor_new_primes_prime. ftsf_factor_fsat_swap_factor_new_primes = frm_prime_left_ftsf_fsat_swap_factor_new_primes_prime * frm_prime_right_ftsf_fsat_swap_factor_new_primes_prime -> frm_prime_left_ftsf_fsat_swap_factor_new_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_factor_new_primes_prime = 1)))))))

Complete tactic proof in conservative notation

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

65 script commands · 16 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 (2)
factor permutation product existsfactor permutation swap all prime
01Fix variables and assumptionsL1–10

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

  1. L1
    intro N
  2. L2
    intro b
  3. L3
    intro c
  4. L4
    intro d
  5. L5
    intro e
  6. L6
    intro l
  7. L7
    intro i
  8. L8
    intro p
  9. L9
    intro q
  10. L10
    intro hf
02Fix variables and assumptionsL11–12

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

  1. L11
    intro hi
  2. L12
    intro hs
03Separate the logical casesL13–14

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

  1. L13
    cases hf
  2. L14
    cases hf_right
04Establish hproductL15–19

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

  1. L15
    have hproduct : ∃ Q. Product(d,e,S l,Q)Definitions: Product(d,e,S l,Q)Original native command in the exact edition
  2. L16
    specialize factor_permutation_product_exists (d)
  3. L17
    specialize factor_permutation_product_exists (e)
  4. L18
    specialize factor_permutation_product_exists (S l)
  5. L19
    apply factor_permutation_product_exists
05Separate the logical casesL20–20

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

  1. L20
    cases hproduct
06Establish hsameL21–21

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

  1. L21
    have hsame : N = x
07Separate the logical casesL22–25

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

  1. L22
    cases hs
  2. L23
    cases hs_right
  3. L24
    cases hs_right_right
  4. L25
    cases hs_right_right_right
08Use earlier factsL26–35

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

  1. L26
    specialize beta_product_swap_last_invariant (b)
  2. L27
    specialize beta_product_swap_last_invariant (c)
  3. L28
    specialize beta_product_swap_last_invariant (d)
  4. L29
    specialize beta_product_swap_last_invariant (e)
  5. L30
    specialize beta_product_swap_last_invariant (l)
  6. L31
    specialize beta_product_swap_last_invariant (i)
  7. L32
    specialize beta_product_swap_last_invariant (p)
  8. L33
    specialize beta_product_swap_last_invariant (q)
  9. L34
    specialize beta_product_swap_last_invariant (N)
  10. L35
    specialize beta_product_swap_last_invariant (x)
09Use earlier factsL36–44

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

  1. L36
    apply beta_product_swap_last_invariant
  2. L37
    exact hi
  3. L38
    exact hs_left
  4. L39
    exact hs_right_left
  5. L40
    exact hs_right_right_left
  6. L41
    exact hs_right_right_right_left
  7. L42
    exact hs_right_right_right_right
  8. L43
    exact hf_right_left
  9. L44
    exact hproduct_witness
10Establish hxL45–47

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

  1. L45
    have hx : x = N
  2. L46
    symm
  3. L47
    exact hsame
11Separate the logical casesL48–48

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

  1. L48
    split
12Use earlier factsL49–49

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

  1. L49
    exact hf_left
13Separate the logical casesL50–50

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

  1. L50
    split
14Calculate and transport equalitiesL51–52

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

  1. L51
    rewrite hx at hproduct_witness
  2. L52
    rewrite hx at hproduct_witness
15Use earlier factsL53–62

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

  1. L53
    exact hproduct_witness
  2. L54
    specialize factor_permutation_swap_all_prime (b)
  3. L55
    specialize factor_permutation_swap_all_prime (c)
  4. L56
    specialize factor_permutation_swap_all_prime (d)
  5. L57
    specialize factor_permutation_swap_all_prime (e)
  6. L58
    specialize factor_permutation_swap_all_prime (l)
  7. L59
    specialize factor_permutation_swap_all_prime (i)
  8. L60
    specialize factor_permutation_swap_all_prime (p)
  9. L61
    specialize factor_permutation_swap_all_prime (q)
  10. L62
    apply factor_permutation_swap_all_prime
16Use earlier factsL63–65

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

  1. L63
    exact hi
  2. L64
    exact hf_right_right
  3. L65
    exact hs

Library-wide reading audit

Original defined command ledger · 65 lines
  1. 0001intro N
  2. 0002intro b
  3. 0003intro c
  4. 0004intro d
  5. 0005intro e
  6. 0006intro l
  7. 0007intro i
  8. 0008intro p
  9. 0009intro q
  10. 0010intro hf
  11. 0011intro hi
  12. 0012intro hs
  13. 0013cases hf
  14. 0014cases hf_right
  15. 0015have hproduct : ∃ Q. Product(d,e,S l,Q)
  16. 0016specialize factor_permutation_product_exists (d)
  17. 0017specialize factor_permutation_product_exists (e)
  18. 0018specialize factor_permutation_product_exists (S l)
  19. 0019apply factor_permutation_product_exists
  20. 0020cases hproduct
  21. 0021have hsame : N = x
  22. 0022cases hs
  23. 0023cases hs_right
  24. 0024cases hs_right_right
  25. 0025cases hs_right_right_right
  26. 0026specialize beta_product_swap_last_invariant (b)
  27. 0027specialize beta_product_swap_last_invariant (c)
  28. 0028specialize beta_product_swap_last_invariant (d)
  29. 0029specialize beta_product_swap_last_invariant (e)
  30. 0030specialize beta_product_swap_last_invariant (l)
  31. 0031specialize beta_product_swap_last_invariant (i)
  32. 0032specialize beta_product_swap_last_invariant (p)
  33. 0033specialize beta_product_swap_last_invariant (q)
  34. 0034specialize beta_product_swap_last_invariant (N)
  35. 0035specialize beta_product_swap_last_invariant (x)
  36. 0036apply beta_product_swap_last_invariant
  37. 0037exact hi
  38. 0038exact hs_left
  39. 0039exact hs_right_left
  40. 0040exact hs_right_right_left
  41. 0041exact hs_right_right_right_left
  42. 0042exact hs_right_right_right_right
  43. 0043exact hf_right_left
  44. 0044exact hproduct_witness
  45. 0045have hx : x = N
  46. 0046symm
  47. 0047exact hsame
  48. 0048split
  49. 0049exact hf_left
  50. 0050split
  51. 0051rewrite hx at hproduct_witness
  52. 0052rewrite hx at hproduct_witness
  53. 0053exact hproduct_witness
  54. 0054specialize factor_permutation_swap_all_prime (b)
  55. 0055specialize factor_permutation_swap_all_prime (c)
  56. 0056specialize factor_permutation_swap_all_prime (d)
  57. 0057specialize factor_permutation_swap_all_prime (e)
  58. 0058specialize factor_permutation_swap_all_prime (l)
  59. 0059specialize factor_permutation_swap_all_prime (i)
  60. 0060specialize factor_permutation_swap_all_prime (p)
  61. 0061specialize factor_permutation_swap_all_prime (q)
  62. 0062apply factor_permutation_swap_all_prime
  63. 0063exact hi
  64. 0064exact hf_right_right
  65. 0065exact hs