Swapping two actual map entries preserves boundedness and injectivity and constructively recovers full finite 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.
forall b c d e l i p q. (exists pfp_gap_bijection_swap_index. pfp_gap_bijection_swap_index + S (i) = (l)) -> (((forall pfp_i_bijection_swap_oldbounded. (exists pfp_gap_bijection_swap_oldboundedindex. pfp_gap_bijection_swap_oldboundedindex + S (pfp_i_bijection_swap_oldbounded) = (S l)) -> exists pfp_a_bijection_swap_oldbounded. (((exists ff_h_pfp_bijection_swap_oldboundedentry. ff_h_pfp_bijection_swap_oldboundedentry + S (pfp_a_bijection_swap_oldbounded) = S ((S (pfp_i_bijection_swap_oldbounded)) * c)) /\ exists ff_q_pfp_bijection_swap_oldboundedentry. b = ff_q_pfp_bijection_swap_oldboundedentry * S ((S (pfp_i_bijection_swap_oldbounded)) * c) + (pfp_a_bijection_swap_oldbounded))) /\ (exists pfp_gap_bijection_swap_oldboundedvalue. pfp_gap_bijection_swap_oldboundedvalue + S (pfp_a_bijection_swap_oldbounded) = (S l))) /\ (((forall pfp_i_bijection_swap_oldinjective pfp_j_bijection_swap_oldinjective pfp_a_bijection_swap_oldinjective. (exists pfp_gap_bijection_swap_oldinjectivefirst. pfp_gap_bijection_swap_oldinjectivefirst + S (pfp_i_bijection_swap_oldinjective) = (S l)) -> (exists pfp_gap_bijection_swap_oldinjectivesecond. pfp_gap_bijection_swap_oldinjectivesecond + S (pfp_j_bijection_swap_oldinjective) = (S l)) -> (((exists ff_h_pfp_bijection_swap_oldinjectiveleft. ff_h_pfp_bijection_swap_oldinjectiveleft + S (pfp_a_bijection_swap_oldinjective) = S ((S (pfp_i_bijection_swap_oldinjective)) * c)) /\ exists ff_q_pfp_bijection_swap_oldinjectiveleft. b = ff_q_pfp_bijection_swap_oldinjectiveleft * S ((S (pfp_i_bijection_swap_oldinjective)) * c) + (pfp_a_bijection_swap_oldinjective))) -> (((exists ff_h_pfp_bijection_swap_oldinjectiveright. ff_h_pfp_bijection_swap_oldinjectiveright + S (pfp_a_bijection_swap_oldinjective) = S ((S (pfp_j_bijection_swap_oldinjective)) * c)) /\ exists ff_q_pfp_bijection_swap_oldinjectiveright. b = ff_q_pfp_bijection_swap_oldinjectiveright * S ((S (pfp_j_bijection_swap_oldinjective)) * c) + (pfp_a_bijection_swap_oldinjective))) -> pfp_i_bijection_swap_oldinjective = pfp_j_bijection_swap_oldinjective) /\ (forall pfp_a_bijection_swap_oldsurjective. (exists pfp_gap_bijection_swap_oldsurjectivevalue. pfp_gap_bijection_swap_oldsurjectivevalue + S (pfp_a_bijection_swap_oldsurjective) = (S l)) -> exists pfp_i_bijection_swap_oldsurjective. (exists pfp_gap_bijection_swap_oldsurjectiveindex. pfp_gap_bijection_swap_oldsurjectiveindex + S (pfp_i_bijection_swap_oldsurjective) = (S l)) /\ (((exists ff_h_pfp_bijection_swap_oldsurjectiveentry. ff_h_pfp_bijection_swap_oldsurjectiveentry + S (pfp_a_bijection_swap_oldsurjective) = S ((S (pfp_i_bijection_swap_oldsurjective)) * c)) /\ exists ff_q_pfp_bijection_swap_oldsurjectiveentry. b = ff_q_pfp_bijection_swap_oldsurjectiveentry * S ((S (pfp_i_bijection_swap_oldsurjective)) * c) + (pfp_a_bijection_swap_oldsurjective)))))))) -> (((((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)))))))))))) -> (((forall pfp_i_bijection_swap_newbounded. (exists pfp_gap_bijection_swap_newboundedindex. pfp_gap_bijection_swap_newboundedindex + S (pfp_i_bijection_swap_newbounded) = (S l)) -> exists pfp_a_bijection_swap_newbounded. (((exists ff_h_pfp_bijection_swap_newboundedentry. ff_h_pfp_bijection_swap_newboundedentry + S (pfp_a_bijection_swap_newbounded) = S ((S (pfp_i_bijection_swap_newbounded)) * e)) /\ exists ff_q_pfp_bijection_swap_newboundedentry. d = ff_q_pfp_bijection_swap_newboundedentry * S ((S (pfp_i_bijection_swap_newbounded)) * e) + (pfp_a_bijection_swap_newbounded))) /\ (exists pfp_gap_bijection_swap_newboundedvalue. pfp_gap_bijection_swap_newboundedvalue + S (pfp_a_bijection_swap_newbounded) = (S l))) /\ (((forall pfp_i_bijection_swap_newinjective pfp_j_bijection_swap_newinjective pfp_a_bijection_swap_newinjective. (exists pfp_gap_bijection_swap_newinjectivefirst. pfp_gap_bijection_swap_newinjectivefirst + S (pfp_i_bijection_swap_newinjective) = (S l)) -> (exists pfp_gap_bijection_swap_newinjectivesecond. pfp_gap_bijection_swap_newinjectivesecond + S (pfp_j_bijection_swap_newinjective) = (S l)) -> (((exists ff_h_pfp_bijection_swap_newinjectiveleft. ff_h_pfp_bijection_swap_newinjectiveleft + S (pfp_a_bijection_swap_newinjective) = S ((S (pfp_i_bijection_swap_newinjective)) * e)) /\ exists ff_q_pfp_bijection_swap_newinjectiveleft. d = ff_q_pfp_bijection_swap_newinjectiveleft * S ((S (pfp_i_bijection_swap_newinjective)) * e) + (pfp_a_bijection_swap_newinjective))) -> (((exists ff_h_pfp_bijection_swap_newinjectiveright. ff_h_pfp_bijection_swap_newinjectiveright + S (pfp_a_bijection_swap_newinjective) = S ((S (pfp_j_bijection_swap_newinjective)) * e)) /\ exists ff_q_pfp_bijection_swap_newinjectiveright. d = ff_q_pfp_bijection_swap_newinjectiveright * S ((S (pfp_j_bijection_swap_newinjective)) * e) + (pfp_a_bijection_swap_newinjective))) -> pfp_i_bijection_swap_newinjective = pfp_j_bijection_swap_newinjective) /\ (forall pfp_a_bijection_swap_newsurjective. (exists pfp_gap_bijection_swap_newsurjectivevalue. pfp_gap_bijection_swap_newsurjectivevalue + S (pfp_a_bijection_swap_newsurjective) = (S l)) -> exists pfp_i_bijection_swap_newsurjective. (exists pfp_gap_bijection_swap_newsurjectiveindex. pfp_gap_bijection_swap_newsurjectiveindex + S (pfp_i_bijection_swap_newsurjective) = (S l)) /\ (((exists ff_h_pfp_bijection_swap_newsurjectiveentry. ff_h_pfp_bijection_swap_newsurjectiveentry + S (pfp_a_bijection_swap_newsurjective) = S ((S (pfp_i_bijection_swap_newsurjective)) * e)) /\ exists ff_q_pfp_bijection_swap_newsurjectiveentry. d = ff_q_pfp_bijection_swap_newsurjectiveentry * S ((S (pfp_i_bijection_swap_newsurjective)) * e) + (pfp_a_bijection_swap_newsurjective))))))))
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.
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.
01Fix variables and assumptionsL1–10
Work with arbitrary variables or the premises of the current implication.