AF0015

factor_permutation_swap_factorization

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

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

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 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)))))))

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 3 declared prerequisites and contains 65 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

AF0008 factor_permutation_product_exists beta_product_swap_last_invariant Stable theorem; checked-use authorized AF0014 factor_permutation_swap_all_prime

Direct dependents

AF0016 factor_permutation_swapped_factorization_exists

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

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.

Named ingredients (2)
factor permutation product existsfactor permutation swap all prime

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 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
  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 exact 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 : exists Q. (exists ff_u_fsat_swap_product ff_v_fsat_swap_product. ((((exists ff_h_fsat_swap_product_start. ff_h_fsat_swap_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_product)) /\ exists ff_q_fsat_swap_product_start. ff_u_fsat_swap_product = ff_q_fsat_swap_product_start * S ((S (0)) * ff_v_fsat_swap_product) + (1))) /\ ((((exists ff_h_fsat_swap_product_terminal. ff_h_fsat_swap_product_terminal + S (Q) = S ((S (S l)) * ff_v_fsat_swap_product)) /\ exists ff_q_fsat_swap_product_terminal. ff_u_fsat_swap_product = ff_q_fsat_swap_product_terminal * S ((S (S l)) * ff_v_fsat_swap_product) + (Q))) /\ forall ff_i_fsat_swap_product. (exists ff_lt_fsat_swap_product_bound. ff_lt_fsat_swap_product_bound + S ff_i_fsat_swap_product = S l) -> exists ff_p_fsat_swap_product ff_r_fsat_swap_product ff_s_fsat_swap_product. ((((exists ff_h_fsat_swap_product_factor. ff_h_fsat_swap_product_factor + S (ff_p_fsat_swap_product) = S ((S (ff_i_fsat_swap_product)) * e)) /\ exists ff_q_fsat_swap_product_factor. d = ff_q_fsat_swap_product_factor * S ((S (ff_i_fsat_swap_product)) * e) + (ff_p_fsat_swap_product))) /\ ((((exists ff_h_fsat_swap_product_partial. ff_h_fsat_swap_product_partial + S (ff_r_fsat_swap_product) = S ((S (ff_i_fsat_swap_product)) * ff_v_fsat_swap_product)) /\ exists ff_q_fsat_swap_product_partial. ff_u_fsat_swap_product = ff_q_fsat_swap_product_partial * S ((S (ff_i_fsat_swap_product)) * ff_v_fsat_swap_product) + (ff_r_fsat_swap_product))) /\ ((((exists ff_h_fsat_swap_product_successor. ff_h_fsat_swap_product_successor + S (ff_s_fsat_swap_product) = S ((S (S ff_i_fsat_swap_product)) * ff_v_fsat_swap_product)) /\ exists ff_q_fsat_swap_product_successor. ff_u_fsat_swap_product = ff_q_fsat_swap_product_successor * S ((S (S ff_i_fsat_swap_product)) * ff_v_fsat_swap_product) + (ff_s_fsat_swap_product))) /\ ff_s_fsat_swap_product = ff_r_fsat_swap_product * ff_p_fsat_swap_product))))))
  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