PA007F

beta_sign_factor_prefix_extend

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

Append the selected 1/r factor while preserving every earlier decoded factor.

Exact expanded PA statement

forall sb sc fb fc r l a f. (forall gspf_index_recode_before gspf_bit_recode_before. (exists gsp_lt_gap_recode_before_bound. gsp_lt_gap_recode_before_bound + S gspf_index_recode_before = l) -> (((exists ff_h_gspf_recode_before_bit. ff_h_gspf_recode_before_bit + S (gspf_bit_recode_before) = S ((S (gspf_index_recode_before)) * sc)) /\ exists ff_q_gspf_recode_before_bit. sb = ff_q_gspf_recode_before_bit * S ((S (gspf_index_recode_before)) * sc) + (gspf_bit_recode_before))) -> (((gspf_bit_recode_before = 0) /\ (((exists gsp_beta_height_gspf_recode_before_one. gsp_beta_height_gspf_recode_before_one + S (1) = S ((S (gspf_index_recode_before)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_before_one. fb = gsp_beta_quotient_gspf_recode_before_one * S ((S (gspf_index_recode_before)) * fc) + (1)))) \/ ((gspf_bit_recode_before = 1) /\ (((exists ff_h_gspf_recode_before_predecessor. ff_h_gspf_recode_before_predecessor + S (r) = S ((S (gspf_index_recode_before)) * fc)) /\ exists ff_q_gspf_recode_before_predecessor. fb = ff_q_gspf_recode_before_predecessor * S ((S (gspf_index_recode_before)) * fc) + (r)))))) -> (((exists ff_h_recode_source_last. ff_h_recode_source_last + S (a) = S ((S (l)) * sc)) /\ exists ff_q_recode_source_last. sb = ff_q_recode_source_last * S ((S (l)) * sc) + (a))) -> ((a = 0 /\ f = 1) \/ (a = 1 /\ f = r)) -> exists z d. (forall gspf_index_recode_after gspf_bit_recode_after. (exists gsp_lt_gap_recode_after_bound. gsp_lt_gap_recode_after_bound + S gspf_index_recode_after = S l) -> (((exists ff_h_gspf_recode_after_bit. ff_h_gspf_recode_after_bit + S (gspf_bit_recode_after) = S ((S (gspf_index_recode_after)) * sc)) /\ exists ff_q_gspf_recode_after_bit. sb = ff_q_gspf_recode_after_bit * S ((S (gspf_index_recode_after)) * sc) + (gspf_bit_recode_after))) -> (((gspf_bit_recode_after = 0) /\ (((exists gsp_beta_height_gspf_recode_after_one. gsp_beta_height_gspf_recode_after_one + S (1) = S ((S (gspf_index_recode_after)) * d)) /\ exists gsp_beta_quotient_gspf_recode_after_one. z = gsp_beta_quotient_gspf_recode_after_one * S ((S (gspf_index_recode_after)) * d) + (1)))) \/ ((gspf_bit_recode_after = 1) /\ (((exists ff_h_gspf_recode_after_predecessor. ff_h_gspf_recode_after_predecessor + S (r) = S ((S (gspf_index_recode_after)) * d)) /\ exists ff_q_gspf_recode_after_predecessor. z = ff_q_gspf_recode_after_predecessor * S ((S (gspf_index_recode_after)) * d) + (r))))))

Structural proof guide

Generated structural guide

Append the selected 1/r factor while preserving every earlier decoded factor.

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

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

Referenced ingredients

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA002X beta_prefix_extend PA003D finite_lt_succ_eq_or_lt PA002F beta_at_unique

Direct dependents

PA007G beta_sign_factor_prefix_exists

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 sb
  2. 0002intro sc
  3. 0003intro fb
  4. 0004intro fc
  5. 0005intro r
  6. 0006intro l
  7. 0007intro a
  8. 0008intro f
  9. 0009intro hsigns
  10. 0010intro hlast
  11. 0011intro hchosen
  12. 0012specialize beta_prefix_extend l
  13. 0013specialize beta_prefix_extend fb
  14. 0014specialize beta_prefix_extend fc
  15. 0015specialize beta_prefix_extend f
  16. 0016cases beta_prefix_extend
  17. 0017cases beta_prefix_extend_witness
  18. 0018cases beta_prefix_extend_witness_witness
  19. 0019exists x
  20. 0020exists x1
  21. 0021intro i
  22. 0022intro v
  23. 0023intro hi
  24. 0024intro hv
  25. 0025have hsplit : i = l \/ exists gap. gap + S i = l
  26. 0026specialize finite_lt_succ_eq_or_lt l
  27. 0027specialize finite_lt_succ_eq_or_lt i
  28. 0028apply finite_lt_succ_eq_or_lt
  29. 0029exact hi
  30. 0030cases hsplit
  31. 0031have hvlast : ((exists ff_h_recode_top_source. ff_h_recode_top_source + S (v) = S ((S (l)) * sc)) /\ exists ff_q_recode_top_source. sb = ff_q_recode_top_source * S ((S (l)) * sc) + (v))
  32. 0032rewrite hsplit_left at hv
  33. 0033rewrite hsplit_left at hv
  34. 0034exact hv
  35. 0035have hva : v = a
  36. 0036specialize beta_at_unique sb
  37. 0037specialize beta_at_unique sc
  38. 0038specialize beta_at_unique l
  39. 0039specialize beta_at_unique v
  40. 0040specialize beta_at_unique a
  41. 0041apply beta_at_unique
  42. 0042exact hvlast
  43. 0043exact hlast
  44. 0044cases hchosen
  45. 0045cases hchosen_left
  46. 0046left
  47. 0047split
  48. 0048trans a
  49. 0049exact hva
  50. 0050exact hchosen_left_left
  51. 0051have hnew_one : ((exists gsp_beta_height_recode_new_one. gsp_beta_height_recode_new_one + S (1) = S ((S (l)) * x1)) /\ exists gsp_beta_quotient_recode_new_one. x = gsp_beta_quotient_recode_new_one * S ((S (l)) * x1) + (1))
  52. 0052rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  53. 0053rewrite hchosen_left_right at beta_prefix_extend_witness_witness_left
  54. 0054exact beta_prefix_extend_witness_witness_left
  55. 0055rewrite hsplit_left
  56. 0056rewrite hsplit_left
  57. 0057exact hnew_one
  58. 0058cases hchosen_right
  59. 0059right
  60. 0060split
  61. 0061trans a
  62. 0062exact hva
  63. 0063exact hchosen_right_left
  64. 0064have hnew_predecessor : ((exists ff_h_recode_new_predecessor. ff_h_recode_new_predecessor + S (r) = S ((S (l)) * x1)) /\ exists ff_q_recode_new_predecessor. x = ff_q_recode_new_predecessor * S ((S (l)) * x1) + (r))
  65. 0065rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  66. 0066rewrite hchosen_right_right at beta_prefix_extend_witness_witness_left
  67. 0067exact beta_prefix_extend_witness_witness_left
  68. 0068rewrite hsplit_left
  69. 0069rewrite hsplit_left
  70. 0070exact hnew_predecessor
  71. 0071have hold : ((v = 0 /\ (((exists gsp_beta_height_recode_old_one. gsp_beta_height_recode_old_one + S (1) = S ((S (i)) * fc)) /\ exists gsp_beta_quotient_recode_old_one. fb = gsp_beta_quotient_recode_old_one * S ((S (i)) * fc) + (1)))) \/ (v = 1 /\ (((exists ff_h_recode_old_predecessor. ff_h_recode_old_predecessor + S (r) = S ((S (i)) * fc)) /\ exists ff_q_recode_old_predecessor. fb = ff_q_recode_old_predecessor * S ((S (i)) * fc) + (r)))))
  72. 0072specialize hsigns i
  73. 0073specialize hsigns v
  74. 0074apply hsigns
  75. 0075exact hsplit_right
  76. 0076exact hv
  77. 0077cases hold
  78. 0078cases hold_left
  79. 0079left
  80. 0080split
  81. 0081exact hold_left_left
  82. 0082specialize beta_prefix_extend_witness_witness_right i
  83. 0083specialize beta_prefix_extend_witness_witness_right 1
  84. 0084apply beta_prefix_extend_witness_witness_right
  85. 0085exact hsplit_right
  86. 0086exact hold_left_right
  87. 0087cases hold_right
  88. 0088right
  89. 0089split
  90. 0090exact hold_right_left
  91. 0091specialize beta_prefix_extend_witness_witness_right i
  92. 0092specialize beta_prefix_extend_witness_witness_right r
  93. 0093apply beta_prefix_extend_witness_witness_right
  94. 0094exact hsplit_right
  95. 0095exact hold_right_right