PA00B7

paired_successor_lift_adjacent_units

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

Successor-lifted adjacent inverse indices multiply to one modulo p.

Exact expanded PA statement

forall p n u v b c f g m. (forall wip_index_wsl_inverse. (exists wip_gap_wsl_inverse_prefix_bound. wip_gap_wsl_inverse_prefix_bound + S wip_index_wsl_inverse = n) -> exists wip_mate_wsl_inverse. ((((exists wip_beta_height_wsl_inverse_decoded. wip_beta_height_wsl_inverse_decoded + S (wip_mate_wsl_inverse) = S ((S (wip_index_wsl_inverse)) * v)) /\ exists wip_beta_quotient_wsl_inverse_decoded. u = wip_beta_quotient_wsl_inverse_decoded * S ((S (wip_index_wsl_inverse)) * v) + (wip_mate_wsl_inverse))) /\ ((exists wip_gap_wsl_inverse_inverse_index_bound. wip_gap_wsl_inverse_inverse_index_bound + S wip_index_wsl_inverse = n) /\ ((exists wip_gap_wsl_inverse_inverse_mate_bound. wip_gap_wsl_inverse_inverse_mate_bound + S wip_mate_wsl_inverse = n) /\ (exists wip_mod_left_wsl_inverse_inverse_mod wip_mod_right_wsl_inverse_inverse_mod. ((S wip_index_wsl_inverse) * S wip_mate_wsl_inverse) + p * wip_mod_left_wsl_inverse_inverse_mod = 1 + p * wip_mod_right_wsl_inverse_inverse_mod))))) -> (forall fom_index_wsl_bounded. (exists fom_gap_wsl_bounded_index_bound. fom_gap_wsl_bounded_index_bound + S (fom_index_wsl_bounded) = m + m) -> exists fom_value_wsl_bounded. ((((exists fom_beta_height_wsl_bounded_entry. fom_beta_height_wsl_bounded_entry + S (fom_value_wsl_bounded) = S ((S (fom_index_wsl_bounded)) * c)) /\ exists fom_beta_quotient_wsl_bounded_entry. b = fom_beta_quotient_wsl_bounded_entry * S ((S (fom_index_wsl_bounded)) * c) + (fom_value_wsl_bounded))) /\ (exists fom_gap_wsl_bounded_value_bound. fom_gap_wsl_bounded_value_bound + S (fom_value_wsl_bounded) = n))) -> (forall wpop_pair_wsl_pairs. (exists wpo_gap_wsl_pairs_pair_bound. wpo_gap_wsl_pairs_pair_bound + S (wpop_pair_wsl_pairs) = m) -> exists wpop_left_wsl_pairs wpop_right_wsl_pairs. ((((exists wpo_beta_height_wsl_pairs_left_entry. wpo_beta_height_wsl_pairs_left_entry + S (wpop_left_wsl_pairs) = S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c)) /\ exists wpo_beta_quotient_wsl_pairs_left_entry. b = wpo_beta_quotient_wsl_pairs_left_entry * S ((S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs)) * c) + (wpop_left_wsl_pairs))) /\ ((((exists wpo_beta_height_wsl_pairs_right_entry. wpo_beta_height_wsl_pairs_right_entry + S (wpop_right_wsl_pairs) = S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c)) /\ exists wpo_beta_quotient_wsl_pairs_right_entry. b = wpo_beta_quotient_wsl_pairs_right_entry * S ((S (S (wpop_pair_wsl_pairs + wpop_pair_wsl_pairs))) * c) + (wpop_right_wsl_pairs))) /\ (((exists wpo_beta_height_wsl_pairs_inverse_entry. wpo_beta_height_wsl_pairs_inverse_entry + S (wpop_right_wsl_pairs) = S ((S (wpop_left_wsl_pairs)) * v)) /\ exists wpo_beta_quotient_wsl_pairs_inverse_entry. u = wpo_beta_quotient_wsl_pairs_inverse_entry * S ((S (wpop_left_wsl_pairs)) * v) + (wpop_right_wsl_pairs)))))) -> (forall wsl_index_wsl_lift wsl_value_wsl_lift. (exists wpo_gap_wsl_lift_bound. wpo_gap_wsl_lift_bound + S (wsl_index_wsl_lift) = m + m) -> (((exists wpo_beta_height_wsl_lift_source. wpo_beta_height_wsl_lift_source + S (wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * c)) /\ exists wpo_beta_quotient_wsl_lift_source. b = wpo_beta_quotient_wsl_lift_source * S ((S (wsl_index_wsl_lift)) * c) + (wsl_value_wsl_lift))) -> (((exists wpo_beta_height_wsl_lift_target. wpo_beta_height_wsl_lift_target + S (S wsl_value_wsl_lift) = S ((S (wsl_index_wsl_lift)) * g)) /\ exists wpo_beta_quotient_wsl_lift_target. f = wpo_beta_quotient_wsl_lift_target * S ((S (wsl_index_wsl_lift)) * g) + (S wsl_value_wsl_lift)))) -> (forall wpp_pair_wsl_adjacent wpp_left_wsl_adjacent wpp_right_wsl_adjacent. (exists wpp_gap_wsl_adjacent_pair_bound. wpp_gap_wsl_adjacent_pair_bound + S (wpp_pair_wsl_adjacent) = m) -> (((exists wpp_beta_height_wsl_adjacent_left_entry. wpp_beta_height_wsl_adjacent_left_entry + S (wpp_left_wsl_adjacent) = S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_left_entry. f = wpp_beta_quotient_wsl_adjacent_left_entry * S ((S ((wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_left_wsl_adjacent))) -> (((exists wpp_beta_height_wsl_adjacent_right_entry. wpp_beta_height_wsl_adjacent_right_entry + S (wpp_right_wsl_adjacent) = S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g)) /\ exists wpp_beta_quotient_wsl_adjacent_right_entry. f = wpp_beta_quotient_wsl_adjacent_right_entry * S ((S (S (wpp_pair_wsl_adjacent + wpp_pair_wsl_adjacent))) * g) + (wpp_right_wsl_adjacent))) -> (exists wpp_mod_left_wsl_adjacent_pair_mod wpp_mod_right_wsl_adjacent_pair_mod. (wpp_left_wsl_adjacent * wpp_right_wsl_adjacent) + p * wpp_mod_left_wsl_adjacent_pair_mod = (1) + p * wpp_mod_right_wsl_adjacent_pair_mod))

Structural proof guide

Generated structural guide

Successor-lifted adjacent inverse indices multiply to one modulo p.

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 (10), intermediate claims (12), equality transport (4).

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

PA00B8 paired_pair_order_factor_code_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 n
  3. 0003intro u
  4. 0004intro v
  5. 0005intro b
  6. 0006intro c
  7. 0007intro f
  8. 0008intro g
  9. 0009intro m
  10. 0010intro hinverse
  11. 0011intro hbounded
  12. 0012intro hpairs
  13. 0013intro hlift
  14. 0014intro t
  15. 0015intro a
  16. 0016intro d
  17. 0017intro ht
  18. 0018intro ha
  19. 0019intro hd
  20. 0020have hpair : exists i j. ((((exists wpo_beta_height_wsl_order_even_i. wpo_beta_height_wsl_order_even_i + S (i) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_wsl_order_even_i. b = wpo_beta_quotient_wsl_order_even_i * S ((S (t + t)) * c) + (i))) /\ ((((exists wpo_beta_height_wsl_order_odd_j. wpo_beta_height_wsl_order_odd_j + S (j) = S ((S (S (t + t))) * c)) /\ exists wpo_beta_quotient_wsl_order_odd_j. b = wpo_beta_quotient_wsl_order_odd_j * S ((S (S (t + t))) * c) + (j))) /\ (((exists wpo_beta_height_wsl_inverse_i_j. wpo_beta_height_wsl_inverse_i_j + S (j) = S ((S (i)) * v)) /\ exists wpo_beta_quotient_wsl_inverse_i_j. u = wpo_beta_quotient_wsl_inverse_i_j * S ((S (i)) * v) + (j)))))
  21. 0021specialize hpairs t
  22. 0022apply hpairs
  23. 0023exact ht
  24. 0024cases hpair
  25. 0025cases hpair_witness
  26. 0026cases hpair_witness_witness
  27. 0027cases hpair_witness_witness_right
  28. 0028have heven : exists wpo_gap_wsl_even_bound. wpo_gap_wsl_even_bound + S (t + t) = m + m
  29. 0029specialize pair_index_left_below_double t
  30. 0030specialize pair_index_left_below_double m
  31. 0031apply pair_index_left_below_double
  32. 0032exact ht
  33. 0033have hodd : exists wpo_gap_wsl_odd_bound. wpo_gap_wsl_odd_bound + S (S (t + t)) = m + m
  34. 0034specialize pair_index_right_below_double t
  35. 0035specialize pair_index_right_below_double m
  36. 0036apply pair_index_right_below_double
  37. 0037exact ht
  38. 0038have hlift_left : ((exists wpo_beta_height_wsl_lifted_even_i. wpo_beta_height_wsl_lifted_even_i + S (S x) = S ((S (t + t)) * g)) /\ exists wpo_beta_quotient_wsl_lifted_even_i. f = wpo_beta_quotient_wsl_lifted_even_i * S ((S (t + t)) * g) + (S x))
  39. 0039specialize hlift (t + t)
  40. 0040specialize hlift x
  41. 0041apply hlift
  42. 0042exact heven
  43. 0043exact hpair_witness_witness_left
  44. 0044have hlift_right : ((exists wpo_beta_height_wsl_lifted_odd_j. wpo_beta_height_wsl_lifted_odd_j + S (S x1) = S ((S (S (t + t))) * g)) /\ exists wpo_beta_quotient_wsl_lifted_odd_j. f = wpo_beta_quotient_wsl_lifted_odd_j * S ((S (S (t + t))) * g) + (S x1))
  45. 0045specialize hlift (S (t + t))
  46. 0046specialize hlift x1
  47. 0047apply hlift
  48. 0048exact hodd
  49. 0049exact hpair_witness_witness_right_left
  50. 0050have haeq : a = S x
  51. 0051specialize beta_at_unique f
  52. 0052specialize beta_at_unique g
  53. 0053specialize beta_at_unique (t + t)
  54. 0054specialize beta_at_unique a
  55. 0055specialize beta_at_unique (S x)
  56. 0056apply beta_at_unique
  57. 0057exact ha
  58. 0058exact hlift_left
  59. 0059have hdeq : d = S x1
  60. 0060specialize beta_at_unique f
  61. 0061specialize beta_at_unique g
  62. 0062specialize beta_at_unique (S (t + t))
  63. 0063specialize beta_at_unique d
  64. 0064specialize beta_at_unique (S x1)
  65. 0065apply beta_at_unique
  66. 0066exact hd
  67. 0067exact hlift_right
  68. 0068have hbounded_data : exists w. ((((exists wpo_beta_height_wsl_bounded_even_entry. wpo_beta_height_wsl_bounded_even_entry + S (w) = S ((S (t + t)) * c)) /\ exists wpo_beta_quotient_wsl_bounded_even_entry. b = wpo_beta_quotient_wsl_bounded_even_entry * S ((S (t + t)) * c) + (w))) /\ (exists wpo_gap_wsl_bounded_even_value. wpo_gap_wsl_bounded_even_value + S (w) = n))
  69. 0069specialize hbounded (t + t)
  70. 0070apply hbounded
  71. 0071exact heven
  72. 0072cases hbounded_data
  73. 0073cases hbounded_data_witness
  74. 0074have hieq : x = x2
  75. 0075specialize beta_at_unique b
  76. 0076specialize beta_at_unique c
  77. 0077specialize beta_at_unique (t + t)
  78. 0078specialize beta_at_unique x
  79. 0079specialize beta_at_unique x2
  80. 0080apply beta_at_unique
  81. 0081exact hpair_witness_witness_left
  82. 0082exact hbounded_data_witness_left
  83. 0083have hibound : exists h. h + S x = n
  84. 0084rewrite hieq
  85. 0085exact hbounded_data_witness_right
  86. 0086have hinverse_data : exists q. ((((exists wpo_beta_height_wsl_inverse_at_i_entry. wpo_beta_height_wsl_inverse_at_i_entry + S (q) = S ((S (x)) * v)) /\ exists wpo_beta_quotient_wsl_inverse_at_i_entry. u = wpo_beta_quotient_wsl_inverse_at_i_entry * S ((S (x)) * v) + (q))) /\ ((exists wpo_gap_wsl_inverse_at_i_source_bound. wpo_gap_wsl_inverse_at_i_source_bound + S (x) = n) /\ ((exists wpo_gap_wsl_inverse_at_i_mate_bound. wpo_gap_wsl_inverse_at_i_mate_bound + S (q) = n) /\ exists y z. (S x * S q) + p * y = 1 + p * z)))
  87. 0087specialize hinverse x
  88. 0088apply hinverse
  89. 0089exact hibound
  90. 0090cases hinverse_data
  91. 0091cases hinverse_data_witness
  92. 0092cases hinverse_data_witness_right
  93. 0093cases hinverse_data_witness_right_right
  94. 0094have hjeq : x1 = x3
  95. 0095specialize beta_at_unique u
  96. 0096specialize beta_at_unique v
  97. 0097specialize beta_at_unique x
  98. 0098specialize beta_at_unique x1
  99. 0099specialize beta_at_unique x3
  100. 0100apply beta_at_unique
  101. 0101exact hpair_witness_witness_right_right
  102. 0102exact hinverse_data_witness_left
  103. 0103rewrite haeq
  104. 0104rewrite hdeq
  105. 0105rewrite hjeq
  106. 0106exact hinverse_data_witness_right_right_right