AF000F

factor_permutation_matching_append

A matching map stays matching when the same actual last factor is appended to both lists and the fresh last index is appended to the map.

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. ∀ u. ∀ v. ∀ U. ∀ V. ∀ l. ∀ p. FactorListMatching(b,c,d,e,u,v,l) → BetaAt(U,V,l,l) ∧ (∀ x. ∀ y. Lt(x,l) → BetaAt(u,v,x,y) → BetaAt(U,V,x,y)) → BetaAt(b,c,l,p) → BetaAt(d,e,l,p) → FactorListMatching(b,c,d,e,U,V,S l)

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

Definition DAG

FactorListMatching(b,c,d,e,u,v,l) · 2Lt(a,b) · 2BetaAt(b,c,i,x) · 6

Actual proof prerequisites

finite_lt_succ_eq_or_lt · checked external prerequisitebeta_at_unique · checked external prerequisitefactor_permutation_prefix_reflect
Original expanded first-order statement 
forall b c d e u v U V l p. (forall pfp_i_append_old pfp_j_append_old pfp_a_append_old. (exists pfp_gap_append_oldbound. pfp_gap_append_oldbound + S (pfp_i_append_old) = (l)) -> (((exists ff_h_pfp_append_oldmap. ff_h_pfp_append_oldmap + S (pfp_j_append_old) = S ((S (pfp_i_append_old)) * v)) /\ exists ff_q_pfp_append_oldmap. u = ff_q_pfp_append_oldmap * S ((S (pfp_i_append_old)) * v) + (pfp_j_append_old))) -> (((exists ff_h_pfp_append_oldsource. ff_h_pfp_append_oldsource + S (pfp_a_append_old) = S ((S (pfp_i_append_old)) * c)) /\ exists ff_q_pfp_append_oldsource. b = ff_q_pfp_append_oldsource * S ((S (pfp_i_append_old)) * c) + (pfp_a_append_old))) -> (((exists ff_h_pfp_append_oldtarget. ff_h_pfp_append_oldtarget + S (pfp_a_append_old) = S ((S (pfp_j_append_old)) * e)) /\ exists ff_q_pfp_append_oldtarget. d = ff_q_pfp_append_oldtarget * S ((S (pfp_j_append_old)) * e) + (pfp_a_append_old)))) -> (((((exists ff_h_pfp_append_extensionlast. ff_h_pfp_append_extensionlast + S (l) = S ((S (l)) * V)) /\ exists ff_q_pfp_append_extensionlast. U = ff_q_pfp_append_extensionlast * S ((S (l)) * V) + (l))) /\ (forall pfp_i_append_extensionprefix pfp_a_append_extensionprefix. (exists pfp_gap_append_extensionprefixbound. pfp_gap_append_extensionprefixbound + S (pfp_i_append_extensionprefix) = (l)) -> (((exists ff_h_pfp_append_extensionprefixold. ff_h_pfp_append_extensionprefixold + S (pfp_a_append_extensionprefix) = S ((S (pfp_i_append_extensionprefix)) * v)) /\ exists ff_q_pfp_append_extensionprefixold. u = ff_q_pfp_append_extensionprefixold * S ((S (pfp_i_append_extensionprefix)) * v) + (pfp_a_append_extensionprefix))) -> (((exists ff_h_pfp_append_extensionprefixnew. ff_h_pfp_append_extensionprefixnew + S (pfp_a_append_extensionprefix) = S ((S (pfp_i_append_extensionprefix)) * V)) /\ exists ff_q_pfp_append_extensionprefixnew. U = ff_q_pfp_append_extensionprefixnew * S ((S (pfp_i_append_extensionprefix)) * V) + (pfp_a_append_extensionprefix)))))) -> (((exists ff_h_pfp_append_left. ff_h_pfp_append_left + S (p) = S ((S (l)) * c)) /\ exists ff_q_pfp_append_left. b = ff_q_pfp_append_left * S ((S (l)) * c) + (p))) -> (((exists ff_h_pfp_append_right. ff_h_pfp_append_right + S (p) = S ((S (l)) * e)) /\ exists ff_q_pfp_append_right. d = ff_q_pfp_append_right * S ((S (l)) * e) + (p))) -> (forall pfp_i_append_new pfp_j_append_new pfp_a_append_new. (exists pfp_gap_append_newbound. pfp_gap_append_newbound + S (pfp_i_append_new) = (S l)) -> (((exists ff_h_pfp_append_newmap. ff_h_pfp_append_newmap + S (pfp_j_append_new) = S ((S (pfp_i_append_new)) * V)) /\ exists ff_q_pfp_append_newmap. U = ff_q_pfp_append_newmap * S ((S (pfp_i_append_new)) * V) + (pfp_j_append_new))) -> (((exists ff_h_pfp_append_newsource. ff_h_pfp_append_newsource + S (pfp_a_append_new) = S ((S (pfp_i_append_new)) * c)) /\ exists ff_q_pfp_append_newsource. b = ff_q_pfp_append_newsource * S ((S (pfp_i_append_new)) * c) + (pfp_a_append_new))) -> (((exists ff_h_pfp_append_newtarget. ff_h_pfp_append_newtarget + S (pfp_a_append_new) = S ((S (pfp_j_append_new)) * e)) /\ exists ff_q_pfp_append_newtarget. d = ff_q_pfp_append_newtarget * S ((S (pfp_j_append_new)) * e) + (pfp_a_append_new))))

Complete tactic proof in conservative notation

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

73 script commands · 14 reading checkpoints · 4 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.

Named ingredients (1)
factor permutation prefix reflect
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 u
  6. L6
    intro v
  7. L7
    intro U
  8. L8
    intro V
  9. L9
    intro l
  10. L10
    intro p
02Fix variables and assumptionsL11–14

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

  1. L11
    intro hm
  2. L12
    intro hext
  3. L13
    intro hleft
  4. L14
    intro hright
03Separate the logical casesL15–15

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

  1. L15
    cases hext
04Fix variables and assumptionsL16–21

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

  1. L16
    intro i
  2. L17
    intro j
  3. L18
    intro a
  4. L19
    intro hi
  5. L20
    intro hmap
  6. L21
    intro hsource
05Establish hcaseL22–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply finite lt succ eq or lt.

  1. L22
    have hcase : i = l ∨ Lt(i,l)Definitions: Lt(i,l)Original native command in the exact edition
  2. L23
    specialize finite_lt_succ_eq_or_lt (l)
  3. L24
    specialize finite_lt_succ_eq_or_lt (i)
  4. L25
    apply finite_lt_succ_eq_or_lt
  5. L26
    exact hi
06Separate the logical casesL27–27

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

  1. L27
    cases hcase
07Establish hjL28–37

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

  1. L28
    have hj : j = l
  2. L29
    specialize beta_at_unique (U)
  3. L30
    specialize beta_at_unique (V)
  4. L31
    specialize beta_at_unique (l)
  5. L32
    specialize beta_at_unique (j)
  6. L33
    specialize beta_at_unique (l)
  7. L34
    apply beta_at_unique
  8. L35
    rewrite hcase_left at hmap
  9. L36
    rewrite hcase_left at hmap
  10. L37
    exact hmap
08Use earlier factsL38–38

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

  1. L38
    exact hext_left
09Establish haL39–48

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

  1. L39
    have ha : a = p
  2. L40
    specialize beta_at_unique (b)
  3. L41
    specialize beta_at_unique (c)
  4. L42
    specialize beta_at_unique (l)
  5. L43
    specialize beta_at_unique (a)
  6. L44
    specialize beta_at_unique (p)
  7. L45
    apply beta_at_unique
  8. L46
    rewrite hcase_left at hsource
  9. L47
    rewrite hcase_left at hsource
  10. L48
    exact hsource
10Use earlier factsL49–49

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

  1. L49
    exact hleft
11Calculate and transport equalitiesL50–53

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

  1. L50
    rewrite hj
  2. L51
    rewrite hj
  3. L52
    rewrite ha
  4. L53
    rewrite ha
12Use earlier factsL54–54

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

  1. L54
    exact hright
13Establish holdL55–64

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor permutation prefix reflect.

  1. L55
    have hold : BetaAt(u,v,i,j)Definitions: BetaAt(u,v,i,j)Original native command in the exact edition
  2. L56
    specialize factor_permutation_prefix_reflect (u)
  3. L57
    specialize factor_permutation_prefix_reflect (v)
  4. L58
    specialize factor_permutation_prefix_reflect (U)
  5. L59
    specialize factor_permutation_prefix_reflect (V)
  6. L60
    specialize factor_permutation_prefix_reflect (l)
  7. L61
    specialize factor_permutation_prefix_reflect (i)
  8. L62
    specialize factor_permutation_prefix_reflect (j)
  9. L63
    apply factor_permutation_prefix_reflect
  10. L64
    exact hext_right
14Use earlier factsL65–73

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

  1. L65
    exact hcase_right
  2. L66
    exact hmap
  3. L67
    specialize hm (i)
  4. L68
    specialize hm (j)
  5. L69
    specialize hm (a)
  6. L70
    apply hm
  7. L71
    exact hcase_right
  8. L72
    exact hold
  9. L73
    exact hsource

Library-wide reading audit

Original defined command ledger · 73 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro d
  4. 0004intro e
  5. 0005intro u
  6. 0006intro v
  7. 0007intro U
  8. 0008intro V
  9. 0009intro l
  10. 0010intro p
  11. 0011intro hm
  12. 0012intro hext
  13. 0013intro hleft
  14. 0014intro hright
  15. 0015cases hext
  16. 0016intro i
  17. 0017intro j
  18. 0018intro a
  19. 0019intro hi
  20. 0020intro hmap
  21. 0021intro hsource
  22. 0022have hcase : i = l ∨ Lt(i,l)
  23. 0023specialize finite_lt_succ_eq_or_lt (l)
  24. 0024specialize finite_lt_succ_eq_or_lt (i)
  25. 0025apply finite_lt_succ_eq_or_lt
  26. 0026exact hi
  27. 0027cases hcase
  28. 0028have hj : j = l
  29. 0029specialize beta_at_unique (U)
  30. 0030specialize beta_at_unique (V)
  31. 0031specialize beta_at_unique (l)
  32. 0032specialize beta_at_unique (j)
  33. 0033specialize beta_at_unique (l)
  34. 0034apply beta_at_unique
  35. 0035rewrite hcase_left at hmap
  36. 0036rewrite hcase_left at hmap
  37. 0037exact hmap
  38. 0038exact hext_left
  39. 0039have ha : a = p
  40. 0040specialize beta_at_unique (b)
  41. 0041specialize beta_at_unique (c)
  42. 0042specialize beta_at_unique (l)
  43. 0043specialize beta_at_unique (a)
  44. 0044specialize beta_at_unique (p)
  45. 0045apply beta_at_unique
  46. 0046rewrite hcase_left at hsource
  47. 0047rewrite hcase_left at hsource
  48. 0048exact hsource
  49. 0049exact hleft
  50. 0050rewrite hj
  51. 0051rewrite hj
  52. 0052rewrite ha
  53. 0053rewrite ha
  54. 0054exact hright
  55. 0055have hold : BetaAt(u,v,i,j)
  56. 0056specialize factor_permutation_prefix_reflect (u)
  57. 0057specialize factor_permutation_prefix_reflect (v)
  58. 0058specialize factor_permutation_prefix_reflect (U)
  59. 0059specialize factor_permutation_prefix_reflect (V)
  60. 0060specialize factor_permutation_prefix_reflect (l)
  61. 0061specialize factor_permutation_prefix_reflect (i)
  62. 0062specialize factor_permutation_prefix_reflect (j)
  63. 0063apply factor_permutation_prefix_reflect
  64. 0064exact hext_right
  65. 0065exact hcase_right
  66. 0066exact hmap
  67. 0067specialize hm (i)
  68. 0068specialize hm (j)
  69. 0069specialize hm (a)
  70. 0070apply hm
  71. 0071exact hcase_right
  72. 0072exact hold
  73. 0073exact hsource