AF001B

prime_factorization_exists_unique_up_to_permutation

Construct an actual prime-factor list for every positive natural and an actual matching permutation to every competing unordered factorization. Both factor-list existence and uniqueness witnesses are conclusions, with no supplied canonical factorization.

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. ¬n = 0 → ∃ x. ∃ y. ∃ z. PrimeFactorList(n,y,z,x) ∧ (∀ m. ∀ k. ∀ i. PrimeFactorList(n,k,i,m) → ∃ j. ∃ u. PrimeFactorListPermutation(y,z,x,k,i,m,j,u))

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

Definition DAG

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

Actual proof prerequisites

foundation_prime_factor_list_existsprime_factor_lists_permutation_exists
Original expanded first-order statement 
forall n. ~(n = 0) -> exists l b c. (((~(n = 0) /\ ((exists ff_u_fsat_complete_source_product ff_v_fsat_complete_source_product. ((((exists ff_h_fsat_complete_source_product_start. ff_h_fsat_complete_source_product_start + S (1) = S ((S (0)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_start. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_start * S ((S (0)) * ff_v_fsat_complete_source_product) + (1))) /\ ((((exists ff_h_fsat_complete_source_product_terminal. ff_h_fsat_complete_source_product_terminal + S (n) = S ((S (l)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_terminal. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_terminal * S ((S (l)) * ff_v_fsat_complete_source_product) + (n))) /\ forall ff_i_fsat_complete_source_product. (exists ff_lt_fsat_complete_source_product_bound. ff_lt_fsat_complete_source_product_bound + S ff_i_fsat_complete_source_product = l) -> exists ff_p_fsat_complete_source_product ff_r_fsat_complete_source_product ff_s_fsat_complete_source_product. ((((exists ff_h_fsat_complete_source_product_factor. ff_h_fsat_complete_source_product_factor + S (ff_p_fsat_complete_source_product) = S ((S (ff_i_fsat_complete_source_product)) * c)) /\ exists ff_q_fsat_complete_source_product_factor. b = ff_q_fsat_complete_source_product_factor * S ((S (ff_i_fsat_complete_source_product)) * c) + (ff_p_fsat_complete_source_product))) /\ ((((exists ff_h_fsat_complete_source_product_partial. ff_h_fsat_complete_source_product_partial + S (ff_r_fsat_complete_source_product) = S ((S (ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_partial. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_partial * S ((S (ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product) + (ff_r_fsat_complete_source_product))) /\ ((((exists ff_h_fsat_complete_source_product_successor. ff_h_fsat_complete_source_product_successor + S (ff_s_fsat_complete_source_product) = S ((S (S ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product)) /\ exists ff_q_fsat_complete_source_product_successor. ff_u_fsat_complete_source_product = ff_q_fsat_complete_source_product_successor * S ((S (S ff_i_fsat_complete_source_product)) * ff_v_fsat_complete_source_product) + (ff_s_fsat_complete_source_product))) /\ ff_s_fsat_complete_source_product = ff_r_fsat_complete_source_product * ff_p_fsat_complete_source_product)))))) /\ (forall ftsf_index_fsat_complete_source_primes. (exists ftsf_gap_fsat_complete_source_primes_bound. ftsf_gap_fsat_complete_source_primes_bound + S ftsf_index_fsat_complete_source_primes = (l)) -> exists ftsf_factor_fsat_complete_source_primes. ((((exists ff_h_ftsf_fsat_complete_source_primes_entry. ff_h_ftsf_fsat_complete_source_primes_entry + S (ftsf_factor_fsat_complete_source_primes) = S ((S (ftsf_index_fsat_complete_source_primes)) * c)) /\ exists ff_q_ftsf_fsat_complete_source_primes_entry. b = ff_q_ftsf_fsat_complete_source_primes_entry * S ((S (ftsf_index_fsat_complete_source_primes)) * c) + (ftsf_factor_fsat_complete_source_primes))) /\ ((~(ftsf_factor_fsat_complete_source_primes = 1) /\ forall frm_prime_left_ftsf_fsat_complete_source_primes_prime frm_prime_right_ftsf_fsat_complete_source_primes_prime. ftsf_factor_fsat_complete_source_primes = frm_prime_left_ftsf_fsat_complete_source_primes_prime * frm_prime_right_ftsf_fsat_complete_source_primes_prime -> frm_prime_left_ftsf_fsat_complete_source_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_complete_source_primes_prime = 1))))))) /\ forall m d e. ((~(n = 0) /\ ((exists ff_u_fsat_complete_target_product ff_v_fsat_complete_target_product. ((((exists ff_h_fsat_complete_target_product_start. ff_h_fsat_complete_target_product_start + S (1) = S ((S (0)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_start. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_start * S ((S (0)) * ff_v_fsat_complete_target_product) + (1))) /\ ((((exists ff_h_fsat_complete_target_product_terminal. ff_h_fsat_complete_target_product_terminal + S (n) = S ((S (m)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_terminal. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_terminal * S ((S (m)) * ff_v_fsat_complete_target_product) + (n))) /\ forall ff_i_fsat_complete_target_product. (exists ff_lt_fsat_complete_target_product_bound. ff_lt_fsat_complete_target_product_bound + S ff_i_fsat_complete_target_product = m) -> exists ff_p_fsat_complete_target_product ff_r_fsat_complete_target_product ff_s_fsat_complete_target_product. ((((exists ff_h_fsat_complete_target_product_factor. ff_h_fsat_complete_target_product_factor + S (ff_p_fsat_complete_target_product) = S ((S (ff_i_fsat_complete_target_product)) * e)) /\ exists ff_q_fsat_complete_target_product_factor. d = ff_q_fsat_complete_target_product_factor * S ((S (ff_i_fsat_complete_target_product)) * e) + (ff_p_fsat_complete_target_product))) /\ ((((exists ff_h_fsat_complete_target_product_partial. ff_h_fsat_complete_target_product_partial + S (ff_r_fsat_complete_target_product) = S ((S (ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_partial. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_partial * S ((S (ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product) + (ff_r_fsat_complete_target_product))) /\ ((((exists ff_h_fsat_complete_target_product_successor. ff_h_fsat_complete_target_product_successor + S (ff_s_fsat_complete_target_product) = S ((S (S ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product)) /\ exists ff_q_fsat_complete_target_product_successor. ff_u_fsat_complete_target_product = ff_q_fsat_complete_target_product_successor * S ((S (S ff_i_fsat_complete_target_product)) * ff_v_fsat_complete_target_product) + (ff_s_fsat_complete_target_product))) /\ ff_s_fsat_complete_target_product = ff_r_fsat_complete_target_product * ff_p_fsat_complete_target_product)))))) /\ (forall ftsf_index_fsat_complete_target_primes. (exists ftsf_gap_fsat_complete_target_primes_bound. ftsf_gap_fsat_complete_target_primes_bound + S ftsf_index_fsat_complete_target_primes = (m)) -> exists ftsf_factor_fsat_complete_target_primes. ((((exists ff_h_ftsf_fsat_complete_target_primes_entry. ff_h_ftsf_fsat_complete_target_primes_entry + S (ftsf_factor_fsat_complete_target_primes) = S ((S (ftsf_index_fsat_complete_target_primes)) * e)) /\ exists ff_q_ftsf_fsat_complete_target_primes_entry. d = ff_q_ftsf_fsat_complete_target_primes_entry * S ((S (ftsf_index_fsat_complete_target_primes)) * e) + (ftsf_factor_fsat_complete_target_primes))) /\ ((~(ftsf_factor_fsat_complete_target_primes = 1) /\ forall frm_prime_left_ftsf_fsat_complete_target_primes_prime frm_prime_right_ftsf_fsat_complete_target_primes_prime. ftsf_factor_fsat_complete_target_primes = frm_prime_left_ftsf_fsat_complete_target_primes_prime * frm_prime_right_ftsf_fsat_complete_target_primes_prime -> frm_prime_left_ftsf_fsat_complete_target_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_complete_target_primes_prime = 1))))))) -> exists u v. (((l = m) /\ (((((forall pfp_i_complete_permutationpermutationbounded. (exists pfp_gap_complete_permutationpermutationboundedindex. pfp_gap_complete_permutationpermutationboundedindex + S (pfp_i_complete_permutationpermutationbounded) = (l)) -> exists pfp_a_complete_permutationpermutationbounded. (((exists ff_h_pfp_complete_permutationpermutationboundedentry. ff_h_pfp_complete_permutationpermutationboundedentry + S (pfp_a_complete_permutationpermutationbounded) = S ((S (pfp_i_complete_permutationpermutationbounded)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationboundedentry. u = ff_q_pfp_complete_permutationpermutationboundedentry * S ((S (pfp_i_complete_permutationpermutationbounded)) * v) + (pfp_a_complete_permutationpermutationbounded))) /\ (exists pfp_gap_complete_permutationpermutationboundedvalue. pfp_gap_complete_permutationpermutationboundedvalue + S (pfp_a_complete_permutationpermutationbounded) = (l))) /\ (((forall pfp_i_complete_permutationpermutationinjective pfp_j_complete_permutationpermutationinjective pfp_a_complete_permutationpermutationinjective. (exists pfp_gap_complete_permutationpermutationinjectivefirst. pfp_gap_complete_permutationpermutationinjectivefirst + S (pfp_i_complete_permutationpermutationinjective) = (l)) -> (exists pfp_gap_complete_permutationpermutationinjectivesecond. pfp_gap_complete_permutationpermutationinjectivesecond + S (pfp_j_complete_permutationpermutationinjective) = (l)) -> (((exists ff_h_pfp_complete_permutationpermutationinjectiveleft. ff_h_pfp_complete_permutationpermutationinjectiveleft + S (pfp_a_complete_permutationpermutationinjective) = S ((S (pfp_i_complete_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationinjectiveleft. u = ff_q_pfp_complete_permutationpermutationinjectiveleft * S ((S (pfp_i_complete_permutationpermutationinjective)) * v) + (pfp_a_complete_permutationpermutationinjective))) -> (((exists ff_h_pfp_complete_permutationpermutationinjectiveright. ff_h_pfp_complete_permutationpermutationinjectiveright + S (pfp_a_complete_permutationpermutationinjective) = S ((S (pfp_j_complete_permutationpermutationinjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationinjectiveright. u = ff_q_pfp_complete_permutationpermutationinjectiveright * S ((S (pfp_j_complete_permutationpermutationinjective)) * v) + (pfp_a_complete_permutationpermutationinjective))) -> pfp_i_complete_permutationpermutationinjective = pfp_j_complete_permutationpermutationinjective) /\ (forall pfp_a_complete_permutationpermutationsurjective. (exists pfp_gap_complete_permutationpermutationsurjectivevalue. pfp_gap_complete_permutationpermutationsurjectivevalue + S (pfp_a_complete_permutationpermutationsurjective) = (l)) -> exists pfp_i_complete_permutationpermutationsurjective. (exists pfp_gap_complete_permutationpermutationsurjectiveindex. pfp_gap_complete_permutationpermutationsurjectiveindex + S (pfp_i_complete_permutationpermutationsurjective) = (l)) /\ (((exists ff_h_pfp_complete_permutationpermutationsurjectiveentry. ff_h_pfp_complete_permutationpermutationsurjectiveentry + S (pfp_a_complete_permutationpermutationsurjective) = S ((S (pfp_i_complete_permutationpermutationsurjective)) * v)) /\ exists ff_q_pfp_complete_permutationpermutationsurjectiveentry. u = ff_q_pfp_complete_permutationpermutationsurjectiveentry * S ((S (pfp_i_complete_permutationpermutationsurjective)) * v) + (pfp_a_complete_permutationpermutationsurjective)))))))) /\ (forall pfp_i_complete_permutationmatching pfp_j_complete_permutationmatching pfp_a_complete_permutationmatching. (exists pfp_gap_complete_permutationmatchingbound. pfp_gap_complete_permutationmatchingbound + S (pfp_i_complete_permutationmatching) = (l)) -> (((exists ff_h_pfp_complete_permutationmatchingmap. ff_h_pfp_complete_permutationmatchingmap + S (pfp_j_complete_permutationmatching) = S ((S (pfp_i_complete_permutationmatching)) * v)) /\ exists ff_q_pfp_complete_permutationmatchingmap. u = ff_q_pfp_complete_permutationmatchingmap * S ((S (pfp_i_complete_permutationmatching)) * v) + (pfp_j_complete_permutationmatching))) -> (((exists ff_h_pfp_complete_permutationmatchingsource. ff_h_pfp_complete_permutationmatchingsource + S (pfp_a_complete_permutationmatching) = S ((S (pfp_i_complete_permutationmatching)) * c)) /\ exists ff_q_pfp_complete_permutationmatchingsource. b = ff_q_pfp_complete_permutationmatchingsource * S ((S (pfp_i_complete_permutationmatching)) * c) + (pfp_a_complete_permutationmatching))) -> (((exists ff_h_pfp_complete_permutationmatchingtarget. ff_h_pfp_complete_permutationmatchingtarget + S (pfp_a_complete_permutationmatching) = S ((S (pfp_j_complete_permutationmatching)) * e)) /\ exists ff_q_pfp_complete_permutationmatchingtarget. d = ff_q_pfp_complete_permutationmatchingtarget * S ((S (pfp_j_complete_permutationmatching)) * e) + (pfp_a_complete_permutationmatching)))))))))

Complete tactic proof in conservative notation

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

29 script commands · 10 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 (2)
foundation prime factor list existsprime factor lists permutation exists
01Fix variables and assumptionsL1–2

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

  1. L1
    intro n
  2. L2
    intro hn
02Establish hsourceL3–6

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

  1. L3
    have hsource : ∃ l. ∃ b. ∃ c. PrimeFactorList(n,b,c,l)Definitions: PrimeFactorList(n,b,c,l)Original native command in the exact edition
  2. L4
    specialize foundation_prime_factor_list_exists (n)
  3. L5
    apply foundation_prime_factor_list_exists
  4. L6
    exact hn
03Separate the logical casesL7–9

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

  1. L7
    cases hsource
  2. L8
    cases hsource_witness
  3. L9
    cases hsource_witness_witness
04Construct an explicit witnessL10–12

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

  1. L10
    exists x
  2. L11
    exists x1
  3. L12
    exists x2
05Separate the logical casesL13–13

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

  1. L13
    split
06Use earlier factsL14–14

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

  1. L14
    exact hsource_witness_witness_witness
07Fix variables and assumptionsL15–18

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

  1. L15
    intro m
  2. L16
    intro d
  3. L17
    intro e
  4. L18
    intro htarget
08Use earlier factsL19–26

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

  1. L19
    specialize prime_factor_lists_permutation_exists (n)
  2. L20
    specialize prime_factor_lists_permutation_exists (x1)
  3. L21
    specialize prime_factor_lists_permutation_exists (x2)
  4. L22
    specialize prime_factor_lists_permutation_exists (x)
  5. L23
    specialize prime_factor_lists_permutation_exists (d)
  6. L24
    specialize prime_factor_lists_permutation_exists (e)
  7. L25
    specialize prime_factor_lists_permutation_exists (m)
  8. L26
    apply prime_factor_lists_permutation_exists
09Separate the logical casesL27–27

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

  1. L27
    split
10Use earlier factsL28–29

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

  1. L28
    exact hsource_witness_witness_witness
  2. L29
    exact htarget

Library-wide reading audit

Original defined command ledger · 29 lines
  1. 0001intro n
  2. 0002intro hn
  3. 0003have hsource : ∃ l. ∃ b. ∃ c. PrimeFactorList(n,b,c,l)
  4. 0004specialize foundation_prime_factor_list_exists (n)
  5. 0005apply foundation_prime_factor_list_exists
  6. 0006exact hn
  7. 0007cases hsource
  8. 0008cases hsource_witness
  9. 0009cases hsource_witness_witness
  10. 0010exists x
  11. 0011exists x1
  12. 0012exists x2
  13. 0013split
  14. 0014exact hsource_witness_witness_witness
  15. 0015intro m
  16. 0016intro d
  17. 0017intro e
  18. 0018intro htarget
  19. 0019specialize prime_factor_lists_permutation_exists (n)
  20. 0020specialize prime_factor_lists_permutation_exists (x1)
  21. 0021specialize prime_factor_lists_permutation_exists (x2)
  22. 0022specialize prime_factor_lists_permutation_exists (x)
  23. 0023specialize prime_factor_lists_permutation_exists (d)
  24. 0024specialize prime_factor_lists_permutation_exists (e)
  25. 0025specialize prime_factor_lists_permutation_exists (m)
  26. 0026apply prime_factor_lists_permutation_exists
  27. 0027split
  28. 0028exact hsource_witness_witness_witness
  29. 0029exact htarget