PA002X

beta_prefix_extend

Stable checked-use theorem · independently closed

Rebase an arbitrary decoded prefix and append one exact natural value.

Exact expanded PA statement

forall k b e s. exists z c. (((exists h. h + S s = S ((S k) * c)) /\ exists q. z = q * S ((S k) * c) + s) /\ forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> ((exists h. h + S a = S ((S i) * c)) /\ exists q. z = q * S ((S i) * c) + a))

Structural proof guide

Generated structural guide

Rebase an arbitrary decoded prefix and append one exact natural value.

Use the direct prerequisites bounded_common_multiple_exists, scaled_bounded_common_multiple, bounded_beta_exclusive_recode_invariant, le_refl, beta_modulus_nonzero, binary_crt_fold_step, new_value_lt_scaled_base, beta_value_lt_scaled_base, beta_at_of_mod_eq_bound as previously established PA formulas.

The proof proceeds by case analysis (9), intermediate claims (10).

Referenced ingredients

PA000K bounded_common_multiple_exists PA000L scaled_bounded_common_multiple PA002I bounded_beta_exclusive_recode_invariant PA001A le_refl PA000U beta_modulus_nonzero PA0028 binary_crt_fold_step PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base PA002W beta_at_of_mod_eq_bound

Proof neighborhood

Direct dependencies

PA000K bounded_common_multiple_exists PA000L scaled_bounded_common_multiple PA002I bounded_beta_exclusive_recode_invariant PA001A le_refl PA000U beta_modulus_nonzero PA0028 binary_crt_fold_step PA002Q new_value_lt_scaled_base PA002T beta_value_lt_scaled_base PA002W beta_at_of_mod_eq_bound

Direct dependents

PA002Y beta_range_succ_extend PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0044 beta_repeat_succ_extend PA004J beta_prefix_replace_exists PA0073 gauss_signed_half_prefix_extend PA007D beta_magnitude_predecessor_recode_exists PA007F beta_sign_factor_prefix_extend PA007K beta_pointwise_mul_prefix_extend PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008R prime_scaled_inverse_prefix_extend PA0093 finite_inverse_choice_prefix_extend PA009K beta_prefix_append_two_exists PA00A5 prime_inverse_prefix_extend PA00BX beta_division_prefix_extend PA00DC eisenstein_row_indicator_prefix_extend PA00DI eisenstein_rectangle_row_count_prefix_extend PA00E8 eisenstein_transposed_column_prefix_extend PA00EH eisenstein_transposed_column_count_prefix_extend PA00EW eisenstein_successor_row_split_prefix_extend

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.

  1. 0001intro k
  2. 0002intro b
  3. 0003intro e
  4. 0004intro s
  5. 0005have hC : exists C. (~(C = 0) /\ forall t. (exists h. S t + S h = S k) -> exists q. C = S t * q)
  6. 0006specialize bounded_common_multiple_exists k
  7. 0007exact bounded_common_multiple_exists
  8. 0008cases hC
  9. 0009cases hC_witness
  10. 0010have hcm2 : forall t. (exists h. S t + S h = S k) -> exists q. x * S (b + s) = S t * q
  11. 0011specialize scaled_bounded_common_multiple k
  12. 0012specialize scaled_bounded_common_multiple x
  13. 0013specialize scaled_bounded_common_multiple (S (b + s))
  14. 0014apply scaled_bounded_common_multiple
  15. 0015exact hC_witness_right
  16. 0016have hall : forall n. (exists h. h + n = k) -> exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = n) -> exists q. P = S ((S i) * (x * S (b + s))) * q) /\ ((forall i a. (exists h. h + S i = n) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + n = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
  17. 0017specialize bounded_beta_exclusive_recode_invariant k
  18. 0018specialize bounded_beta_exclusive_recode_invariant (x * S (b + s))
  19. 0019specialize bounded_beta_exclusive_recode_invariant b
  20. 0020specialize bounded_beta_exclusive_recode_invariant e
  21. 0021apply bounded_beta_exclusive_recode_invariant
  22. 0022exact hcm2
  23. 0023have hinv : exists P z. (~(P = 0) /\ ((forall i. (exists h. h + S i = k) -> exists q. P = S ((S i) * (x * S (b + s))) * q) /\ ((forall i a. (exists h. h + S i = k) -> ((exists h. h + S a = S ((S i) * e)) /\ exists q. b = q * S ((S i) * e) + a) -> exists u v. z + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v) /\ forall j. (exists g. g + k = j) -> (exists h. h + j = k) -> forall d. (exists u. P = d * u) -> (exists v. S ((S j) * (x * S (b + s))) = d * v) -> d = 1)))
  24. 0024specialize hall k
  25. 0025apply hall
  26. 0026specialize le_refl k
  27. 0027exact le_refl
  28. 0028cases hinv
  29. 0029cases hinv_witness
  30. 0030cases hinv_witness_witness
  31. 0031cases hinv_witness_witness_right
  32. 0032cases hinv_witness_witness_right_right
  33. 0033have hcop : forall d. (exists u. x1 = d * u) -> (exists v. S ((S k) * (x * S (b + s))) = d * v) -> d = 1
  34. 0034specialize hinv_witness_witness_right_right_right k
  35. 0035apply hinv_witness_witness_right_right_right
  36. 0036specialize le_refl k
  37. 0037exact le_refl
  38. 0038specialize le_refl k
  39. 0039exact le_refl
  40. 0040have hnew0 : ~(S ((S k) * (x * S (b + s))) = 0)
  41. 0041specialize beta_modulus_nonzero (x * S (b + s))
  42. 0042specialize beta_modulus_nonzero k
  43. 0043exact beta_modulus_nonzero
  44. 0044have hfold : exists z2. ((forall m a. (exists q. x1 = m * q) -> (exists u v. x2 + m * u = a + m * v) -> exists r t. z2 + m * r = a + m * t) /\ exists q r. z2 + S ((S k) * (x * S (b + s))) * q = s + S ((S k) * (x * S (b + s))) * r)
  45. 0045specialize binary_crt_fold_step x1
  46. 0046specialize binary_crt_fold_step (S ((S k) * (x * S (b + s))))
  47. 0047specialize binary_crt_fold_step x2
  48. 0048specialize binary_crt_fold_step s
  49. 0049apply binary_crt_fold_step
  50. 0050exact hinv_witness_witness_left
  51. 0051exact hnew0
  52. 0052exact hcop
  53. 0053cases hfold
  54. 0054cases hfold_witness
  55. 0055exists x3
  56. 0056exists x * S (b + s)
  57. 0057split
  58. 0058specialize beta_at_of_mod_eq_bound x3
  59. 0059specialize beta_at_of_mod_eq_bound (x * S (b + s))
  60. 0060specialize beta_at_of_mod_eq_bound k
  61. 0061specialize beta_at_of_mod_eq_bound s
  62. 0062apply beta_at_of_mod_eq_bound
  63. 0063specialize new_value_lt_scaled_base b
  64. 0064specialize new_value_lt_scaled_base s
  65. 0065specialize new_value_lt_scaled_base x
  66. 0066specialize new_value_lt_scaled_base k
  67. 0067apply new_value_lt_scaled_base
  68. 0068exact hC_witness_left
  69. 0069exact hfold_witness_right
  70. 0070intro i
  71. 0071intro a
  72. 0072intro hi
  73. 0073intro hati
  74. 0074have hmi : exists q. x1 = S ((S i) * (x * S (b + s))) * q
  75. 0075specialize hinv_witness_witness_right_left i
  76. 0076apply hinv_witness_witness_right_left
  77. 0077exact hi
  78. 0078have hzold : exists u v. x2 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  79. 0079specialize hinv_witness_witness_right_right_left i
  80. 0080specialize hinv_witness_witness_right_right_left a
  81. 0081apply hinv_witness_witness_right_right_left
  82. 0082exact hi
  83. 0083exact hati
  84. 0084have hznew : exists u v. x3 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  85. 0085specialize hfold_witness_left (S ((S i) * (x * S (b + s))))
  86. 0086specialize hfold_witness_left a
  87. 0087apply hfold_witness_left
  88. 0088exact hmi
  89. 0089exact hzold
  90. 0090specialize beta_at_of_mod_eq_bound x3
  91. 0091specialize beta_at_of_mod_eq_bound (x * S (b + s))
  92. 0092specialize beta_at_of_mod_eq_bound i
  93. 0093specialize beta_at_of_mod_eq_bound a
  94. 0094apply beta_at_of_mod_eq_bound
  95. 0095specialize beta_value_lt_scaled_base b
  96. 0096specialize beta_value_lt_scaled_base e
  97. 0097specialize beta_value_lt_scaled_base i
  98. 0098specialize beta_value_lt_scaled_base a
  99. 0099specialize beta_value_lt_scaled_base x
  100. 0100specialize beta_value_lt_scaled_base s
  101. 0101specialize beta_value_lt_scaled_base i
  102. 0102apply beta_value_lt_scaled_base
  103. 0103exact hati
  104. 0104exact hC_witness_left
  105. 0105exact hznew