PA009X

scaled_pair_order_successor_lift_adjacent_targets

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

A successor-lifted terminal scaled-orbit history has adjacent products congruent to a.

Exact expanded PA statement

forall p a n u v b c f g h. n = h + h -> (forall esip_index_enr_prefix. (exists esip_gap_enr_prefix_prefix_bound. esip_gap_enr_prefix_prefix_bound + S (esip_index_enr_prefix) = n) -> exists esip_mate_enr_prefix. ((((exists ff_h_esip_enr_prefix_entry. ff_h_esip_enr_prefix_entry + S (esip_mate_enr_prefix) = S ((S (esip_index_enr_prefix)) * v)) /\ exists ff_q_esip_enr_prefix_entry. u = ff_q_esip_enr_prefix_entry * S ((S (esip_index_enr_prefix)) * v) + (esip_mate_enr_prefix))) /\ ((exists esip_gap_enr_prefix_relation_index_bound. esip_gap_enr_prefix_relation_index_bound + S (esip_index_enr_prefix) = n) /\ ((((~((S esip_index_enr_prefix) = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_left_bound. esip_gap_enr_prefix_relation_scaled_left_bound + S (S esip_index_enr_prefix) = p))) /\ (((~(esip_mate_enr_prefix = 0) /\ (exists esip_gap_enr_prefix_relation_scaled_right_bound. esip_gap_enr_prefix_relation_scaled_right_bound + S (esip_mate_enr_prefix) = p))) /\ (exists esi_mod_left_enr_prefix_relation_scaled_mod esi_mod_right_enr_prefix_relation_scaled_mod. ((S esip_index_enr_prefix) * esip_mate_enr_prefix) + p * esi_mod_left_enr_prefix_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_relation_scaled_mod))))))) -> (forall fom_index_enr_raw_bounded. (exists fom_gap_enr_raw_bounded_index_bound. fom_gap_enr_raw_bounded_index_bound + S (fom_index_enr_raw_bounded) = h + h) -> exists fom_value_enr_raw_bounded. ((((exists fom_beta_height_enr_raw_bounded_entry. fom_beta_height_enr_raw_bounded_entry + S (fom_value_enr_raw_bounded) = S ((S (fom_index_enr_raw_bounded)) * c)) /\ exists fom_beta_quotient_enr_raw_bounded_entry. b = fom_beta_quotient_enr_raw_bounded_entry * S ((S (fom_index_enr_raw_bounded)) * c) + (fom_value_enr_raw_bounded))) /\ (exists fom_gap_enr_raw_bounded_value_bound. fom_gap_enr_raw_bounded_value_bound + S (fom_value_enr_raw_bounded) = n))) -> (forall espi_pair_enr_history. (exists wpo_gap_enr_history_pair_bound. wpo_gap_enr_history_pair_bound + S (espi_pair_enr_history) = h) -> exists espi_left_enr_history espi_right_enr_history. (((((exists wpo_beta_height_enr_history_left_entry. wpo_beta_height_enr_history_left_entry + S (espi_left_enr_history) = S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c)) /\ exists wpo_beta_quotient_enr_history_left_entry. b = wpo_beta_quotient_enr_history_left_entry * S ((S (espi_pair_enr_history + espi_pair_enr_history)) * c) + (espi_left_enr_history))) /\ (((((exists wpo_beta_height_enr_history_right_entry. wpo_beta_height_enr_history_right_entry + S (espi_right_enr_history) = S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c)) /\ exists wpo_beta_quotient_enr_history_right_entry. b = wpo_beta_quotient_enr_history_right_entry * S ((S (S (espi_pair_enr_history + espi_pair_enr_history))) * c) + (espi_right_enr_history))) /\ (((exists wpo_beta_height_enr_history_scaled_edge. wpo_beta_height_enr_history_scaled_edge + S (S espi_right_enr_history) = S ((S (espi_left_enr_history)) * v)) /\ exists wpo_beta_quotient_enr_history_scaled_edge. u = wpo_beta_quotient_enr_history_scaled_edge * S ((S (espi_left_enr_history)) * v) + (S espi_right_enr_history)))))))) -> (forall wsl_index_enr_lift_n wsl_value_enr_lift_n. (exists wpo_gap_enr_lift_n_bound. wpo_gap_enr_lift_n_bound + S (wsl_index_enr_lift_n) = n) -> (((exists wpo_beta_height_enr_lift_n_source. wpo_beta_height_enr_lift_n_source + S (wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * c)) /\ exists wpo_beta_quotient_enr_lift_n_source. b = wpo_beta_quotient_enr_lift_n_source * S ((S (wsl_index_enr_lift_n)) * c) + (wsl_value_enr_lift_n))) -> (((exists wpo_beta_height_enr_lift_n_target. wpo_beta_height_enr_lift_n_target + S (S wsl_value_enr_lift_n) = S ((S (wsl_index_enr_lift_n)) * g)) /\ exists wpo_beta_quotient_enr_lift_n_target. f = wpo_beta_quotient_enr_lift_n_target * S ((S (wsl_index_enr_lift_n)) * g) + (S wsl_value_enr_lift_n)))) -> (forall wpp_pair_enr_target_pairs wpp_left_enr_target_pairs wpp_right_enr_target_pairs. (exists wpp_gap_enr_target_pairs_pair_bound. wpp_gap_enr_target_pairs_pair_bound + S (wpp_pair_enr_target_pairs) = h) -> (((exists wpp_beta_height_enr_target_pairs_left_entry. wpp_beta_height_enr_target_pairs_left_entry + S (wpp_left_enr_target_pairs) = S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_left_entry. f = wpp_beta_quotient_enr_target_pairs_left_entry * S ((S ((wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_left_enr_target_pairs))) -> (((exists wpp_beta_height_enr_target_pairs_right_entry. wpp_beta_height_enr_target_pairs_right_entry + S (wpp_right_enr_target_pairs) = S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g)) /\ exists wpp_beta_quotient_enr_target_pairs_right_entry. f = wpp_beta_quotient_enr_target_pairs_right_entry * S ((S (S (wpp_pair_enr_target_pairs + wpp_pair_enr_target_pairs))) * g) + (wpp_right_enr_target_pairs))) -> (exists wpp_mod_left_enr_target_pairs_pair_mod wpp_mod_right_enr_target_pairs_pair_mod. (wpp_left_enr_target_pairs * wpp_right_enr_target_pairs) + p * wpp_mod_left_enr_target_pairs_pair_mod = (a) + p * wpp_mod_right_enr_target_pairs_pair_mod))

Structural proof guide

Generated structural guide

A successor-lifted terminal scaled-orbit history has adjacent products congruent to a.

Use the direct prerequisites pair_index_left_below_double, pair_index_right_below_double, beta_at_unique as previously established PA formulas.

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

Referenced ingredients

PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA002F beta_at_unique

Proof neighborhood

Direct dependencies

PA009Q pair_index_left_below_double PA009R pair_index_right_below_double PA002F beta_at_unique

Direct dependents

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 p
  2. 0002intro a
  3. 0003intro n
  4. 0004intro u
  5. 0005intro v
  6. 0006intro b
  7. 0007intro c
  8. 0008intro f
  9. 0009intro g
  10. 0010intro h
  11. 0011intro heven
  12. 0012intro hprefix
  13. 0013intro hbounded
  14. 0014intro hhistory
  15. 0015intro hlift
  16. 0016intro t
  17. 0017intro left
  18. 0018intro right
  19. 0019intro ht
  20. 0020intro hleft
  21. 0021intro hright
  22. 0022have horbit : exists i j. (((exists ff_h_enr_history_left. ff_h_enr_history_left + S (i) = S ((S (t + t)) * c)) /\ exists ff_q_enr_history_left. b = ff_q_enr_history_left * S ((S (t + t)) * c) + (i))) /\ ((((exists ff_h_enr_history_right. ff_h_enr_history_right + S (j) = S ((S (S (t + t))) * c)) /\ exists ff_q_enr_history_right. b = ff_q_enr_history_right * S ((S (S (t + t))) * c) + (j))) /\ (((exists ff_h_enr_history_scaled. ff_h_enr_history_scaled + S (S j) = S ((S (i)) * v)) /\ exists ff_q_enr_history_scaled. u = ff_q_enr_history_scaled * S ((S (i)) * v) + (S j))))
  23. 0023specialize hhistory t
  24. 0024apply hhistory
  25. 0025exact ht
  26. 0026cases horbit
  27. 0027cases horbit_witness
  28. 0028cases horbit_witness_witness
  29. 0029cases horbit_witness_witness_right
  30. 0030have heven_raw : exists wpo_gap_enr_even_bound_raw. wpo_gap_enr_even_bound_raw + S (t + t) = h + h
  31. 0031specialize pair_index_left_below_double t
  32. 0032specialize pair_index_left_below_double h
  33. 0033apply pair_index_left_below_double
  34. 0034exact ht
  35. 0035have hodd_raw : exists wpo_gap_enr_odd_bound_raw. wpo_gap_enr_odd_bound_raw + S (S (t + t)) = h + h
  36. 0036specialize pair_index_right_below_double t
  37. 0037specialize pair_index_right_below_double h
  38. 0038apply pair_index_right_below_double
  39. 0039exact ht
  40. 0040have heven_n : exists wpo_gap_enr_even_bound_n. wpo_gap_enr_even_bound_n + S (t + t) = n
  41. 0041rewrite heven
  42. 0042exact heven_raw
  43. 0043have hodd_n : exists wpo_gap_enr_odd_bound_n. wpo_gap_enr_odd_bound_n + S (S (t + t)) = n
  44. 0044rewrite heven
  45. 0045exact hodd_raw
  46. 0046have hlift_left : ((exists ff_h_enr_lifted_left. ff_h_enr_lifted_left + S (S x) = S ((S (t + t)) * g)) /\ exists ff_q_enr_lifted_left. f = ff_q_enr_lifted_left * S ((S (t + t)) * g) + (S x))
  47. 0047specialize hlift (t + t)
  48. 0048specialize hlift x
  49. 0049apply hlift
  50. 0050exact heven_n
  51. 0051exact horbit_witness_witness_left
  52. 0052have hlift_right : ((exists ff_h_enr_lifted_right. ff_h_enr_lifted_right + S (S x1) = S ((S (S (t + t))) * g)) /\ exists ff_q_enr_lifted_right. f = ff_q_enr_lifted_right * S ((S (S (t + t))) * g) + (S x1))
  53. 0053specialize hlift (S (t + t))
  54. 0054specialize hlift x1
  55. 0055apply hlift
  56. 0056exact hodd_n
  57. 0057exact horbit_witness_witness_right_left
  58. 0058have hleft_eq : left = S x
  59. 0059specialize beta_at_unique f
  60. 0060specialize beta_at_unique g
  61. 0061specialize beta_at_unique (t + t)
  62. 0062specialize beta_at_unique left
  63. 0063specialize beta_at_unique (S x)
  64. 0064apply beta_at_unique
  65. 0065exact hleft
  66. 0066exact hlift_left
  67. 0067have hright_eq : right = S x1
  68. 0068specialize beta_at_unique f
  69. 0069specialize beta_at_unique g
  70. 0070specialize beta_at_unique (S (t + t))
  71. 0071specialize beta_at_unique right
  72. 0072specialize beta_at_unique (S x1)
  73. 0073apply beta_at_unique
  74. 0074exact hright
  75. 0075exact hlift_right
  76. 0076have hbounded_even : exists w. (((exists ff_h_enr_bounded_even_entry. ff_h_enr_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists ff_q_enr_bounded_even_entry. b = ff_q_enr_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_enr_bounded_even_value. wpo_gap_enr_bounded_even_value + S (w) = n)
  77. 0077specialize hbounded (t + t)
  78. 0078apply hbounded
  79. 0079exact heven_raw
  80. 0080cases hbounded_even
  81. 0081cases hbounded_even_witness
  82. 0082have hsource_eq : x = x2
  83. 0083specialize beta_at_unique b
  84. 0084specialize beta_at_unique c
  85. 0085specialize beta_at_unique (t + t)
  86. 0086specialize beta_at_unique x
  87. 0087specialize beta_at_unique x2
  88. 0088apply beta_at_unique
  89. 0089exact horbit_witness_witness_left
  90. 0090exact hbounded_even_witness_left
  91. 0091have hsource_bound : exists gap. gap + S x = n
  92. 0092rewrite hsource_eq
  93. 0093exact hbounded_even_witness_right
  94. 0094have hprefix_data : exists y. (((exists ff_h_enr_prefix_at_x_entry. ff_h_enr_prefix_at_x_entry + S (y) = S ((S (x)) * v)) /\ exists ff_q_enr_prefix_at_x_entry. u = ff_q_enr_prefix_at_x_entry * S ((S (x)) * v) + (y))) /\ ((exists esip_gap_enr_prefix_at_x_relation_index_bound. esip_gap_enr_prefix_at_x_relation_index_bound + S (x) = n) /\ ((((~((S x) = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_left_bound. esip_gap_enr_prefix_at_x_relation_scaled_left_bound + S (S x) = p))) /\ (((~(y = 0) /\ (exists esip_gap_enr_prefix_at_x_relation_scaled_right_bound. esip_gap_enr_prefix_at_x_relation_scaled_right_bound + S (y) = p))) /\ (exists esi_mod_left_enr_prefix_at_x_relation_scaled_mod esi_mod_right_enr_prefix_at_x_relation_scaled_mod. ((S x) * y) + p * esi_mod_left_enr_prefix_at_x_relation_scaled_mod = (a) + p * esi_mod_right_enr_prefix_at_x_relation_scaled_mod)))))
  95. 0095specialize hprefix x
  96. 0096apply hprefix
  97. 0097exact hsource_bound
  98. 0098cases hprefix_data
  99. 0099cases hprefix_data_witness
  100. 0100cases hprefix_data_witness_right
  101. 0101cases hprefix_data_witness_right_right
  102. 0102cases hprefix_data_witness_right_right_right
  103. 0103have hmate_eq : x3 = S x1
  104. 0104specialize beta_at_unique u
  105. 0105specialize beta_at_unique v
  106. 0106specialize beta_at_unique x
  107. 0107specialize beta_at_unique x3
  108. 0108specialize beta_at_unique (S x1)
  109. 0109apply beta_at_unique
  110. 0110exact hprefix_data_witness_left
  111. 0111exact horbit_witness_witness_right_right
  112. 0112rewrite hleft_eq
  113. 0113rewrite hright_eq
  114. 0114rewrite <- hmate_eq
  115. 0115exact hprefix_data_witness_right_right_right_right