AF0012

factor_permutation_swap_reflect_unchanged

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

An actual swapped prefix reflects back to the original entry at every index other than the two moved indices.

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 k a. (((((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)))))))))))) -> (exists pfp_gap_reflect_swap_bound. pfp_gap_reflect_swap_bound + S (k) = (S l)) -> ~(k = i) -> ~(k = l) -> (((exists ff_h_pfp_reflect_swap_new. ff_h_pfp_reflect_swap_new + S (a) = S ((S (k)) * e)) /\ exists ff_q_pfp_reflect_swap_new. d = ff_q_pfp_reflect_swap_new * S ((S (k)) * e) + (a))) -> (((exists ff_h_pfp_reflect_swap_old. ff_h_pfp_reflect_swap_old + S (a) = S ((S (k)) * c)) /\ exists ff_q_pfp_reflect_swap_old. b = ff_q_pfp_reflect_swap_old * S ((S (k)) * c) + (a)))

Constructive proof overview

Generated structural guide

An actual swapped prefix reflects back to the original entry at every index other than the two moved indices.

The unchanged tactic script uses 2 declared prerequisites and contains 45 exact native proof lines.

Alpha v34 checked-use · first admitted v28 · independently kernel and Lean verified; not Stable

Proof neighborhood

Direct dependencies

beta_at_exists Stable theorem; checked-use authorized beta_at_unique Stable theorem; checked-use authorized

Direct dependents

AF0014 factor_permutation_swap_all_prime AF0017 factor_permutation_matching_unswap

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

45 script commands · 9 reading checkpoints · 3 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.

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 k
  10. L10
    intro a
02Fix variables and assumptionsL11–15

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

  1. L11
    intro hs
  2. L12
    intro hk
  3. L13
    intro hki
  4. L14
    intro hkl
  5. L15
    intro hnew
03Separate the logical casesL16–19

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

  1. L16
    cases hs
  2. L17
    cases hs_right
  3. L18
    cases hs_right_right
  4. L19
    cases hs_right_right_right
04Establish holdL20–24

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at exists.

  1. L20
    have hold : exists z. (((exists ff_h_pfp_swap_original. ff_h_pfp_swap_original + S (z) = S ((S (k)) * c)) /\ exists ff_q_pfp_swap_original. b = ff_q_pfp_swap_original * S ((S (k)) * c) + (z)))
  2. L21
    specialize beta_at_exists (b)
  3. L22
    specialize beta_at_exists (c)
  4. L23
    specialize beta_at_exists (k)
  5. L24
    apply beta_at_exists
05Separate the logical casesL25–25

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

  1. L25
    cases hold
06Establish hmovedL26–33

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hs right right right right.

  1. L26
    have hmoved : ((exists ff_h_pfp_swap_moved. ff_h_pfp_swap_moved + S (x) = S ((S (k)) * e)) /\ exists ff_q_pfp_swap_moved. d = ff_q_pfp_swap_moved * S ((S (k)) * e) + (x))
  2. L27
    specialize hs_right_right_right_right (k)
  3. L28
    specialize hs_right_right_right_right (x)
  4. L29
    apply hs_right_right_right_right
  5. L30
    exact hk
  6. L31
    exact hki
  7. L32
    exact hkl
  8. L33
    exact hold_witness
07Establish heqL34–43

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta at unique.

  1. L34
    have heq : a = x
  2. L35
    specialize beta_at_unique (d)
  3. L36
    specialize beta_at_unique (e)
  4. L37
    specialize beta_at_unique (k)
  5. L38
    specialize beta_at_unique (a)
  6. L39
    specialize beta_at_unique (x)
  7. L40
    apply beta_at_unique
  8. L41
    exact hnew
  9. L42
    exact hmoved
  10. L43
    rewrite heq
08Calculate and transport equalitiesL44–44

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

  1. L44
    rewrite heq
09Use earlier factsL45–45

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

  1. L45
    exact hold_witness

Library-wide reading audit

Original exact command ledger · 45 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 k
  10. 0010intro a
  11. 0011intro hs
  12. 0012intro hk
  13. 0013intro hki
  14. 0014intro hkl
  15. 0015intro hnew
  16. 0016cases hs
  17. 0017cases hs_right
  18. 0018cases hs_right_right
  19. 0019cases hs_right_right_right
  20. 0020have hold : exists z. (((exists ff_h_pfp_swap_original. ff_h_pfp_swap_original + S (z) = S ((S (k)) * c)) /\ exists ff_q_pfp_swap_original. b = ff_q_pfp_swap_original * S ((S (k)) * c) + (z)))
  21. 0021specialize beta_at_exists (b)
  22. 0022specialize beta_at_exists (c)
  23. 0023specialize beta_at_exists (k)
  24. 0024apply beta_at_exists
  25. 0025cases hold
  26. 0026have hmoved : ((exists ff_h_pfp_swap_moved. ff_h_pfp_swap_moved + S (x) = S ((S (k)) * e)) /\ exists ff_q_pfp_swap_moved. d = ff_q_pfp_swap_moved * S ((S (k)) * e) + (x))
  27. 0027specialize hs_right_right_right_right (k)
  28. 0028specialize hs_right_right_right_right (x)
  29. 0029apply hs_right_right_right_right
  30. 0030exact hk
  31. 0031exact hki
  32. 0032exact hkl
  33. 0033exact hold_witness
  34. 0034have heq : a = x
  35. 0035specialize beta_at_unique (d)
  36. 0036specialize beta_at_unique (e)
  37. 0037specialize beta_at_unique (k)
  38. 0038specialize beta_at_unique (a)
  39. 0039specialize beta_at_unique (x)
  40. 0040apply beta_at_unique
  41. 0041exact hnew
  42. 0042exact hmoved
  43. 0043rewrite heq
  44. 0044rewrite heq
  45. 0045exact hold_witness