AF0013

factor_permutation_swap_bijection

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

Swapping two actual map entries preserves boundedness and injectivity and constructively recovers full finite surjectivity.

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

Constructive proof overview

Generated structural guide

Swapping two actual map entries preserves boundedness and injectivity and constructively recovers full finite surjectivity.

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

finite_swap_last_bounded Stable theorem; checked-use authorized finite_swap_last_injective Stable theorem; checked-use authorized finite_bounded_injective_surjective Stable theorem; checked-use authorized

Direct dependents

AF0018 factor_permutation_matched_unswap_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 · 15 reading checkpoints · 2 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.

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 b
  2. L2
    intro c
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro l
  6. L6
    intro i
  7. L7
    intro p
  8. L8
    intro q
  9. L9
    intro hi
  10. L10
    intro hp
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hs
03Separate the logical casesL12–17

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

  1. L12
    cases hp
  2. L13
    cases hp_right
  3. L14
    cases hs
  4. L15
    cases hs_right
  5. L16
    cases hs_right_right
  6. L17
    cases hs_right_right_right
04Establish hbL18–27

Establish this local claim before using it. It is not an additional assumption.

  1. L18
    have hb : forall pfp_i_swap_bounded. (exists pfp_gap_swap_boundedindex. pfp_gap_swap_boundedindex + S (pfp_i_swap_bounded) = (S l)) -> exists pfp_a_swap_bounded. (((exists ff_h_pfp_swap_boundedentry. ff_h_pfp_swap_boundedentry + S (pfp_a_swap_bounded) = S ((S (pfp_i_swap_bounded)) * e)) /\ exists ff_q_pfp_swap_boundedentry. d = ff_q_pfp_swap_boundedentry * S ((S (pfp_i_swap_bounded)) * e) + (pfp_a_swap_bounded))) /\ (exists pfp_gap_swap_boundedvalue. pfp_gap_swap_boundedvalue + S (pfp_a_swap_bounded) = (S l))
  2. L19
    specialize finite_swap_last_bounded (b)
  3. L20
    specialize finite_swap_last_bounded (c)
  4. L21
    specialize finite_swap_last_bounded (d)
  5. L22
    specialize finite_swap_last_bounded (e)
  6. L23
    specialize finite_swap_last_bounded (l)
  7. L24
    specialize finite_swap_last_bounded (S l)
  8. L25
    specialize finite_swap_last_bounded (i)
  9. L26
    specialize finite_swap_last_bounded (p)
  10. L27
    specialize finite_swap_last_bounded (q)
05Use earlier factsL28–28

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

  1. L28
    apply finite_swap_last_bounded
06Calculate and transport equalitiesL29–29

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L29
    refl
07Use earlier factsL30–36

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

  1. L30
    exact hi
  2. L31
    exact hp_left
  3. L32
    exact hs_left
  4. L33
    exact hs_right_left
  5. L34
    exact hs_right_right_left
  6. L35
    exact hs_right_right_right_left
  7. L36
    exact hs_right_right_right_right
08Establish hjL37–46

Establish this local claim before using it. It is not an additional assumption.

  1. L37
    have hj : InjectivePrefix(d,e,S l)Definitions: InjectivePrefix
  2. L38
    specialize finite_swap_last_injective (b)
  3. L39
    specialize finite_swap_last_injective (c)
  4. L40
    specialize finite_swap_last_injective (d)
  5. L41
    specialize finite_swap_last_injective (e)
  6. L42
    specialize finite_swap_last_injective (l)
  7. L43
    specialize finite_swap_last_injective (S l)
  8. L44
    specialize finite_swap_last_injective (i)
  9. L45
    specialize finite_swap_last_injective (p)
  10. L46
    specialize finite_swap_last_injective (q)
09Use earlier factsL47–47

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

  1. L47
    apply finite_swap_last_injective
10Calculate and transport equalitiesL48–48

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L48
    refl
11Use earlier factsL49–55

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

  1. L49
    exact hi
  2. L50
    exact hp_right_left
  3. L51
    exact hs_left
  4. L52
    exact hs_right_left
  5. L53
    exact hs_right_right_left
  6. L54
    exact hs_right_right_right_left
  7. L55
    exact hs_right_right_right_right
12Separate the logical casesL56–56

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

  1. L56
    split
13Use earlier factsL57–57

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

  1. L57
    exact hb
14Separate the logical casesL58–58

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

  1. L58
    split
15Use earlier factsL59–65

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

  1. L59
    exact hj
  2. L60
    specialize finite_bounded_injective_surjective (S l)
  3. L61
    specialize finite_bounded_injective_surjective (d)
  4. L62
    specialize finite_bounded_injective_surjective (e)
  5. L63
    apply finite_bounded_injective_surjective
  6. L64
    exact hb
  7. L65
    exact hj

Library-wide reading audit

Original exact command ledger · 65 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro l
  6. 0006intro i
  7. 0007intro p
  8. 0008intro q
  9. 0009intro hi
  10. 0010intro hp
  11. 0011intro hs
  12. 0012cases hp
  13. 0013cases hp_right
  14. 0014cases hs
  15. 0015cases hs_right
  16. 0016cases hs_right_right
  17. 0017cases hs_right_right_right
  18. 0018have hb : forall pfp_i_swap_bounded. (exists pfp_gap_swap_boundedindex. pfp_gap_swap_boundedindex + S (pfp_i_swap_bounded) = (S l)) -> exists pfp_a_swap_bounded. (((exists ff_h_pfp_swap_boundedentry. ff_h_pfp_swap_boundedentry + S (pfp_a_swap_bounded) = S ((S (pfp_i_swap_bounded)) * e)) /\ exists ff_q_pfp_swap_boundedentry. d = ff_q_pfp_swap_boundedentry * S ((S (pfp_i_swap_bounded)) * e) + (pfp_a_swap_bounded))) /\ (exists pfp_gap_swap_boundedvalue. pfp_gap_swap_boundedvalue + S (pfp_a_swap_bounded) = (S l))
  19. 0019specialize finite_swap_last_bounded (b)
  20. 0020specialize finite_swap_last_bounded (c)
  21. 0021specialize finite_swap_last_bounded (d)
  22. 0022specialize finite_swap_last_bounded (e)
  23. 0023specialize finite_swap_last_bounded (l)
  24. 0024specialize finite_swap_last_bounded (S l)
  25. 0025specialize finite_swap_last_bounded (i)
  26. 0026specialize finite_swap_last_bounded (p)
  27. 0027specialize finite_swap_last_bounded (q)
  28. 0028apply finite_swap_last_bounded
  29. 0029refl
  30. 0030exact hi
  31. 0031exact hp_left
  32. 0032exact hs_left
  33. 0033exact hs_right_left
  34. 0034exact hs_right_right_left
  35. 0035exact hs_right_right_right_left
  36. 0036exact hs_right_right_right_right
  37. 0037have hj : forall pfp_i_swap_injective pfp_j_swap_injective pfp_a_swap_injective. (exists pfp_gap_swap_injectivefirst. pfp_gap_swap_injectivefirst + S (pfp_i_swap_injective) = (S l)) -> (exists pfp_gap_swap_injectivesecond. pfp_gap_swap_injectivesecond + S (pfp_j_swap_injective) = (S l)) -> (((exists ff_h_pfp_swap_injectiveleft. ff_h_pfp_swap_injectiveleft + S (pfp_a_swap_injective) = S ((S (pfp_i_swap_injective)) * e)) /\ exists ff_q_pfp_swap_injectiveleft. d = ff_q_pfp_swap_injectiveleft * S ((S (pfp_i_swap_injective)) * e) + (pfp_a_swap_injective))) -> (((exists ff_h_pfp_swap_injectiveright. ff_h_pfp_swap_injectiveright + S (pfp_a_swap_injective) = S ((S (pfp_j_swap_injective)) * e)) /\ exists ff_q_pfp_swap_injectiveright. d = ff_q_pfp_swap_injectiveright * S ((S (pfp_j_swap_injective)) * e) + (pfp_a_swap_injective))) -> pfp_i_swap_injective = pfp_j_swap_injective
  38. 0038specialize finite_swap_last_injective (b)
  39. 0039specialize finite_swap_last_injective (c)
  40. 0040specialize finite_swap_last_injective (d)
  41. 0041specialize finite_swap_last_injective (e)
  42. 0042specialize finite_swap_last_injective (l)
  43. 0043specialize finite_swap_last_injective (S l)
  44. 0044specialize finite_swap_last_injective (i)
  45. 0045specialize finite_swap_last_injective (p)
  46. 0046specialize finite_swap_last_injective (q)
  47. 0047apply finite_swap_last_injective
  48. 0048refl
  49. 0049exact hi
  50. 0050exact hp_right_left
  51. 0051exact hs_left
  52. 0052exact hs_right_left
  53. 0053exact hs_right_right_left
  54. 0054exact hs_right_right_right_left
  55. 0055exact hs_right_right_right_right
  56. 0056split
  57. 0057exact hb
  58. 0058split
  59. 0059exact hj
  60. 0060specialize finite_bounded_injective_surjective (S l)
  61. 0061specialize finite_bounded_injective_surjective (d)
  62. 0062specialize finite_bounded_injective_surjective (e)
  63. 0063apply finite_bounded_injective_surjective
  64. 0064exact hb
  65. 0065exact hj