PA007G

beta_sign_factor_prefix_exists

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

Every finite beta bit prefix admits a beta-coded 1/r sign-factor prefix.

Exact expanded PA statement

forall sb sc r l e. (((exists ff_u_recode_count_sum ff_v_recode_count_sum. ((((exists ff_h_recode_count_sum_start. ff_h_recode_count_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_start. ff_u_recode_count_sum = ff_q_recode_count_sum_start * S ((S (0)) * ff_v_recode_count_sum) + (0))) /\ ((((exists ff_h_recode_count_sum_terminal. ff_h_recode_count_sum_terminal + S (e) = S ((S (l)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_terminal. ff_u_recode_count_sum = ff_q_recode_count_sum_terminal * S ((S (l)) * ff_v_recode_count_sum) + (e))) /\ forall ff_i_recode_count_sum. (exists ff_lt_recode_count_sum_bound. ff_lt_recode_count_sum_bound + S ff_i_recode_count_sum = l) -> exists ff_a_recode_count_sum ff_r_recode_count_sum ff_s_recode_count_sum. ((((exists ff_h_recode_count_sum_summand. ff_h_recode_count_sum_summand + S (ff_a_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * sc)) /\ exists ff_q_recode_count_sum_summand. sb = ff_q_recode_count_sum_summand * S ((S (ff_i_recode_count_sum)) * sc) + (ff_a_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_partial. ff_h_recode_count_sum_partial + S (ff_r_recode_count_sum) = S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_partial. ff_u_recode_count_sum = ff_q_recode_count_sum_partial * S ((S (ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_r_recode_count_sum))) /\ ((((exists ff_h_recode_count_sum_successor. ff_h_recode_count_sum_successor + S (ff_s_recode_count_sum) = S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum)) /\ exists ff_q_recode_count_sum_successor. ff_u_recode_count_sum = ff_q_recode_count_sum_successor * S ((S (S ff_i_recode_count_sum)) * ff_v_recode_count_sum) + (ff_s_recode_count_sum))) /\ ff_s_recode_count_sum = ff_r_recode_count_sum + ff_a_recode_count_sum)))))) /\ (forall ff_i_recode_count_bits. (exists ff_lt_recode_count_bits_bound. ff_lt_recode_count_bits_bound + S ff_i_recode_count_bits = l) -> exists ff_bit_recode_count_bits. ((((exists ff_h_recode_count_bits_decoded. ff_h_recode_count_bits_decoded + S (ff_bit_recode_count_bits) = S ((S (ff_i_recode_count_bits)) * sc)) /\ exists ff_q_recode_count_bits_decoded. sb = ff_q_recode_count_bits_decoded * S ((S (ff_i_recode_count_bits)) * sc) + (ff_bit_recode_count_bits))) /\ (ff_bit_recode_count_bits = 0 \/ ff_bit_recode_count_bits = 1))))) -> exists fb fc. (forall gspf_index_recode_result gspf_bit_recode_result. (exists gsp_lt_gap_recode_result_bound. gsp_lt_gap_recode_result_bound + S gspf_index_recode_result = l) -> (((exists ff_h_gspf_recode_result_bit. ff_h_gspf_recode_result_bit + S (gspf_bit_recode_result) = S ((S (gspf_index_recode_result)) * sc)) /\ exists ff_q_gspf_recode_result_bit. sb = ff_q_gspf_recode_result_bit * S ((S (gspf_index_recode_result)) * sc) + (gspf_bit_recode_result))) -> (((gspf_bit_recode_result = 0) /\ (((exists gsp_beta_height_gspf_recode_result_one. gsp_beta_height_gspf_recode_result_one + S (1) = S ((S (gspf_index_recode_result)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_result_one. fb = gsp_beta_quotient_gspf_recode_result_one * S ((S (gspf_index_recode_result)) * fc) + (1)))) \/ ((gspf_bit_recode_result = 1) /\ (((exists ff_h_gspf_recode_result_predecessor. ff_h_gspf_recode_result_predecessor + S (r) = S ((S (gspf_index_recode_result)) * fc)) /\ exists ff_q_gspf_recode_result_predecessor. fb = ff_q_gspf_recode_result_predecessor * S ((S (gspf_index_recode_result)) * fc) + (r))))))

Structural proof guide

Generated structural guide

Every finite beta bit prefix admits a beta-coded 1/r sign-factor prefix.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, bit_count_succ_decompose, beta_sign_factor_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (9), intermediate claims (3).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0042 bit_count_succ_decompose PA007F beta_sign_factor_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA0042 bit_count_succ_decompose PA007F beta_sign_factor_prefix_extend

Direct dependents

PA007J beta_sign_factor_product_power_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 r
  4. 0004induction l
  5. 0005intro e
  6. 0006intro hcount
  7. 0007exists 0
  8. 0008exists 0
  9. 0009intro i
  10. 0010intro v
  11. 0011intro hi
  12. 0012intro hv
  13. 0013exfalso
  14. 0014cases hi
  15. 0015have hsi : S i = 0
  16. 0016specialize add_eq_zero_right x
  17. 0017specialize add_eq_zero_right (S i)
  18. 0018apply add_eq_zero_right
  19. 0019exact hi_witness
  20. 0020specialize succ_ne_zero i
  21. 0021apply succ_ne_zero
  22. 0022exact hsi
  23. 0023intro e
  24. 0024intro hcount
  25. 0025have hdecomp : exists a k. (((exists ff_h_recode_count_last. ff_h_recode_count_last + S (a) = S ((S (l)) * sc)) /\ exists ff_q_recode_count_last. sb = ff_q_recode_count_last * S ((S (l)) * sc) + (a))) /\ ((((exists ff_u_recode_count_prefix_sum ff_v_recode_count_prefix_sum. ((((exists ff_h_recode_count_prefix_sum_start. ff_h_recode_count_prefix_sum_start + S (0) = S ((S (0)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_start. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_start * S ((S (0)) * ff_v_recode_count_prefix_sum) + (0))) /\ ((((exists ff_h_recode_count_prefix_sum_terminal. ff_h_recode_count_prefix_sum_terminal + S (k) = S ((S (l)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_terminal. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_terminal * S ((S (l)) * ff_v_recode_count_prefix_sum) + (k))) /\ forall ff_i_recode_count_prefix_sum. (exists ff_lt_recode_count_prefix_sum_bound. ff_lt_recode_count_prefix_sum_bound + S ff_i_recode_count_prefix_sum = l) -> exists ff_a_recode_count_prefix_sum ff_r_recode_count_prefix_sum ff_s_recode_count_prefix_sum. ((((exists ff_h_recode_count_prefix_sum_summand. ff_h_recode_count_prefix_sum_summand + S (ff_a_recode_count_prefix_sum) = S ((S (ff_i_recode_count_prefix_sum)) * sc)) /\ exists ff_q_recode_count_prefix_sum_summand. sb = ff_q_recode_count_prefix_sum_summand * S ((S (ff_i_recode_count_prefix_sum)) * sc) + (ff_a_recode_count_prefix_sum))) /\ ((((exists ff_h_recode_count_prefix_sum_partial. ff_h_recode_count_prefix_sum_partial + S (ff_r_recode_count_prefix_sum) = S ((S (ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_partial. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_partial * S ((S (ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum) + (ff_r_recode_count_prefix_sum))) /\ ((((exists ff_h_recode_count_prefix_sum_successor. ff_h_recode_count_prefix_sum_successor + S (ff_s_recode_count_prefix_sum) = S ((S (S ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum)) /\ exists ff_q_recode_count_prefix_sum_successor. ff_u_recode_count_prefix_sum = ff_q_recode_count_prefix_sum_successor * S ((S (S ff_i_recode_count_prefix_sum)) * ff_v_recode_count_prefix_sum) + (ff_s_recode_count_prefix_sum))) /\ ff_s_recode_count_prefix_sum = ff_r_recode_count_prefix_sum + ff_a_recode_count_prefix_sum)))))) /\ (forall ff_i_recode_count_prefix_bits. (exists ff_lt_recode_count_prefix_bits_bound. ff_lt_recode_count_prefix_bits_bound + S ff_i_recode_count_prefix_bits = l) -> exists ff_bit_recode_count_prefix_bits. ((((exists ff_h_recode_count_prefix_bits_decoded. ff_h_recode_count_prefix_bits_decoded + S (ff_bit_recode_count_prefix_bits) = S ((S (ff_i_recode_count_prefix_bits)) * sc)) /\ exists ff_q_recode_count_prefix_bits_decoded. sb = ff_q_recode_count_prefix_bits_decoded * S ((S (ff_i_recode_count_prefix_bits)) * sc) + (ff_bit_recode_count_prefix_bits))) /\ (ff_bit_recode_count_prefix_bits = 0 \/ ff_bit_recode_count_prefix_bits = 1))))) /\ ((a = 0 \/ a = 1) /\ e = k + a))
  26. 0026specialize bit_count_succ_decompose sb
  27. 0027specialize bit_count_succ_decompose sc
  28. 0028specialize bit_count_succ_decompose l
  29. 0029specialize bit_count_succ_decompose (S l)
  30. 0030specialize bit_count_succ_decompose e
  31. 0031apply bit_count_succ_decompose
  32. 0032refl
  33. 0033exact hcount
  34. 0034cases hdecomp
  35. 0035cases hdecomp_witness
  36. 0036cases hdecomp_witness_witness
  37. 0037cases hdecomp_witness_witness_right
  38. 0038cases hdecomp_witness_witness_right_right
  39. 0039have hprevious : exists fb fc. (forall gspf_index_recode_previous gspf_bit_recode_previous. (exists gsp_lt_gap_recode_previous_bound. gsp_lt_gap_recode_previous_bound + S gspf_index_recode_previous = l) -> (((exists ff_h_gspf_recode_previous_bit. ff_h_gspf_recode_previous_bit + S (gspf_bit_recode_previous) = S ((S (gspf_index_recode_previous)) * sc)) /\ exists ff_q_gspf_recode_previous_bit. sb = ff_q_gspf_recode_previous_bit * S ((S (gspf_index_recode_previous)) * sc) + (gspf_bit_recode_previous))) -> (((gspf_bit_recode_previous = 0) /\ (((exists gsp_beta_height_gspf_recode_previous_one. gsp_beta_height_gspf_recode_previous_one + S (1) = S ((S (gspf_index_recode_previous)) * fc)) /\ exists gsp_beta_quotient_gspf_recode_previous_one. fb = gsp_beta_quotient_gspf_recode_previous_one * S ((S (gspf_index_recode_previous)) * fc) + (1)))) \/ ((gspf_bit_recode_previous = 1) /\ (((exists ff_h_gspf_recode_previous_predecessor. ff_h_gspf_recode_previous_predecessor + S (r) = S ((S (gspf_index_recode_previous)) * fc)) /\ exists ff_q_gspf_recode_previous_predecessor. fb = ff_q_gspf_recode_previous_predecessor * S ((S (gspf_index_recode_previous)) * fc) + (r))))))
  40. 0040specialize IH x1
  41. 0041apply IH
  42. 0042exact hdecomp_witness_witness_right_left
  43. 0043cases hprevious
  44. 0044cases hprevious_witness
  45. 0045cases hdecomp_witness_witness_right_right_left
  46. 0046specialize beta_sign_factor_prefix_extend sb
  47. 0047specialize beta_sign_factor_prefix_extend sc
  48. 0048specialize beta_sign_factor_prefix_extend x2
  49. 0049specialize beta_sign_factor_prefix_extend x3
  50. 0050specialize beta_sign_factor_prefix_extend r
  51. 0051specialize beta_sign_factor_prefix_extend l
  52. 0052specialize beta_sign_factor_prefix_extend x
  53. 0053specialize beta_sign_factor_prefix_extend 1
  54. 0054apply beta_sign_factor_prefix_extend
  55. 0055exact hprevious_witness_witness
  56. 0056exact hdecomp_witness_witness_left
  57. 0057left
  58. 0058split
  59. 0059exact hdecomp_witness_witness_right_right_left_left
  60. 0060refl
  61. 0061specialize beta_sign_factor_prefix_extend sb
  62. 0062specialize beta_sign_factor_prefix_extend sc
  63. 0063specialize beta_sign_factor_prefix_extend x2
  64. 0064specialize beta_sign_factor_prefix_extend x3
  65. 0065specialize beta_sign_factor_prefix_extend r
  66. 0066specialize beta_sign_factor_prefix_extend l
  67. 0067specialize beta_sign_factor_prefix_extend x
  68. 0068specialize beta_sign_factor_prefix_extend r
  69. 0069apply beta_sign_factor_prefix_extend
  70. 0070exact hprevious_witness_witness
  71. 0071exact hdecomp_witness_witness_left
  72. 0072right
  73. 0073split
  74. 0074exact hdecomp_witness_witness_right_right_left_right
  75. 0075refl