AF0012

factor_permutation_swap_reflect_unchanged

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

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

∀ b. ∀ c. ∀ d. ∀ e. ∀ l. ∀ i. ∀ p. ∀ q. ∀ k. ∀ a. BetaAt(b,c,i,p) ∧ (BetaAt(b,c,l,q) ∧ (BetaAt(d,e,i,q) ∧ (BetaAt(d,e,l,p) ∧ (∀ x. ∀ y. Lt(x,S l) → ¬x = i → ¬x = l → BetaAt(b,c,x,y) → BetaAt(d,e,x,y))))) → Lt(k,S l) → ¬k = i → ¬k = l → BetaAt(d,e,k,a) → BetaAt(b,c,k,a)

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

Definition DAG

Lt(a,b) · 2BetaAt(b,c,i,x) · 10

Actual proof prerequisites

beta_at_exists · checked external prerequisitebeta_at_unique · checked external prerequisite
Original expanded first-order 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)))

Complete tactic proof in conservative notation

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

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.

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.

  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 : ∃ z. BetaAt(b,c,k,z)Definitions: BetaAt(b,c,k,z)Original native command in the exact edition
  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 : BetaAt(d,e,k,x)Definitions: BetaAt(d,e,k,x)Original native command in the exact edition
  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 defined 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 : ∃ z. BetaAt(b,c,k,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 : BetaAt(d,e,k,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