PA008S

prime_scaled_inverse_prefix_exists_bounded

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

Every bounded predecessor length has a beta-coded scaled-inverse prefix.

Exact expanded PA statement

forall p a n l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_esip_bounded_prime esi_prime_right_esip_bounded_prime. p = esi_prime_left_esip_bounded_prime * esi_prime_right_esip_bounded_prime -> esi_prime_left_esip_bounded_prime = 1 \/ esi_prime_right_esip_bounded_prime = 1)) -> ~(a = 0) -> (exists esip_gap_bounded_target_bound. esip_gap_bounded_target_bound + S (a) = p) -> (exists esip_weak_gap_bounded. esip_weak_gap_bounded + l = n) -> exists b c. (forall esip_index_bounded_result. (exists esip_gap_bounded_result_prefix_bound. esip_gap_bounded_result_prefix_bound + S (esip_index_bounded_result) = l) -> exists esip_mate_bounded_result. ((((exists ff_h_esip_bounded_result_entry. ff_h_esip_bounded_result_entry + S (esip_mate_bounded_result) = S ((S (esip_index_bounded_result)) * c)) /\ exists ff_q_esip_bounded_result_entry. b = ff_q_esip_bounded_result_entry * S ((S (esip_index_bounded_result)) * c) + (esip_mate_bounded_result))) /\ ((exists esip_gap_bounded_result_relation_index_bound. esip_gap_bounded_result_relation_index_bound + S (esip_index_bounded_result) = n) /\ ((((~((S esip_index_bounded_result) = 0) /\ (exists esip_gap_bounded_result_relation_scaled_left_bound. esip_gap_bounded_result_relation_scaled_left_bound + S (S esip_index_bounded_result) = p))) /\ (((~(esip_mate_bounded_result = 0) /\ (exists esip_gap_bounded_result_relation_scaled_right_bound. esip_gap_bounded_result_relation_scaled_right_bound + S (esip_mate_bounded_result) = p))) /\ (exists esi_mod_left_bounded_result_relation_scaled_mod esi_mod_right_bounded_result_relation_scaled_mod. ((S esip_index_bounded_result) * esip_mate_bounded_result) + p * esi_mod_left_bounded_result_relation_scaled_mod = (a) + p * esi_mod_right_bounded_result_relation_scaled_mod)))))))

Structural proof guide

Generated structural guide

Every bounded predecessor length has a beta-coded scaled-inverse prefix.

Use the direct prerequisites add_eq_zero_right, succ_ne_zero, lt_to_le, prime_scaled_inverse_prefix_extend as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (5), intermediate claims (4).

Referenced ingredients

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA008R prime_scaled_inverse_prefix_extend

Proof neighborhood

Direct dependencies

PA0004 add_eq_zero_right PA0005 succ_ne_zero PA000X lt_to_le PA008R prime_scaled_inverse_prefix_extend

Direct dependents

PA008T prime_scaled_inverse_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 p
  2. 0002intro a
  3. 0003intro n
  4. 0004induction l
  5. 0005intro hpn
  6. 0006intro hp
  7. 0007intro ha0
  8. 0008intro hap
  9. 0009intro hln
  10. 0010exists 0
  11. 0011exists 0
  12. 0012intro i
  13. 0013intro hi
  14. 0014exfalso
  15. 0015cases hi
  16. 0016have hsi : S i = 0
  17. 0017specialize add_eq_zero_right x
  18. 0018specialize add_eq_zero_right (S i)
  19. 0019apply add_eq_zero_right
  20. 0020exact hi_witness
  21. 0021specialize succ_ne_zero i
  22. 0022apply succ_ne_zero
  23. 0023exact hsi
  24. 0024intro hpn
  25. 0025intro hp
  26. 0026intro ha0
  27. 0027intro hap
  28. 0028intro hln
  29. 0029have hprev_bound : exists h. h + l = n
  30. 0030specialize lt_to_le l
  31. 0031specialize lt_to_le n
  32. 0032apply lt_to_le
  33. 0033exact hln
  34. 0034have hprev : exists b c. (forall esip_index_bounded_previous. (exists esip_gap_bounded_previous_prefix_bound. esip_gap_bounded_previous_prefix_bound + S (esip_index_bounded_previous) = l) -> exists esip_mate_bounded_previous. ((((exists ff_h_esip_bounded_previous_entry. ff_h_esip_bounded_previous_entry + S (esip_mate_bounded_previous) = S ((S (esip_index_bounded_previous)) * c)) /\ exists ff_q_esip_bounded_previous_entry. b = ff_q_esip_bounded_previous_entry * S ((S (esip_index_bounded_previous)) * c) + (esip_mate_bounded_previous))) /\ ((exists esip_gap_bounded_previous_relation_index_bound. esip_gap_bounded_previous_relation_index_bound + S (esip_index_bounded_previous) = n) /\ ((((~((S esip_index_bounded_previous) = 0) /\ (exists esip_gap_bounded_previous_relation_scaled_left_bound. esip_gap_bounded_previous_relation_scaled_left_bound + S (S esip_index_bounded_previous) = p))) /\ (((~(esip_mate_bounded_previous = 0) /\ (exists esip_gap_bounded_previous_relation_scaled_right_bound. esip_gap_bounded_previous_relation_scaled_right_bound + S (esip_mate_bounded_previous) = p))) /\ (exists esi_mod_left_bounded_previous_relation_scaled_mod esi_mod_right_bounded_previous_relation_scaled_mod. ((S esip_index_bounded_previous) * esip_mate_bounded_previous) + p * esi_mod_left_bounded_previous_relation_scaled_mod = (a) + p * esi_mod_right_bounded_previous_relation_scaled_mod)))))))
  35. 0035apply IH
  36. 0036exact hpn
  37. 0037exact hp
  38. 0038exact ha0
  39. 0039exact hap
  40. 0040exact hprev_bound
  41. 0041cases hprev
  42. 0042cases hprev_witness
  43. 0043have hnext : exists z d. (forall esip_index_bounded_successor. (exists esip_gap_bounded_successor_prefix_bound. esip_gap_bounded_successor_prefix_bound + S (esip_index_bounded_successor) = S l) -> exists esip_mate_bounded_successor. ((((exists ff_h_esip_bounded_successor_entry. ff_h_esip_bounded_successor_entry + S (esip_mate_bounded_successor) = S ((S (esip_index_bounded_successor)) * d)) /\ exists ff_q_esip_bounded_successor_entry. z = ff_q_esip_bounded_successor_entry * S ((S (esip_index_bounded_successor)) * d) + (esip_mate_bounded_successor))) /\ ((exists esip_gap_bounded_successor_relation_index_bound. esip_gap_bounded_successor_relation_index_bound + S (esip_index_bounded_successor) = n) /\ ((((~((S esip_index_bounded_successor) = 0) /\ (exists esip_gap_bounded_successor_relation_scaled_left_bound. esip_gap_bounded_successor_relation_scaled_left_bound + S (S esip_index_bounded_successor) = p))) /\ (((~(esip_mate_bounded_successor = 0) /\ (exists esip_gap_bounded_successor_relation_scaled_right_bound. esip_gap_bounded_successor_relation_scaled_right_bound + S (esip_mate_bounded_successor) = p))) /\ (exists esi_mod_left_bounded_successor_relation_scaled_mod esi_mod_right_bounded_successor_relation_scaled_mod. ((S esip_index_bounded_successor) * esip_mate_bounded_successor) + p * esi_mod_left_bounded_successor_relation_scaled_mod = (a) + p * esi_mod_right_bounded_successor_relation_scaled_mod)))))))
  44. 0044specialize prime_scaled_inverse_prefix_extend p
  45. 0045specialize prime_scaled_inverse_prefix_extend a
  46. 0046specialize prime_scaled_inverse_prefix_extend n
  47. 0047specialize prime_scaled_inverse_prefix_extend x
  48. 0048specialize prime_scaled_inverse_prefix_extend x1
  49. 0049specialize prime_scaled_inverse_prefix_extend l
  50. 0050specialize prime_scaled_inverse_prefix_extend (S l)
  51. 0051apply prime_scaled_inverse_prefix_extend
  52. 0052exact hpn
  53. 0053exact hp
  54. 0054exact ha0
  55. 0055exact hap
  56. 0056exact hln
  57. 0057refl
  58. 0058exact hprev_witness_witness
  59. 0059cases hnext
  60. 0060cases hnext_witness
  61. 0061exists x2
  62. 0062exists x3
  63. 0063exact hnext_witness_witness