PA0054

beta_reindex_alignment_swap_last

Stable checked-use theorem · independently closed

Simultaneous interior/final swaps of an index code and target factors preserve alignment.

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 PA statement

forall r s u v b c z d w e n i m x y. (((exists ff_h_align_swap_map_i. ff_h_align_swap_map_i + S (m) = S ((S (i)) * v)) /\ exists ff_q_align_swap_map_i. u = ff_q_align_swap_map_i * S ((S (i)) * v) + (m))) -> (((exists ff_h_align_swap_map_n. ff_h_align_swap_map_n + S (n) = S ((S (n)) * v)) /\ exists ff_q_align_swap_map_n. u = ff_q_align_swap_map_n * S ((S (n)) * v) + (n))) -> (forall k j. (exists h. h + S k = S n) -> ~(k = i) -> ~(k = n) -> (((exists ff_h_align_swap_map_old. ff_h_align_swap_map_old + S (j) = S ((S (k)) * s)) /\ exists ff_q_align_swap_map_old. r = ff_q_align_swap_map_old * S ((S (k)) * s) + (j))) -> (((exists ff_h_align_swap_map_new. ff_h_align_swap_map_new + S (j) = S ((S (k)) * v)) /\ exists ff_q_align_swap_map_new. u = ff_q_align_swap_map_new * S ((S (k)) * v) + (j)))) -> (((exists ff_h_align_swap_source_m. ff_h_align_swap_source_m + S (y) = S ((S (m)) * c)) /\ exists ff_q_align_swap_source_m. b = ff_q_align_swap_source_m * S ((S (m)) * c) + (y))) -> (((exists ff_h_align_swap_source_n. ff_h_align_swap_source_n + S (x) = S ((S (n)) * c)) /\ exists ff_q_align_swap_source_n. b = ff_q_align_swap_source_n * S ((S (n)) * c) + (x))) -> (((exists ff_h_align_swap_target_i. ff_h_align_swap_target_i + S (y) = S ((S (i)) * e)) /\ exists ff_q_align_swap_target_i. w = ff_q_align_swap_target_i * S ((S (i)) * e) + (y))) -> (((exists ff_h_align_swap_target_n. ff_h_align_swap_target_n + S (x) = S ((S (n)) * e)) /\ exists ff_q_align_swap_target_n. w = ff_q_align_swap_target_n * S ((S (n)) * e) + (x))) -> (forall k a. (exists h. h + S k = S n) -> ~(k = i) -> ~(k = n) -> (((exists ff_h_align_swap_target_old. ff_h_align_swap_target_old + S (a) = S ((S (k)) * d)) /\ exists ff_q_align_swap_target_old. z = ff_q_align_swap_target_old * S ((S (k)) * d) + (a))) -> (((exists ff_h_align_swap_target_new. ff_h_align_swap_target_new + S (a) = S ((S (k)) * e)) /\ exists ff_q_align_swap_target_new. w = ff_q_align_swap_target_new * S ((S (k)) * e) + (a)))) -> (forall fpr_i_align_swap_old fpr_j_align_swap_old fpr_x_align_swap_old. (exists fpr_h_align_swap_old. fpr_h_align_swap_old + S fpr_i_align_swap_old = S n) -> (((exists ff_h_align_swap_old_map. ff_h_align_swap_old_map + S (fpr_j_align_swap_old) = S ((S (fpr_i_align_swap_old)) * s)) /\ exists ff_q_align_swap_old_map. r = ff_q_align_swap_old_map * S ((S (fpr_i_align_swap_old)) * s) + (fpr_j_align_swap_old))) -> (((exists ff_h_align_swap_old_source. ff_h_align_swap_old_source + S (fpr_x_align_swap_old) = S ((S (fpr_j_align_swap_old)) * c)) /\ exists ff_q_align_swap_old_source. b = ff_q_align_swap_old_source * S ((S (fpr_j_align_swap_old)) * c) + (fpr_x_align_swap_old))) -> (((exists ff_h_align_swap_old_target. ff_h_align_swap_old_target + S (fpr_x_align_swap_old) = S ((S (fpr_i_align_swap_old)) * d)) /\ exists ff_q_align_swap_old_target. z = ff_q_align_swap_old_target * S ((S (fpr_i_align_swap_old)) * d) + (fpr_x_align_swap_old)))) -> (forall fpr_i_align_swap_new fpr_j_align_swap_new fpr_x_align_swap_new. (exists fpr_h_align_swap_new. fpr_h_align_swap_new + S fpr_i_align_swap_new = S n) -> (((exists ff_h_align_swap_new_map. ff_h_align_swap_new_map + S (fpr_j_align_swap_new) = S ((S (fpr_i_align_swap_new)) * v)) /\ exists ff_q_align_swap_new_map. u = ff_q_align_swap_new_map * S ((S (fpr_i_align_swap_new)) * v) + (fpr_j_align_swap_new))) -> (((exists ff_h_align_swap_new_source. ff_h_align_swap_new_source + S (fpr_x_align_swap_new) = S ((S (fpr_j_align_swap_new)) * c)) /\ exists ff_q_align_swap_new_source. b = ff_q_align_swap_new_source * S ((S (fpr_j_align_swap_new)) * c) + (fpr_x_align_swap_new))) -> (((exists ff_h_align_swap_new_target. ff_h_align_swap_new_target + S (fpr_x_align_swap_new) = S ((S (fpr_i_align_swap_new)) * e)) /\ exists ff_q_align_swap_new_target. w = ff_q_align_swap_new_target * S ((S (fpr_i_align_swap_new)) * e) + (fpr_x_align_swap_new))))

Structural proof guide

Generated structural guide

Simultaneous interior/final swaps of an index code and target factors preserve alignment.

Use the direct prerequisites beta_prefix_swap_last_reflect, beta_at_unique as previously established PA formulas.

The proof proceeds by case analysis (6), intermediate claims (5), equality transport (12).

Referenced ingredients

PA004N beta_prefix_swap_last_reflect PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA004N beta_prefix_swap_last_reflect PA002F beta_at_unique

Direct dependents

PA007X beta_product_permutation_invariant PA00CX beta_sum_permutation_invariant

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

102 script commands · 21 reading checkpoints · 5 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.

Named ingredients (2)
beta prefix swap last reflectbeta at unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro r
  2. L2
    intro s
  3. L3
    intro u
  4. L4
    intro v
  5. L5
    intro b
  6. L6
    intro c
  7. L7
    intro z
  8. L8
    intro d
  9. L9
    intro w
  10. L10
    intro e
02Fix variables and assumptionsL11–20

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

  1. L11
    intro n
  2. L12
    intro i
  3. L13
    intro m
  4. L14
    intro x
  5. L15
    intro y
  6. L16
    intro hmap_i
  7. L17
    intro hmap_n
  8. L18
    intro hmap_preserve
  9. L19
    intro hsource_m
  10. L20
    intro hsource_n
03Fix variables and assumptionsL21–24

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

  1. L21
    intro htarget_i
  2. L22
    intro htarget_n
  3. L23
    intro htarget_preserve
  4. L24
    intro haligned
04Establish hreflectL25–34

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

  1. L25
    have hreflect : forall k j. (exists h. h + S k = S n) -> ((exists h. h + S j = S ((S k) * v)) /\ exists q. u = q * S ((S k) * v) + j) -> (k = i /\ j = m) \/ ((k = n /\ j = n) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S j = S ((S k) * s)) /\ exists q. r = q * S ((S k) * s) + j))))
  2. L26
    specialize beta_prefix_swap_last_reflect r
  3. L27
    specialize beta_prefix_swap_last_reflect s
  4. L28
    specialize beta_prefix_swap_last_reflect u
  5. L29
    specialize beta_prefix_swap_last_reflect v
  6. L30
    specialize beta_prefix_swap_last_reflect n
  7. L31
    specialize beta_prefix_swap_last_reflect i
  8. L32
    specialize beta_prefix_swap_last_reflect n
  9. L33
    specialize beta_prefix_swap_last_reflect m
  10. L34
    apply beta_prefix_swap_last_reflect
05Use earlier factsL35–37

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

  1. L35
    exact hmap_i
  2. L36
    exact hmap_n
  3. L37
    exact hmap_preserve
06Fix variables and assumptionsL38–43

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

  1. L38
    intro k
  2. L39
    intro j
  3. L40
    intro a
  4. L41
    intro hk
  5. L42
    intro hmap
  6. L43
    intro hsource
07Use earlier factsL44–45

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

  1. L44
    specialize hreflect k
  2. L45
    specialize hreflect j
08Establish hcasesL46–49

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

  1. L46
    have hcases : (k = i /\ j = m) \/ ((k = n /\ j = n) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S j = S ((S k) * s)) /\ exists q. r = q * S ((S k) * s) + j))))
  2. L47
    apply hreflect
  3. L48
    exact hk
  4. L49
    exact hmap
09Separate the logical casesL50–51

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

  1. L50
    cases hcases
  2. L51
    cases hcases_left
10Establish hayL52–61

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

  1. L52
    have hay : a = y
  2. L53
    specialize beta_at_unique b
  3. L54
    specialize beta_at_unique c
  4. L55
    specialize beta_at_unique m
  5. L56
    specialize beta_at_unique a
  6. L57
    specialize beta_at_unique y
  7. L58
    apply beta_at_unique
  8. L59
    rewrite hcases_left_right at hsource
  9. L60
    rewrite hcases_left_right at hsource
  10. L61
    exact hsource
11Use earlier factsL62–62

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

  1. L62
    exact hsource_m
12Calculate and transport equalitiesL63–66

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

  1. L63
    rewrite hcases_left_left
  2. L64
    rewrite hcases_left_left
  3. L65
    rewrite hay
  4. L66
    rewrite hay
13Use earlier factsL67–67

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

  1. L67
    exact htarget_i
14Separate the logical casesL68–69

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

  1. L68
    cases hcases_right
  2. L69
    cases hcases_right_left
15Establish haxL70–79

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

  1. L70
    have hax : a = x
  2. L71
    specialize beta_at_unique b
  3. L72
    specialize beta_at_unique c
  4. L73
    specialize beta_at_unique n
  5. L74
    specialize beta_at_unique a
  6. L75
    specialize beta_at_unique x
  7. L76
    apply beta_at_unique
  8. L77
    rewrite hcases_right_left_right at hsource
  9. L78
    rewrite hcases_right_left_right at hsource
  10. L79
    exact hsource
16Use earlier factsL80–80

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

  1. L80
    exact hsource_n
17Calculate and transport equalitiesL81–84

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

  1. L81
    rewrite hcases_right_left_left
  2. L82
    rewrite hcases_right_left_left
  3. L83
    rewrite hax
  4. L84
    rewrite hax
18Use earlier factsL85–85

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

  1. L85
    exact htarget_n
19Separate the logical casesL86–87

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

  1. L86
    cases hcases_right_right
  2. L87
    cases hcases_right_right_right
20Establish hold_targetL88–97

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

  1. L88
    have hold_target : ((exists h. h + S a = S ((S k) * d)) /\ exists q. z = q * S ((S k) * d) + a)
  2. L89
    specialize haligned k
  3. L90
    specialize haligned j
  4. L91
    specialize haligned a
  5. L92
    apply haligned
  6. L93
    exact hk
  7. L94
    exact hcases_right_right_right_right
  8. L95
    exact hsource
  9. L96
    specialize htarget_preserve k
  10. L97
    specialize htarget_preserve a
21Use earlier factsL98–102

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

  1. L98
    apply htarget_preserve
  2. L99
    exact hk
  3. L100
    exact hcases_right_right_left
  4. L101
    exact hcases_right_right_right_left
  5. L102
    exact hold_target

Library-wide reading audit

Original exact command ledger · 102 lines
  1. 0001intro r
  2. 0002intro s
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro z
  8. 0008intro d
  9. 0009intro w
  10. 0010intro e
  11. 0011intro n
  12. 0012intro i
  13. 0013intro m
  14. 0014intro x
  15. 0015intro y
  16. 0016intro hmap_i
  17. 0017intro hmap_n
  18. 0018intro hmap_preserve
  19. 0019intro hsource_m
  20. 0020intro hsource_n
  21. 0021intro htarget_i
  22. 0022intro htarget_n
  23. 0023intro htarget_preserve
  24. 0024intro haligned
  25. 0025have hreflect : forall k j. (exists h. h + S k = S n) -> ((exists h. h + S j = S ((S k) * v)) /\ exists q. u = q * S ((S k) * v) + j) -> (k = i /\ j = m) \/ ((k = n /\ j = n) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S j = S ((S k) * s)) /\ exists q. r = q * S ((S k) * s) + j))))
  26. 0026specialize beta_prefix_swap_last_reflect r
  27. 0027specialize beta_prefix_swap_last_reflect s
  28. 0028specialize beta_prefix_swap_last_reflect u
  29. 0029specialize beta_prefix_swap_last_reflect v
  30. 0030specialize beta_prefix_swap_last_reflect n
  31. 0031specialize beta_prefix_swap_last_reflect i
  32. 0032specialize beta_prefix_swap_last_reflect n
  33. 0033specialize beta_prefix_swap_last_reflect m
  34. 0034apply beta_prefix_swap_last_reflect
  35. 0035exact hmap_i
  36. 0036exact hmap_n
  37. 0037exact hmap_preserve
  38. 0038intro k
  39. 0039intro j
  40. 0040intro a
  41. 0041intro hk
  42. 0042intro hmap
  43. 0043intro hsource
  44. 0044specialize hreflect k
  45. 0045specialize hreflect j
  46. 0046have hcases : (k = i /\ j = m) \/ ((k = n /\ j = n) \/ (~(k = i) /\ (~(k = n) /\ ((exists h. h + S j = S ((S k) * s)) /\ exists q. r = q * S ((S k) * s) + j))))
  47. 0047apply hreflect
  48. 0048exact hk
  49. 0049exact hmap
  50. 0050cases hcases
  51. 0051cases hcases_left
  52. 0052have hay : a = y
  53. 0053specialize beta_at_unique b
  54. 0054specialize beta_at_unique c
  55. 0055specialize beta_at_unique m
  56. 0056specialize beta_at_unique a
  57. 0057specialize beta_at_unique y
  58. 0058apply beta_at_unique
  59. 0059rewrite hcases_left_right at hsource
  60. 0060rewrite hcases_left_right at hsource
  61. 0061exact hsource
  62. 0062exact hsource_m
  63. 0063rewrite hcases_left_left
  64. 0064rewrite hcases_left_left
  65. 0065rewrite hay
  66. 0066rewrite hay
  67. 0067exact htarget_i
  68. 0068cases hcases_right
  69. 0069cases hcases_right_left
  70. 0070have hax : a = x
  71. 0071specialize beta_at_unique b
  72. 0072specialize beta_at_unique c
  73. 0073specialize beta_at_unique n
  74. 0074specialize beta_at_unique a
  75. 0075specialize beta_at_unique x
  76. 0076apply beta_at_unique
  77. 0077rewrite hcases_right_left_right at hsource
  78. 0078rewrite hcases_right_left_right at hsource
  79. 0079exact hsource
  80. 0080exact hsource_n
  81. 0081rewrite hcases_right_left_left
  82. 0082rewrite hcases_right_left_left
  83. 0083rewrite hax
  84. 0084rewrite hax
  85. 0085exact htarget_n
  86. 0086cases hcases_right_right
  87. 0087cases hcases_right_right_right
  88. 0088have hold_target : ((exists h. h + S a = S ((S k) * d)) /\ exists q. z = q * S ((S k) * d) + a)
  89. 0089specialize haligned k
  90. 0090specialize haligned j
  91. 0091specialize haligned a
  92. 0092apply haligned
  93. 0093exact hk
  94. 0094exact hcases_right_right_right_right
  95. 0095exact hsource
  96. 0096specialize htarget_preserve k
  97. 0097specialize htarget_preserve a
  98. 0098apply htarget_preserve
  99. 0099exact hk
  100. 0100exact hcases_right_right_left
  101. 0101exact hcases_right_right_right_left
  102. 0102exact hold_target