AF001A

prime_factor_lists_permutation_exists

Exact G005: every two arbitrary unordered prime factorizations of the same positive natural admit an actual coded matching bijection, with equal lengths and explicit boundedness, injectivity, and surjectivity.

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. ∀ l. ∀ d. ∀ e. ∀ m. PrimeFactorList(n,b,c,l) ∧ PrimeFactorList(n,d,e,m) → ∃ x. ∃ y. PrimeFactorListPermutation(b,c,l,d,e,m,x,y)

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

Definition DAG

PermutationPrefix(b,c,l) · 1PrimeFactorList(n,b,c,l) · 2FactorListMatching(b,c,d,e,u,v,l) · 1PrimeFactorListPermutation(b,c,l,d,e,m,u,v) · 1

Actual proof prerequisites

prime_factor_lists_matching_by_length
Original expanded first-order statement 
forall n b c l d e m. (((~(n = 0) /\ ((exists ff_u_fsat_root_source_product ff_v_fsat_root_source_product. ((((exists ff_h_fsat_root_source_product_start. ff_h_fsat_root_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_start. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_start * S ((S (0)) * ff_v_fsat_root_source_product) + (1))) /\ ((((exists ff_h_fsat_root_source_product_terminal. ff_h_fsat_root_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_terminal. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_terminal * S ((S (l)) * ff_v_fsat_root_source_product) + (n))) /\ forall ff_i_fsat_root_source_product. (exists ff_lt_fsat_root_source_product_bound. ff_lt_fsat_root_source_product_bound + S ff_i_fsat_root_source_product = l) -> exists ff_p_fsat_root_source_product ff_r_fsat_root_source_product ff_s_fsat_root_source_product. ((((exists ff_h_fsat_root_source_product_factor. ff_h_fsat_root_source_product_factor + S (ff_p_fsat_root_source_product) = S ((S (ff_i_fsat_root_source_product)) * c)) /\ exists ff_q_fsat_root_source_product_factor. b = ff_q_fsat_root_source_product_factor * S ((S (ff_i_fsat_root_source_product)) * c) + (ff_p_fsat_root_source_product))) /\ ((((exists ff_h_fsat_root_source_product_partial. ff_h_fsat_root_source_product_partial + S (ff_r_fsat_root_source_product) = S ((S (ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_partial. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_partial * S ((S (ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product) + (ff_r_fsat_root_source_product))) /\ ((((exists ff_h_fsat_root_source_product_successor. ff_h_fsat_root_source_product_successor + S (ff_s_fsat_root_source_product) = S ((S (S ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product)) /\ exists ff_q_fsat_root_source_product_successor. ff_u_fsat_root_source_product = ff_q_fsat_root_source_product_successor * S ((S (S ff_i_fsat_root_source_product)) * ff_v_fsat_root_source_product) + (ff_s_fsat_root_source_product))) /\ ff_s_fsat_root_source_product = ff_r_fsat_root_source_product * ff_p_fsat_root_source_product)))))) /\ (forall ftsf_index_fsat_root_source_primes. (exists ftsf_gap_fsat_root_source_primes_bound. ftsf_gap_fsat_root_source_primes_bound + S ftsf_index_fsat_root_source_primes = (l)) -> exists ftsf_factor_fsat_root_source_primes. ((((exists ff_h_ftsf_fsat_root_source_primes_entry. ff_h_ftsf_fsat_root_source_primes_entry + S (ftsf_factor_fsat_root_source_primes) = S ((S (ftsf_index_fsat_root_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_root_source_primes_entry. b = ff_q_ftsf_fsat_root_source_primes_entry * S ((S (ftsf_index_fsat_root_source_primes)) * c) + (ftsf_factor_fsat_root_source_primes))) /\ ((~(ftsf_factor_fsat_root_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_root_source_primes_prime frm_prime_right_ftsf_fsat_root_source_primes_prime. ftsf_factor_fsat_root_source_primes = frm_prime_left_ftsf_fsat_root_source_primes_prime * frm_prime_right_ftsf_fsat_root_source_primes_prime -> frm_prime_left_ftsf_fsat_root_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_root_source_primes_prime = 1))))))) /\ ((~(n = 0) /\ ((exists ff_u_fsat_root_target_product ff_v_fsat_root_target_product. ((((exists ff_h_fsat_root_target_product_start. ff_h_fsat_root_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_start. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_start * S ((S (0)) * ff_v_fsat_root_target_product) + (1))) /\ ((((exists ff_h_fsat_root_target_product_terminal. ff_h_fsat_root_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_terminal. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_terminal * S ((S (m)) * ff_v_fsat_root_target_product) + (n))) /\ forall ff_i_fsat_root_target_product. (exists ff_lt_fsat_root_target_product_bound. ff_lt_fsat_root_target_product_bound + S ff_i_fsat_root_target_product = m) -> exists ff_p_fsat_root_target_product ff_r_fsat_root_target_product ff_s_fsat_root_target_product. ((((exists ff_h_fsat_root_target_product_factor. ff_h_fsat_root_target_product_factor + S (ff_p_fsat_root_target_product) = S ((S (ff_i_fsat_root_target_product)) * e)) /\ exists ff_q_fsat_root_target_product_factor. d = ff_q_fsat_root_target_product_factor * S ((S (ff_i_fsat_root_target_product)) * e) + (ff_p_fsat_root_target_product))) /\ ((((exists ff_h_fsat_root_target_product_partial. ff_h_fsat_root_target_product_partial + S (ff_r_fsat_root_target_product) = S ((S (ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_partial. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_partial * S ((S (ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product) + (ff_r_fsat_root_target_product))) /\ ((((exists ff_h_fsat_root_target_product_successor. ff_h_fsat_root_target_product_successor + S (ff_s_fsat_root_target_product) = S ((S (S ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product)) /\ exists ff_q_fsat_root_target_product_successor. ff_u_fsat_root_target_product = ff_q_fsat_root_target_product_successor * S ((S (S ff_i_fsat_root_target_product)) * ff_v_fsat_root_target_product) + (ff_s_fsat_root_target_product))) /\ ff_s_fsat_root_target_product = ff_r_fsat_root_target_product * ff_p_fsat_root_target_product)))))) /\ (forall ftsf_index_fsat_root_target_primes. (exists ftsf_gap_fsat_root_target_primes_bound. ftsf_gap_fsat_root_target_primes_bound + S ftsf_index_fsat_root_target_primes = (m)) -> exists ftsf_factor_fsat_root_target_primes. ((((exists ff_h_ftsf_fsat_root_target_primes_entry. ff_h_ftsf_fsat_root_target_primes_entry + S (ftsf_factor_fsat_root_target_primes) = S ((S (ftsf_index_fsat_root_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_root_target_primes_entry. d = ff_q_ftsf_fsat_root_target_primes_entry * S ((S (ftsf_index_fsat_root_target_primes)) * e) + (ftsf_factor_fsat_root_target_primes))) /\ ((~(ftsf_factor_fsat_root_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_root_target_primes_prime frm_prime_right_ftsf_fsat_root_target_primes_prime. ftsf_factor_fsat_root_target_primes = frm_prime_left_ftsf_fsat_root_target_primes_prime * frm_prime_right_ftsf_fsat_root_target_primes_prime -> frm_prime_left_ftsf_fsat_root_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_root_target_primes_prime = 1)))))))) -> exists u v. (((l = m) /\ (((((forall pfp_i_root_permutationpermutationbounded. (exists pfp_gap_root_permutationpermutationboundedindex. pfp_gap_root_permutationpermutationboundedindex + S (pfp_i_root_permutationpermutationbounded) = (l)) -> exists pfp_a_root_permutationpermutationbounded. (((exists ff_h_pfp_root_permutationpermutationboundedentry. ff_h_pfp_root_permutationpermutationboundedentry + S (pfp_a_root_permutationpermutationbounded) = S ((S (pfp_i_root_permutationpermutationbounded)) * v)) /\ exists ff_q_pfp_root_permutationpermutationboundedentry. u = ff_q_pfp_root_permutationpermutationboundedentry * S ((S (pfp_i_root_permutationpermutationbounded)) * v) + (pfp_a_root_permutationpermutationbounded))) /\ (exists pfp_gap_root_permutationpermutationboundedvalue. pfp_gap_root_permutationpermutationboundedvalue + S (pfp_a_root_permutationpermutationbounded) = (l))) /\ (((forall pfp_i_root_permutationpermutationinjective pfp_j_root_permutationpermutationinjective pfp_a_root_permutationpermutationinjective. (exists pfp_gap_root_permutationpermutationinjectivefirst. pfp_gap_root_permutationpermutationinjectivefirst + S (pfp_i_root_permutationpermutationinjective) = (l)) -> (exists pfp_gap_root_permutationpermutationinjectivesecond. pfp_gap_root_permutationpermutationinjectivesecond + S (pfp_j_root_permutationpermutationinjective) = (l)) -> (((exists ff_h_pfp_root_permutationpermutationinjectiveleft. ff_h_pfp_root_permutationpermutationinjectiveleft + S (pfp_a_root_permutationpermutationinjective) = S ((S (pfp_i_root_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationinjectiveleft. u = ff_q_pfp_root_permutationpermutationinjectiveleft * S ((S (pfp_i_root_permutationpermutationinjective)) * v) + (pfp_a_root_permutationpermutationinjective))) -> (((exists ff_h_pfp_root_permutationpermutationinjectiveright. ff_h_pfp_root_permutationpermutationinjectiveright + S (pfp_a_root_permutationpermutationinjective) = S ((S (pfp_j_root_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationinjectiveright. u = ff_q_pfp_root_permutationpermutationinjectiveright * S ((S (pfp_j_root_permutationpermutationinjective)) * v) + (pfp_a_root_permutationpermutationinjective))) -> pfp_i_root_permutationpermutationinjective = pfp_j_root_permutationpermutationinjective) /\ (forall pfp_a_root_permutationpermutationsurjective. (exists pfp_gap_root_permutationpermutationsurjectivevalue. pfp_gap_root_permutationpermutationsurjectivevalue + S (pfp_a_root_permutationpermutationsurjective) = (l)) -> exists pfp_i_root_permutationpermutationsurjective. (exists pfp_gap_root_permutationpermutationsurjectiveindex. pfp_gap_root_permutationpermutationsurjectiveindex + S (pfp_i_root_permutationpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_root_permutationpermutationsurjectiveentry. ff_h_pfp_root_permutationpermutationsurjectiveentry + S (pfp_a_root_permutationpermutationsurjective) = S ((S (pfp_i_root_permutationpermutationsurjective)) * v)) /\ exists ff_q_pfp_root_permutationpermutationsurjectiveentry. u = ff_q_pfp_root_permutationpermutationsurjectiveentry * S ((S (pfp_i_root_permutationpermutationsurjective)) * v) + (pfp_a_root_permutationpermutationsurjective)))))))) /\ (forall pfp_i_root_permutationmatching pfp_j_root_permutationmatching pfp_a_root_permutationmatching. (exists pfp_gap_root_permutationmatchingbound. pfp_gap_root_permutationmatchingbound + S (pfp_i_root_permutationmatching) = (l)) -> (((exists ff_h_pfp_root_permutationmatchingmap. ff_h_pfp_root_permutationmatchingmap + S (pfp_j_root_permutationmatching) = S ((S (pfp_i_root_permutationmatching)) * v)) /\ exists ff_q_pfp_root_permutationmatchingmap. u = ff_q_pfp_root_permutationmatchingmap * S ((S (pfp_i_root_permutationmatching)) * v) + (pfp_j_root_permutationmatching))) -> (((exists ff_h_pfp_root_permutationmatchingsource. ff_h_pfp_root_permutationmatchingsource + S (pfp_a_root_permutationmatching) = S ((S (pfp_i_root_permutationmatching)) * c)) /\ exists ff_q_pfp_root_permutationmatchingsource. b = ff_q_pfp_root_permutationmatchingsource * S ((S (pfp_i_root_permutationmatching)) * c) + (pfp_a_root_permutationmatching))) -> (((exists ff_h_pfp_root_permutationmatchingtarget. ff_h_pfp_root_permutationmatchingtarget + S (pfp_a_root_permutationmatching) = S ((S (pfp_j_root_permutationmatching)) * e)) /\ exists ff_q_pfp_root_permutationmatchingtarget. d = ff_q_pfp_root_permutationmatchingtarget * S ((S (pfp_j_root_permutationmatching)) * e) + (pfp_a_root_permutationmatching))))))))

Complete tactic proof in conservative notation

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

28 script commands · 8 reading checkpoints · 1 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)
prime factor lists matching by length
01Fix variables and assumptionsL1–8

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 l
  5. L5
    intro d
  6. L6
    intro e
  7. L7
    intro m
  8. L8
    intro hf
02Separate the logical casesL9–9

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

  1. L9
    cases hf
03Establish hresultL10–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime factor lists matching by length.

  1. L10
    have hresult : l = m ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))Definitions: PermutationPrefix(x,y,l)FactorListMatching(b,c,d,e,x,y,l)Original native command in the exact edition
  2. L11
    specialize prime_factor_lists_matching_by_length (l)
  3. L12
    specialize prime_factor_lists_matching_by_length (n)
  4. L13
    specialize prime_factor_lists_matching_by_length (b)
  5. L14
    specialize prime_factor_lists_matching_by_length (c)
  6. L15
    specialize prime_factor_lists_matching_by_length (m)
  7. L16
    specialize prime_factor_lists_matching_by_length (d)
  8. L17
    specialize prime_factor_lists_matching_by_length (e)
  9. L18
    apply prime_factor_lists_matching_by_length
  10. L19
    exact hf_left
04Use earlier factsL20–20

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

  1. L20
    exact hf_right
05Separate the logical casesL21–23

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

  1. L21
    cases hresult
  2. L22
    cases hresult_right
  3. L23
    cases hresult_right_witness
06Construct an explicit witnessL24–25

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

  1. L24
    exists x
  2. L25
    exists x1
07Separate the logical casesL26–26

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

  1. L26
    split
08Use earlier factsL27–28

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

  1. L27
    exact hresult_left
  2. L28
    exact hresult_right_witness_witness

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro n
  2. 0002intro b
  3. 0003intro c
  4. 0004intro l
  5. 0005intro d
  6. 0006intro e
  7. 0007intro m
  8. 0008intro hf
  9. 0009cases hf
  10. 0010have hresult : l = m ∧ (∃ x. ∃ y. PermutationPrefix(x,y,l) ∧ FactorListMatching(b,c,d,e,x,y,l))
  11. 0011specialize prime_factor_lists_matching_by_length (l)
  12. 0012specialize prime_factor_lists_matching_by_length (n)
  13. 0013specialize prime_factor_lists_matching_by_length (b)
  14. 0014specialize prime_factor_lists_matching_by_length (c)
  15. 0015specialize prime_factor_lists_matching_by_length (m)
  16. 0016specialize prime_factor_lists_matching_by_length (d)
  17. 0017specialize prime_factor_lists_matching_by_length (e)
  18. 0018apply prime_factor_lists_matching_by_length
  19. 0019exact hf_left
  20. 0020exact hf_right
  21. 0021cases hresult
  22. 0022cases hresult_right
  23. 0023cases hresult_right_witness
  24. 0024exists x
  25. 0025exists x1
  26. 0026split
  27. 0027exact hresult_left
  28. 0028exact hresult_right_witness_witness