PA002X

beta_prefix_extend

Stable checked-use theorem · independently closed

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

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 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.

Read the argument

Proof checkpoints

105 script commands · 21 reading checkpoints · 10 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 (9)
bounded common multiple existsscaled bounded common multiplebounded beta exclusive recode invariantle reflbeta modulus nonzerobinary crt fold stepnew value lt scaled basebeta value lt scaled basebeta at of mod eq bound
01Fix variables and assumptionsL1–4

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

  1. L1
    intro k
  2. L2
    intro b
  3. L3
    intro e
  4. L4
    intro s
02Establish hCL5–7

Establish this local claim before using it. It is not an additional assumption.

  1. L5
    have hC : exists C. (~(C = 0) /\ forall t. (exists h. S t + S h = S k) -> exists q. C = S t * q)
  2. L6
    specialize bounded_common_multiple_exists k
  3. L7
    exact bounded_common_multiple_exists
03Separate the logical casesL8–9

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

  1. L8
    cases hC
  2. L9
    cases hC_witness
04Establish hcm2L10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply scaled bounded common multiple.

  1. L10
    have hcm2 : forall t. (exists h. S t + S h = S k) -> exists q. x * S (b + s) = S t * q
  2. L11
    specialize scaled_bounded_common_multiple k
  3. L12
    specialize scaled_bounded_common_multiple x
  4. L13
    specialize scaled_bounded_common_multiple (S (b + s))
  5. L14
    apply scaled_bounded_common_multiple
  6. L15
    exact hC_witness_right
05Establish hallL16–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply bounded beta exclusive recode invariant.

  1. L16
    have 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)))
  2. L17
    specialize bounded_beta_exclusive_recode_invariant k
  3. L18
    specialize bounded_beta_exclusive_recode_invariant (x * S (b + s))
  4. L19
    specialize bounded_beta_exclusive_recode_invariant b
  5. L20
    specialize bounded_beta_exclusive_recode_invariant e
  6. L21
    apply bounded_beta_exclusive_recode_invariant
  7. L22
    exact hcm2
06Establish hinvL23–27

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

  1. L23
    have 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)))
  2. L24
    specialize hall k
  3. L25
    apply hall
  4. L26
    specialize le_refl k
  5. L27
    exact le_refl
07Separate the logical casesL28–32

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

  1. L28
    cases hinv
  2. L29
    cases hinv_witness
  3. L30
    cases hinv_witness_witness
  4. L31
    cases hinv_witness_witness_right
  5. L32
    cases hinv_witness_witness_right_right
08Establish hcopL33–39

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

  1. L33
    have hcop : forall d. (exists u. x1 = d * u) -> (exists v. S ((S k) * (x * S (b + s))) = d * v) -> d = 1
  2. L34
    specialize hinv_witness_witness_right_right_right k
  3. L35
    apply hinv_witness_witness_right_right_right
  4. L36
    specialize le_refl k
  5. L37
    exact le_refl
  6. L38
    specialize le_refl k
  7. L39
    exact le_refl
09Establish hnew0L40–43

Establish this local claim before using it. It is not an additional assumption.

  1. L40
    have hnew0 : ~(S ((S k) * (x * S (b + s))) = 0)
  2. L41
    specialize beta_modulus_nonzero (x * S (b + s))
  3. L42
    specialize beta_modulus_nonzero k
  4. L43
    exact beta_modulus_nonzero
10Establish hfoldL44–52

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply binary crt fold step.

  1. L44
    have 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)
  2. L45
    specialize binary_crt_fold_step x1
  3. L46
    specialize binary_crt_fold_step (S ((S k) * (x * S (b + s))))
  4. L47
    specialize binary_crt_fold_step x2
  5. L48
    specialize binary_crt_fold_step s
  6. L49
    apply binary_crt_fold_step
  7. L50
    exact hinv_witness_witness_left
  8. L51
    exact hnew0
  9. L52
    exact hcop
11Separate the logical casesL53–54

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

  1. L53
    cases hfold
  2. L54
    cases hfold_witness
12Construct an explicit witnessL55–56

Supply the displayed value, then prove that it has the required property.

  1. L55
    exists x3
  2. L56
    exists x * S (b + s)
13Separate the logical casesL57–57

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

  1. L57
    split
14Use earlier factsL58–67

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

  1. L58
    specialize beta_at_of_mod_eq_bound x3
  2. L59
    specialize beta_at_of_mod_eq_bound (x * S (b + s))
  3. L60
    specialize beta_at_of_mod_eq_bound k
  4. L61
    specialize beta_at_of_mod_eq_bound s
  5. L62
    apply beta_at_of_mod_eq_bound
  6. L63
    specialize new_value_lt_scaled_base b
  7. L64
    specialize new_value_lt_scaled_base s
  8. L65
    specialize new_value_lt_scaled_base x
  9. L66
    specialize new_value_lt_scaled_base k
  10. L67
    apply new_value_lt_scaled_base
15Use earlier factsL68–69

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

  1. L68
    exact hC_witness_left
  2. L69
    exact hfold_witness_right
16Fix variables and assumptionsL70–73

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

  1. L70
    intro i
  2. L71
    intro a
  3. L72
    intro hi
  4. L73
    intro hati
17Establish hmiL74–77

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinv witness witness right left.

  1. L74
    have hmi : exists q. x1 = S ((S i) * (x * S (b + s))) * q
  2. L75
    specialize hinv_witness_witness_right_left i
  3. L76
    apply hinv_witness_witness_right_left
  4. L77
    exact hi
18Establish hzoldL78–83

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hinv witness witness right right left.

  1. L78
    have hzold : exists u v. x2 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  2. L79
    specialize hinv_witness_witness_right_right_left i
  3. L80
    specialize hinv_witness_witness_right_right_left a
  4. L81
    apply hinv_witness_witness_right_right_left
  5. L82
    exact hi
  6. L83
    exact hati
19Establish hznewL84–93

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

  1. L84
    have hznew : exists u v. x3 + S ((S i) * (x * S (b + s))) * u = a + S ((S i) * (x * S (b + s))) * v
  2. L85
    specialize hfold_witness_left (S ((S i) * (x * S (b + s))))
  3. L86
    specialize hfold_witness_left a
  4. L87
    apply hfold_witness_left
  5. L88
    exact hmi
  6. L89
    exact hzold
  7. L90
    specialize beta_at_of_mod_eq_bound x3
  8. L91
    specialize beta_at_of_mod_eq_bound (x * S (b + s))
  9. L92
    specialize beta_at_of_mod_eq_bound i
  10. L93
    specialize beta_at_of_mod_eq_bound a
20Use earlier factsL94–103

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

  1. L94
    apply beta_at_of_mod_eq_bound
  2. L95
    specialize beta_value_lt_scaled_base b
  3. L96
    specialize beta_value_lt_scaled_base e
  4. L97
    specialize beta_value_lt_scaled_base i
  5. L98
    specialize beta_value_lt_scaled_base a
  6. L99
    specialize beta_value_lt_scaled_base x
  7. L100
    specialize beta_value_lt_scaled_base s
  8. L101
    specialize beta_value_lt_scaled_base i
  9. L102
    apply beta_value_lt_scaled_base
  10. L103
    exact hati
21Use earlier factsL104–105

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

  1. L104
    exact hC_witness_left
  2. L105
    exact hznew

Library-wide reading audit

Original exact command ledger · 105 lines
  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