PA009I

scaled_inverse_prefix_choose_omitted_orbit

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

Choose an omitted source, decode its actual mate S j, and expose a distinct involutive pair.

Exact expanded PA statement

forall p a n u v b c l. p = S n -> ((~(p = 1) /\ forall esi_prime_left_espo_choose_prime esi_prime_right_espo_choose_prime. p = esi_prime_left_espo_choose_prime * esi_prime_right_espo_choose_prime -> esi_prime_left_espo_choose_prime = 1 \/ esi_prime_right_espo_choose_prime = 1)) -> ~(exists qr_x_espo_choose_nonresidue. exists qr_u_espo_choose_nonresidue qr_v_espo_choose_nonresidue. qr_x_espo_choose_nonresidue * qr_x_espo_choose_nonresidue + p * qr_u_espo_choose_nonresidue = a + p * qr_v_espo_choose_nonresidue) -> (forall esip_index_espo_choose_prefix. (exists esip_gap_espo_choose_prefix_prefix_bound. esip_gap_espo_choose_prefix_prefix_bound + S (esip_index_espo_choose_prefix) = n) -> exists esip_mate_espo_choose_prefix. ((((exists ff_h_esip_espo_choose_prefix_entry. ff_h_esip_espo_choose_prefix_entry + S (esip_mate_espo_choose_prefix) = S ((S (esip_index_espo_choose_prefix)) * v)) /\ exists ff_q_esip_espo_choose_prefix_entry. u = ff_q_esip_espo_choose_prefix_entry * S ((S (esip_index_espo_choose_prefix)) * v) + (esip_mate_espo_choose_prefix))) /\ ((exists esip_gap_espo_choose_prefix_relation_index_bound. esip_gap_espo_choose_prefix_relation_index_bound + S (esip_index_espo_choose_prefix) = n) /\ ((((~((S esip_index_espo_choose_prefix) = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_left_bound. esip_gap_espo_choose_prefix_relation_scaled_left_bound + S (S esip_index_espo_choose_prefix) = p))) /\ (((~(esip_mate_espo_choose_prefix = 0) /\ (exists esip_gap_espo_choose_prefix_relation_scaled_right_bound. esip_gap_espo_choose_prefix_relation_scaled_right_bound + S (esip_mate_espo_choose_prefix) = p))) /\ (exists esi_mod_left_espo_choose_prefix_relation_scaled_mod esi_mod_right_espo_choose_prefix_relation_scaled_mod. ((S esip_index_espo_choose_prefix) * esip_mate_espo_choose_prefix) + p * esi_mod_left_espo_choose_prefix_relation_scaled_mod = (a) + p * esi_mod_right_espo_choose_prefix_relation_scaled_mod))))))) -> (exists wpo_gap_choose_short. wpo_gap_choose_short + S (l) = n) -> (exists i j. ((exists wpo_gap_chosen_i_bound. wpo_gap_chosen_i_bound + S (i) = n) /\ (((~(exists wpo_index_chosen_i_omit_contains. ((exists wpo_gap_chosen_i_omit_contains_bound. wpo_gap_chosen_i_omit_contains_bound + S (wpo_index_chosen_i_omit_contains) = l) /\ (((exists wpo_beta_height_chosen_i_omit_contains_entry. wpo_beta_height_chosen_i_omit_contains_entry + S (i) = S ((S (wpo_index_chosen_i_omit_contains)) * c)) /\ exists wpo_beta_quotient_chosen_i_omit_contains_entry. b = wpo_beta_quotient_chosen_i_omit_contains_entry * S ((S (wpo_index_chosen_i_omit_contains)) * c) + (i)))))) /\ (((exists wpo_gap_chosen_j_bound. wpo_gap_chosen_j_bound + S (j) = n) /\ (((~(i = j)) /\ (((((exists wpo_beta_height_chosen_forward. wpo_beta_height_chosen_forward + S (S j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_chosen_forward. u = wpo_beta_quotient_chosen_forward * S ((S (i)) * v) + (S j))) /\ (((exists wpo_beta_height_chosen_back. wpo_beta_height_chosen_back + S (S i) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_back. u = wpo_beta_quotient_chosen_back * S ((S (j)) * v) + (S i)))))))))))))

Structural proof guide

Generated structural guide

Choose an omitted source, decode its actual mate S j, and expose a distinct involutive pair.

Use the direct prerequisites finite_short_prefix_omits, scaled_inverse_prefix_involutive, scaled_inverse_prefix_no_fixed_of_not_qres as previously established PA formulas.

The proof proceeds by case analysis (7), intermediate claims (5), equality transport (4).

Referenced ingredients

PA0098 finite_short_prefix_omits PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres

Proof neighborhood

Direct dependencies

PA0098 finite_short_prefix_omits PA009E scaled_inverse_prefix_involutive PA009H scaled_inverse_prefix_no_fixed_of_not_qres

Direct dependents

PA009O scaled_inverse_pair_order_choose_append

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. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro l
  9. 0009intro hpn
  10. 0010intro hp
  11. 0011intro hnotqres
  12. 0012intro hprefix
  13. 0013intro hshort
  14. 0014have homitted : exists wpo_value_choose_omitted. ((exists wpo_gap_choose_omitted_value_bound. wpo_gap_choose_omitted_value_bound + S (wpo_value_choose_omitted) = n) /\ (~(exists wpo_index_choose_omitted_omitted_contains. ((exists wpo_gap_choose_omitted_omitted_contains_bound. wpo_gap_choose_omitted_omitted_contains_bound + S (wpo_index_choose_omitted_omitted_contains) = l) /\ (((exists wpo_beta_height_choose_omitted_omitted_contains_entry. wpo_beta_height_choose_omitted_omitted_contains_entry + S (wpo_value_choose_omitted) = S ((S (wpo_index_choose_omitted_omitted_contains)) * c)) /\ exists wpo_beta_quotient_choose_omitted_omitted_contains_entry. b = wpo_beta_quotient_choose_omitted_omitted_contains_entry * S ((S (wpo_index_choose_omitted_omitted_contains)) * c) + (wpo_value_choose_omitted)))))))
  15. 0015specialize finite_short_prefix_omits b
  16. 0016specialize finite_short_prefix_omits c
  17. 0017specialize finite_short_prefix_omits l
  18. 0018specialize finite_short_prefix_omits n
  19. 0019apply finite_short_prefix_omits
  20. 0020exact hshort
  21. 0021cases homitted
  22. 0022cases homitted_witness
  23. 0023have hstored : exists y. ((((exists wpo_beta_height_chosen_stored_x_entry. wpo_beta_height_chosen_stored_x_entry + S (y) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_chosen_stored_x_entry. u = wpo_beta_quotient_chosen_stored_x_entry * S ((S (x)) * v) + (y))) /\ ((exists esip_gap_chosen_stored_x_relation_index_bound. esip_gap_chosen_stored_x_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_chosen_stored_x_relation_scaled_left_bound. esip_gap_chosen_stored_x_relation_scaled_left_bound + S (S x) = p))) /\ (((~(y = 0) /\ (exists esip_gap_chosen_stored_x_relation_scaled_right_bound. esip_gap_chosen_stored_x_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_chosen_stored_x_relation_scaled_mod esi_mod_right_chosen_stored_x_relation_scaled_mod. ((S x) * y) + p * esi_mod_left_chosen_stored_x_relation_scaled_mod = (a) + p * esi_mod_right_chosen_stored_x_relation_scaled_mod))))))
  24. 0024specialize hprefix x
  25. 0025apply hprefix
  26. 0026exact homitted_witness_left
  27. 0027cases hstored
  28. 0028cases hstored_witness
  29. 0029have hinvolutive : exists j. ((x1 = S j) /\ (((exists wpo_gap_chosen_involutive_j_bound. wpo_gap_chosen_involutive_j_bound + S (j) = n) /\ (((exists wpo_beta_height_chosen_involutive_back. wpo_beta_height_chosen_involutive_back + S (S x) = S ((S (j)) * v)) /\ exists wpo_beta_quotient_chosen_involutive_back. u = wpo_beta_quotient_chosen_involutive_back * S ((S (j)) * v) + (S x))))))
  30. 0030specialize scaled_inverse_prefix_involutive p
  31. 0031specialize scaled_inverse_prefix_involutive a
  32. 0032specialize scaled_inverse_prefix_involutive n
  33. 0033specialize scaled_inverse_prefix_involutive u
  34. 0034specialize scaled_inverse_prefix_involutive v
  35. 0035specialize scaled_inverse_prefix_involutive x
  36. 0036specialize scaled_inverse_prefix_involutive x1
  37. 0037apply scaled_inverse_prefix_involutive
  38. 0038exact hpn
  39. 0039exact hp
  40. 0040exact hprefix
  41. 0041exact homitted_witness_left
  42. 0042exact hstored_witness_left
  43. 0043cases hinvolutive
  44. 0044cases hinvolutive_witness
  45. 0045cases hinvolutive_witness_right
  46. 0046have hforward : ((exists wpo_beta_height_chosen_forward_x2. wpo_beta_height_chosen_forward_x2 + S (S x2) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_chosen_forward_x2. u = wpo_beta_quotient_chosen_forward_x2 * S ((S (x)) * v) + (S x2))
  47. 0047rewrite <- hinvolutive_witness_left
  48. 0048rewrite <- hinvolutive_witness_left
  49. 0049exact hstored_witness_left
  50. 0050have hdistinct : ~(x = x2)
  51. 0051intro heq
  52. 0052rewrite <- heq at hforward
  53. 0053rewrite <- heq at hforward
  54. 0054specialize scaled_inverse_prefix_no_fixed_of_not_qres p
  55. 0055specialize scaled_inverse_prefix_no_fixed_of_not_qres a
  56. 0056specialize scaled_inverse_prefix_no_fixed_of_not_qres n
  57. 0057specialize scaled_inverse_prefix_no_fixed_of_not_qres u
  58. 0058specialize scaled_inverse_prefix_no_fixed_of_not_qres v
  59. 0059specialize scaled_inverse_prefix_no_fixed_of_not_qres n
  60. 0060specialize scaled_inverse_prefix_no_fixed_of_not_qres x
  61. 0061apply scaled_inverse_prefix_no_fixed_of_not_qres
  62. 0062exact hnotqres
  63. 0063exact hprefix
  64. 0064exact homitted_witness_left
  65. 0065exact hforward
  66. 0066exists x
  67. 0067exists x2
  68. 0068split
  69. 0069exact homitted_witness_left
  70. 0070split
  71. 0071exact homitted_witness_right
  72. 0072split
  73. 0073exact hinvolutive_witness_right_left
  74. 0074split
  75. 0075exact hdistinct
  76. 0076split
  77. 0077exact hforward
  78. 0078exact hinvolutive_witness_right_right