PA008R

prime_scaled_inverse_prefix_extend

Alpha v16 checked-use theorem · independently closed; not Stable

Append one actual scaled-inverse value to a zero-based source prefix.

Exact expanded PA statement

forall p a n b c l sl. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_extend_prime esi_prime_right_esip_extend_prime. p = esi_prime_left_esip_extend_prime * esi_prime_right_esip_extend_prime -> esi_prime_left_esip_extend_prime = 1 \/ esi_prime_right_esip_extend_prime = 1)) -> ~(a = 0) -> (exists esip_gap_extend_target_bound. esip_gap_extend_target_bound + S (a) = p) -> (exists esip_gap_extend_length_bound. esip_gap_extend_length_bound + S (l) = n) -> sl = S l -> (forall esip_index_extend_before. (exists esip_gap_extend_before_prefix_bound. esip_gap_extend_before_prefix_bound + S (esip_index_extend_before) = l) -> exists esip_mate_extend_before. ((((exists ff_h_esip_extend_before_entry. ff_h_esip_extend_before_entry + S (esip_mate_extend_before) = S ((S (esip_index_extend_before)) * c)) /\ exists ff_q_esip_extend_before_entry. b = ff_q_esip_extend_before_entry * S ((S (esip_index_extend_before)) * c) + (esip_mate_extend_before))) /\ ((exists esip_gap_extend_before_relation_index_bound. esip_gap_extend_before_relation_index_bound + S (esip_index_extend_before) = n) /\ ((((~((S esip_index_extend_before) = 0) /\ (exists esip_gap_extend_before_relation_scaled_left_bound. esip_gap_extend_before_relation_scaled_left_bound + S (S esip_index_extend_before) = p))) /\ (((~(esip_mate_extend_before = 0) /\ (exists esip_gap_extend_before_relation_scaled_right_bound. esip_gap_extend_before_relation_scaled_right_bound + S (esip_mate_extend_before) = p))) /\ (exists esi_mod_left_extend_before_relation_scaled_mod esi_mod_right_extend_before_relation_scaled_mod. ((S esip_index_extend_before) * esip_mate_extend_before) + p * esi_mod_left_extend_before_relation_scaled_mod = (a) + p * esi_mod_right_extend_before_relation_scaled_mod))))))) -> exists z d. (forall esip_index_extend_after. (exists esip_gap_extend_after_prefix_bound. esip_gap_extend_after_prefix_bound + S (esip_index_extend_after) = sl) -> exists esip_mate_extend_after. ((((exists ff_h_esip_extend_after_entry. ff_h_esip_extend_after_entry + S (esip_mate_extend_after) = S ((S (esip_index_extend_after)) * d)) /\ exists ff_q_esip_extend_after_entry. z = ff_q_esip_extend_after_entry * S ((S (esip_index_extend_after)) * d) + (esip_mate_extend_after))) /\ ((exists esip_gap_extend_after_relation_index_bound. esip_gap_extend_after_relation_index_bound + S (esip_index_extend_after) = n) /\ ((((~((S esip_index_extend_after) = 0) /\ (exists esip_gap_extend_after_relation_scaled_left_bound. esip_gap_extend_after_relation_scaled_left_bound + S (S esip_index_extend_after) = p))) /\ (((~(esip_mate_extend_after = 0) /\ (exists esip_gap_extend_after_relation_scaled_right_bound. esip_gap_extend_after_relation_scaled_right_bound + S (esip_mate_extend_after) = p))) /\ (exists esi_mod_left_extend_after_relation_scaled_mod esi_mod_right_extend_after_relation_scaled_mod. ((S esip_index_extend_after) * esip_mate_extend_after) + p * esi_mod_left_extend_after_relation_scaled_mod = (a) + p * esi_mod_right_extend_after_relation_scaled_mod)))))))

Structural proof guide

Generated structural guide

Append one actual scaled-inverse value to a zero-based source prefix.

Use the direct prerequisites succ_ne_zero, succ_le_succ, prime_scaled_inverse_exists, beta_prefix_extend, finite_lt_succ_eq_or_lt as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (4), equality transport (8).

Referenced ingredients

PA0005 succ_ne_zero PA002K succ_le_succ PA008Q prime_scaled_inverse_exists PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Proof neighborhood

Direct dependencies

PA0005 succ_ne_zero PA002K succ_le_succ PA008Q prime_scaled_inverse_exists PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt

Direct dependents

PA008S prime_scaled_inverse_prefix_exists_bounded

Formal native tactic body

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

  1. 0001intro p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro b
  5. 0005intro c
  6. 0006intro l
  7. 0007intro sl
  8. 0008intro hpn
  9. 0009intro hp
  10. 0010intro ha0
  11. 0011intro hap
  12. 0012intro hln
  13. 0013intro hsl
  14. 0014intro hprefix
  15. 0015have hsource_bound : exists esip_gap_extend_source_bound. esip_gap_extend_source_bound + S (S l) = p
  16. 0016rewrite hpn
  17. 0017specialize succ_le_succ (S l)
  18. 0018specialize succ_le_succ n
  19. 0019apply succ_le_succ
  20. 0020exact hln
  21. 0021have hnew : exists j. ((((~((S l) = 0) /\ (exists esip_gap_extend_new_scaled_left_bound. esip_gap_extend_new_scaled_left_bound + S (S l) = p))) /\ (((~(j = 0) /\ (exists esip_gap_extend_new_scaled_right_bound. esip_gap_extend_new_scaled_right_bound + S (j) = p))) /\ (exists esi_mod_left_extend_new_scaled_mod esi_mod_right_extend_new_scaled_mod. ((S l) * j) + p * esi_mod_left_extend_new_scaled_mod = (a) + p * esi_mod_right_extend_new_scaled_mod))))
  22. 0022specialize prime_scaled_inverse_exists p
  23. 0023specialize prime_scaled_inverse_exists a
  24. 0024specialize prime_scaled_inverse_exists (S l)
  25. 0025apply prime_scaled_inverse_exists
  26. 0026exact hp
  27. 0027exact ha0
  28. 0028exact hap
  29. 0029specialize succ_ne_zero l
  30. 0030exact succ_ne_zero
  31. 0031exact hsource_bound
  32. 0032cases hnew
  33. 0033specialize beta_prefix_extend l
  34. 0034specialize beta_prefix_extend b
  35. 0035specialize beta_prefix_extend c
  36. 0036specialize beta_prefix_extend x
  37. 0037cases beta_prefix_extend
  38. 0038cases beta_prefix_extend_witness
  39. 0039cases beta_prefix_extend_witness_witness
  40. 0040exists x1
  41. 0041exists x2
  42. 0042intro i
  43. 0043intro hi
  44. 0044rewrite hsl at hi
  45. 0045have hsplit : i = l \/ exists h. h + S i = l
  46. 0046specialize finite_lt_succ_eq_or_lt l
  47. 0047specialize finite_lt_succ_eq_or_lt i
  48. 0048apply finite_lt_succ_eq_or_lt
  49. 0049exact hi
  50. 0050cases hsplit
  51. 0051exists x
  52. 0052split
  53. 0053rewrite hsplit_left
  54. 0054rewrite hsplit_left
  55. 0055exact beta_prefix_extend_witness_witness_left
  56. 0056split
  57. 0057rewrite hsplit_left
  58. 0058exact hln
  59. 0059rewrite hsplit_left
  60. 0060rewrite hsplit_left
  61. 0061rewrite hsplit_left
  62. 0062exact hnew_witness
  63. 0063have hold : exists j. ((((exists ff_h_esip_extend_old_entry. ff_h_esip_extend_old_entry + S (j) = S ((S (i)) * c)) /\ exists ff_q_esip_extend_old_entry. b = ff_q_esip_extend_old_entry * S ((S (i)) * c) + (j))) /\ ((exists esip_gap_extend_old_relation_index_bound. esip_gap_extend_old_relation_index_bound + S (i) = n) /\ ((((~((S i) = 0) /\ (exists esip_gap_extend_old_relation_scaled_left_bound. esip_gap_extend_old_relation_scaled_left_bound + S (S i) = p))) /\ (((~(j = 0) /\ (exists esip_gap_extend_old_relation_scaled_right_bound. esip_gap_extend_old_relation_scaled_right_bound + S (j) = p))) /\ (exists esi_mod_left_extend_old_relation_scaled_mod esi_mod_right_extend_old_relation_scaled_mod. ((S i) * j) + p * esi_mod_left_extend_old_relation_scaled_mod = (a) + p * esi_mod_right_extend_old_relation_scaled_mod))))))
  64. 0064specialize hprefix i
  65. 0065apply hprefix
  66. 0066exact hsplit_right
  67. 0067cases hold
  68. 0068cases hold_witness
  69. 0069exists x3
  70. 0070split
  71. 0071specialize beta_prefix_extend_witness_witness_right i
  72. 0072specialize beta_prefix_extend_witness_witness_right x3
  73. 0073apply beta_prefix_extend_witness_witness_right
  74. 0074exact hsplit_right
  75. 0075exact hold_witness_left
  76. 0076exact hold_witness_right