PA008C

beta_successor_lift_exists

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

Every decoded finite prefix can be recoded after successor-lifting its values.

Exact expanded PA statement

forall r s l. exists z d. forall i j. (exists frm_gap_successor_lift_bound. frm_gap_successor_lift_bound + S i = l) -> (((exists ff_h_frm_successor_lift_source. ff_h_frm_successor_lift_source + S (j) = S ((S (i)) * s)) /\ exists ff_q_frm_successor_lift_source. r = ff_q_frm_successor_lift_source * S ((S (i)) * s) + (j))) -> (((exists frm_height_successor_lift_target. frm_height_successor_lift_target + S (S j) = S ((S (i)) * d)) /\ exists frm_quotient_successor_lift_target. z = frm_quotient_successor_lift_target * S ((S (i)) * d) + (S j)))

Structural proof guide

Generated structural guide

Every decoded finite prefix can be recoded after successor-lifting its values.

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

The proof proceeds by structural induction (1), case analysis (8), intermediate claims (3), equality transport (6).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA002X beta_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA003D finite_lt_succ_eq_or_lt PA0029 beta_at_exists PA002F beta_at_unique PA002X beta_prefix_extend

Direct dependents

PA008I prime_mul_residue_reindex_exists PA00B6 pair_order_successor_lift_exists PA00BK scaled_pair_order_terminal_power_mod_predecessor

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 r
  2. 0002intro s
  3. 0003induction l
  4. 0004exists 0
  5. 0005exists 0
  6. 0006intro i
  7. 0007intro j
  8. 0008intro hi
  9. 0009intro hsource
  10. 0010exfalso
  11. 0011cases hi
  12. 0012have hsi : S i = 0
  13. 0013specialize add_eq_zero_right x
  14. 0014specialize add_eq_zero_right (S i)
  15. 0015apply add_eq_zero_right
  16. 0016exact hi_witness
  17. 0017specialize succ_ne_zero i
  18. 0018apply succ_ne_zero
  19. 0019exact hsi
  20. 0020cases IH
  21. 0021cases IH_witness
  22. 0022specialize beta_at_exists r
  23. 0023specialize beta_at_exists s
  24. 0024specialize beta_at_exists l
  25. 0025cases beta_at_exists
  26. 0026specialize beta_prefix_extend l
  27. 0027specialize beta_prefix_extend x
  28. 0028specialize beta_prefix_extend x1
  29. 0029specialize beta_prefix_extend (S x2)
  30. 0030cases beta_prefix_extend
  31. 0031cases beta_prefix_extend_witness
  32. 0032cases beta_prefix_extend_witness_witness
  33. 0033exists x3
  34. 0034exists x4
  35. 0035intro i
  36. 0036intro j
  37. 0037intro hi
  38. 0038intro hsource
  39. 0039have hsplit : i = l \/ exists h. h + S i = l
  40. 0040specialize finite_lt_succ_eq_or_lt l
  41. 0041specialize finite_lt_succ_eq_or_lt i
  42. 0042apply finite_lt_succ_eq_or_lt
  43. 0043exact hi
  44. 0044cases hsplit
  45. 0045have hjx : j = x2
  46. 0046specialize beta_at_unique r
  47. 0047specialize beta_at_unique s
  48. 0048specialize beta_at_unique l
  49. 0049specialize beta_at_unique j
  50. 0050specialize beta_at_unique x2
  51. 0051apply beta_at_unique
  52. 0052rewrite hsplit_left at hsource
  53. 0053rewrite hsplit_left at hsource
  54. 0054exact hsource
  55. 0055exact beta_at_exists_witness
  56. 0056rewrite hsplit_left
  57. 0057rewrite hsplit_left
  58. 0058rewrite hjx
  59. 0059rewrite hjx
  60. 0060exact beta_prefix_extend_witness_witness_left
  61. 0061specialize beta_prefix_extend_witness_witness_right i
  62. 0062specialize beta_prefix_extend_witness_witness_right (S j)
  63. 0063apply beta_prefix_extend_witness_witness_right
  64. 0064exact hsplit_right
  65. 0065specialize IH_witness_witness i
  66. 0066specialize IH_witness_witness j
  67. 0067apply IH_witness_witness
  68. 0068exact hsplit_right
  69. 0069exact hsource