Construct a full recoded prime-factor list moving a selected interior prime to the last position, with exact swap witnesses and an unchanged actual product.
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.
forall N b c l i p. ((~(N = 0) /\ ((exists ff_u_fsat_swap_exists_factor_product ff_v_fsat_swap_exists_factor_product. ((((exists ff_h_fsat_swap_exists_factor_product_start. ff_h_fsat_swap_exists_factor_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_start. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_start * S ((S (0)) * ff_v_fsat_swap_exists_factor_product) + (1))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_terminal. ff_h_fsat_swap_exists_factor_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_terminal. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_terminal * S ((S (S l)) * ff_v_fsat_swap_exists_factor_product) + (N))) /\ forall ff_i_fsat_swap_exists_factor_product. (exists ff_lt_fsat_swap_exists_factor_product_bound. ff_lt_fsat_swap_exists_factor_product_bound + S ff_i_fsat_swap_exists_factor_product = S l) -> exists ff_p_fsat_swap_exists_factor_product ff_r_fsat_swap_exists_factor_product ff_s_fsat_swap_exists_factor_product. ((((exists ff_h_fsat_swap_exists_factor_product_factor. ff_h_fsat_swap_exists_factor_product_factor + S (ff_p_fsat_swap_exists_factor_product) = S ((S (ff_i_fsat_swap_exists_factor_product)) * c)) /\ exists ff_q_fsat_swap_exists_factor_product_factor. b = ff_q_fsat_swap_exists_factor_product_factor * S ((S (ff_i_fsat_swap_exists_factor_product)) * c) + (ff_p_fsat_swap_exists_factor_product))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_partial. ff_h_fsat_swap_exists_factor_product_partial + S (ff_r_fsat_swap_exists_factor_product) = S ((S (ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_partial. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_partial * S ((S (ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product) + (ff_r_fsat_swap_exists_factor_product))) /\ ((((exists ff_h_fsat_swap_exists_factor_product_successor. ff_h_fsat_swap_exists_factor_product_successor + S (ff_s_fsat_swap_exists_factor_product) = S ((S (S ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product)) /\ exists ff_q_fsat_swap_exists_factor_product_successor. ff_u_fsat_swap_exists_factor_product = ff_q_fsat_swap_exists_factor_product_successor * S ((S (S ff_i_fsat_swap_exists_factor_product)) * ff_v_fsat_swap_exists_factor_product) + (ff_s_fsat_swap_exists_factor_product))) /\ ff_s_fsat_swap_exists_factor_product = ff_r_fsat_swap_exists_factor_product * ff_p_fsat_swap_exists_factor_product)))))) /\ (forall ftsf_index_fsat_swap_exists_factor_primes. (exists ftsf_gap_fsat_swap_exists_factor_primes_bound. ftsf_gap_fsat_swap_exists_factor_primes_bound + S ftsf_index_fsat_swap_exists_factor_primes = (S l)) -> exists ftsf_factor_fsat_swap_exists_factor_primes. ((((exists ff_h_ftsf_fsat_swap_exists_factor_primes_entry. ff_h_ftsf_fsat_swap_exists_factor_primes_entry + S (ftsf_factor_fsat_swap_exists_factor_primes) = S ((S (ftsf_index_fsat_swap_exists_factor_primes)) * c)) /\ exists ff_q_ftsf_fsat_swap_exists_factor_primes_entry. b = ff_q_ftsf_fsat_swap_exists_factor_primes_entry * S ((S (ftsf_index_fsat_swap_exists_factor_primes)) * c) + (ftsf_factor_fsat_swap_exists_factor_primes))) /\ ((~(ftsf_factor_fsat_swap_exists_factor_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime. ftsf_factor_fsat_swap_exists_factor_primes = frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime * frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime -> frm_prime_left_ftsf_fsat_swap_exists_factor_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_exists_factor_primes_prime = 1))))))) -> (exists pfp_gap_swap_exists_index. pfp_gap_swap_exists_index + S (i) = (l)) -> (((exists ff_h_pfp_swap_exists_selected. ff_h_pfp_swap_exists_selected + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_exists_selected. b = ff_q_pfp_swap_exists_selected * S ((S (i)) * c) + (p))) -> exists d e q. (((~(N = 0) /\ ((exists ff_u_fsat_swap_exists_result_product ff_v_fsat_swap_exists_result_product. ((((exists ff_h_fsat_swap_exists_result_product_start. ff_h_fsat_swap_exists_result_product_start + S (1) = S ((S (0)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_start. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_start * S ((S (0)) * ff_v_fsat_swap_exists_result_product) + (1))) /\ ((((exists ff_h_fsat_swap_exists_result_product_terminal. ff_h_fsat_swap_exists_result_product_terminal + S (N) = S ((S (S l)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_terminal. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_terminal * S ((S (S l)) * ff_v_fsat_swap_exists_result_product) + (N))) /\ forall ff_i_fsat_swap_exists_result_product. (exists ff_lt_fsat_swap_exists_result_product_bound. ff_lt_fsat_swap_exists_result_product_bound + S ff_i_fsat_swap_exists_result_product = S l) -> exists ff_p_fsat_swap_exists_result_product ff_r_fsat_swap_exists_result_product ff_s_fsat_swap_exists_result_product. ((((exists ff_h_fsat_swap_exists_result_product_factor. ff_h_fsat_swap_exists_result_product_factor + S (ff_p_fsat_swap_exists_result_product) = S ((S (ff_i_fsat_swap_exists_result_product)) * e)) /\ exists ff_q_fsat_swap_exists_result_product_factor. d = ff_q_fsat_swap_exists_result_product_factor * S ((S (ff_i_fsat_swap_exists_result_product)) * e) + (ff_p_fsat_swap_exists_result_product))) /\ ((((exists ff_h_fsat_swap_exists_result_product_partial. ff_h_fsat_swap_exists_result_product_partial + S (ff_r_fsat_swap_exists_result_product) = S ((S (ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_partial. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_partial * S ((S (ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product) + (ff_r_fsat_swap_exists_result_product))) /\ ((((exists ff_h_fsat_swap_exists_result_product_successor. ff_h_fsat_swap_exists_result_product_successor + S (ff_s_fsat_swap_exists_result_product) = S ((S (S ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product)) /\ exists ff_q_fsat_swap_exists_result_product_successor. ff_u_fsat_swap_exists_result_product = ff_q_fsat_swap_exists_result_product_successor * S ((S (S ff_i_fsat_swap_exists_result_product)) * ff_v_fsat_swap_exists_result_product) + (ff_s_fsat_swap_exists_result_product))) /\ ff_s_fsat_swap_exists_result_product = ff_r_fsat_swap_exists_result_product * ff_p_fsat_swap_exists_result_product)))))) /\ (forall ftsf_index_fsat_swap_exists_result_primes. (exists ftsf_gap_fsat_swap_exists_result_primes_bound. ftsf_gap_fsat_swap_exists_result_primes_bound + S ftsf_index_fsat_swap_exists_result_primes = (S l)) -> exists ftsf_factor_fsat_swap_exists_result_primes. ((((exists ff_h_ftsf_fsat_swap_exists_result_primes_entry. ff_h_ftsf_fsat_swap_exists_result_primes_entry + S (ftsf_factor_fsat_swap_exists_result_primes) = S ((S (ftsf_index_fsat_swap_exists_result_primes)) * e)) /\ exists ff_q_ftsf_fsat_swap_exists_result_primes_entry. d = ff_q_ftsf_fsat_swap_exists_result_primes_entry * S ((S (ftsf_index_fsat_swap_exists_result_primes)) * e) + (ftsf_factor_fsat_swap_exists_result_primes))) /\ ((~(ftsf_factor_fsat_swap_exists_result_primes = 1) /\ forall frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime. ftsf_factor_fsat_swap_exists_result_primes = frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime * frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime -> frm_prime_left_ftsf_fsat_swap_exists_result_primes_prime = 1 \/ frm_prime_right_ftsf_fsat_swap_exists_result_primes_prime = 1))))))) /\ (((((exists ff_h_pfp_swap_exists_witnessoldi. ff_h_pfp_swap_exists_witnessoldi + S (p) = S ((S (i)) * c)) /\ exists ff_q_pfp_swap_exists_witnessoldi. b = ff_q_pfp_swap_exists_witnessoldi * S ((S (i)) * c) + (p))) /\ (((((exists ff_h_pfp_swap_exists_witnessoldlast. ff_h_pfp_swap_exists_witnessoldlast + S (q) = S ((S (l)) * c)) /\ exists ff_q_pfp_swap_exists_witnessoldlast. b = ff_q_pfp_swap_exists_witnessoldlast * S ((S (l)) * c) + (q))) /\ (((((exists ff_h_pfp_swap_exists_witnessnewi. ff_h_pfp_swap_exists_witnessnewi + S (q) = S ((S (i)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnewi. d = ff_q_pfp_swap_exists_witnessnewi * S ((S (i)) * e) + (q))) /\ (((((exists ff_h_pfp_swap_exists_witnessnewlast. ff_h_pfp_swap_exists_witnessnewlast + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnewlast. d = ff_q_pfp_swap_exists_witnessnewlast * S ((S (l)) * e) + (p))) /\ (forall pfp_j_swap_exists_witness pfp_a_swap_exists_witness. (exists pfp_gap_swap_exists_witnessbound. pfp_gap_swap_exists_witnessbound + S (pfp_j_swap_exists_witness) = (S (l))) -> ~(pfp_j_swap_exists_witness = i) -> ~(pfp_j_swap_exists_witness = l) -> (((exists ff_h_pfp_swap_exists_witnessold. ff_h_pfp_swap_exists_witnessold + S (pfp_a_swap_exists_witness) = S ((S (pfp_j_swap_exists_witness)) * c)) /\ exists ff_q_pfp_swap_exists_witnessold. b = ff_q_pfp_swap_exists_witnessold * S ((S (pfp_j_swap_exists_witness)) * c) + (pfp_a_swap_exists_witness))) -> (((exists ff_h_pfp_swap_exists_witnessnew. ff_h_pfp_swap_exists_witnessnew + S (pfp_a_swap_exists_witness) = S ((S (pfp_j_swap_exists_witness)) * e)) /\ exists ff_q_pfp_swap_exists_witnessnew. d = ff_q_pfp_swap_exists_witnessnew * S ((S (pfp_j_swap_exists_witness)) * e) + (pfp_a_swap_exists_witness)))))))))))))
Complete tactic proof in conservative notation
All 58 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.
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.