PA00B9

beta_adjacent_unit_pairs_product_one

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

Adjacent inverse pairs multiply to one across an exact beta-coded even prefix.

Exact expanded PA statement

forall p b c m Q. (forall wpp_pair_pairs wpp_left_pairs wpp_right_pairs. (exists wpp_gap_pairs_pair_bound. wpp_gap_pairs_pair_bound + S (wpp_pair_pairs) = m) -> (((exists wpp_beta_height_pairs_left_entry. wpp_beta_height_pairs_left_entry + S (wpp_left_pairs) = S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_left_entry. b = wpp_beta_quotient_pairs_left_entry * S ((S ((wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_left_pairs))) -> (((exists wpp_beta_height_pairs_right_entry. wpp_beta_height_pairs_right_entry + S (wpp_right_pairs) = S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c)) /\ exists wpp_beta_quotient_pairs_right_entry. b = wpp_beta_quotient_pairs_right_entry * S ((S (S (wpp_pair_pairs + wpp_pair_pairs))) * c) + (wpp_right_pairs))) -> (exists wpp_mod_left_pairs_pair_mod wpp_mod_right_pairs_pair_mod. (wpp_left_pairs * wpp_right_pairs) + p * wpp_mod_left_pairs_pair_mod = (1) + p * wpp_mod_right_pairs_pair_mod)) -> (exists wpp_trace_code_pair_product wpp_trace_scale_pair_product. ((((exists wpp_beta_height_pair_product_start. wpp_beta_height_pair_product_start + S (1) = S ((S (0)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_start. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_start * S ((S (0)) * wpp_trace_scale_pair_product) + (1))) /\ ((((exists wpp_beta_height_pair_product_terminal. wpp_beta_height_pair_product_terminal + S (Q) = S ((S (m + m)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_terminal. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_terminal * S ((S (m + m)) * wpp_trace_scale_pair_product) + (Q))) /\ forall wpp_index_pair_product. (exists wpp_gap_pair_product_bound. wpp_gap_pair_product_bound + S (wpp_index_pair_product) = m + m) -> exists wpp_factor_pair_product wpp_prefix_pair_product wpp_successor_pair_product. ((((exists wpp_beta_height_pair_product_factor. wpp_beta_height_pair_product_factor + S (wpp_factor_pair_product) = S ((S (wpp_index_pair_product)) * c)) /\ exists wpp_beta_quotient_pair_product_factor. b = wpp_beta_quotient_pair_product_factor * S ((S (wpp_index_pair_product)) * c) + (wpp_factor_pair_product))) /\ ((((exists wpp_beta_height_pair_product_prefix. wpp_beta_height_pair_product_prefix + S (wpp_prefix_pair_product) = S ((S (wpp_index_pair_product)) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_prefix. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_prefix * S ((S (wpp_index_pair_product)) * wpp_trace_scale_pair_product) + (wpp_prefix_pair_product))) /\ ((((exists wpp_beta_height_pair_product_successor. wpp_beta_height_pair_product_successor + S (wpp_successor_pair_product) = S ((S (S (wpp_index_pair_product))) * wpp_trace_scale_pair_product)) /\ exists wpp_beta_quotient_pair_product_successor. wpp_trace_code_pair_product = wpp_beta_quotient_pair_product_successor * S ((S (S (wpp_index_pair_product))) * wpp_trace_scale_pair_product) + (wpp_successor_pair_product))) /\ wpp_successor_pair_product = wpp_prefix_pair_product * wpp_factor_pair_product)))))) -> (exists wpp_mod_left_pair_result wpp_mod_right_pair_result. (Q) + p * wpp_mod_left_pair_result = (1) + p * wpp_mod_right_pair_result)

Structural proof guide

Generated structural guide

Adjacent inverse pairs multiply to one across an exact beta-coded even prefix.

Use the direct prerequisites beta_product_double_succ_decompose, beta_product_zero, le_succ, le_refl, mod_eq_refl, mod_eq_mul, add_succ_left, mul_assoc, one_mul as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (6), intermediate claims (11), equality transport (7), certified simplification (2).

Referenced ingredients

PA009Y beta_product_double_succ_decompose PA0049 beta_product_zero PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000E add_succ_left PA000B mul_assoc PA000M one_mul

Proof neighborhood

Direct dependencies

PA009Y beta_product_double_succ_decompose PA0049 beta_product_zero PA002O le_succ PA001A le_refl PA0023 mod_eq_refl PA004E mod_eq_mul PA000E add_succ_left PA000B mul_assoc PA000M one_mul

Direct dependents

PA00BA paired_pair_order_product_one_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 b
  3. 0003intro c
  4. 0004induction m
  5. 0005intro Q
  6. 0006intro hpairs
  7. 0007intro hproduct
  8. 0008have hzero : 0 + 0 = 0
  9. 0009simp
  10. 0010rewrite hzero at hproduct
  11. 0011rewrite hzero at hproduct
  12. 0012rewrite hzero at hproduct
  13. 0013have hQ : Q = 1
  14. 0014specialize beta_product_zero b
  15. 0015specialize beta_product_zero c
  16. 0016specialize beta_product_zero Q
  17. 0017apply beta_product_zero
  18. 0018exact hproduct
  19. 0019rewrite hQ
  20. 0020specialize mod_eq_refl p
  21. 0021specialize mod_eq_refl 1
  22. 0022exact mod_eq_refl
  23. 0023intro Q
  24. 0024intro hpairs
  25. 0025intro hproduct
  26. 0026have hdouble : S m + S m = S (S (m + m))
  27. 0027simp [add_succ_left]
  28. 0028have hdecomposition : exists wpp_left_factor_successor_decomposition wpp_right_factor_successor_decomposition wpp_prefix_product_successor_decomposition. (((exists wpp_beta_height_successor_decomposition_left_entry. wpp_beta_height_successor_decomposition_left_entry + S (wpp_left_factor_successor_decomposition) = S ((S (m + m)) * c)) /\ exists wpp_beta_quotient_successor_decomposition_left_entry. b = wpp_beta_quotient_successor_decomposition_left_entry * S ((S (m + m)) * c) + (wpp_left_factor_successor_decomposition))) /\ ((((exists wpp_beta_height_successor_decomposition_right_entry. wpp_beta_height_successor_decomposition_right_entry + S (wpp_right_factor_successor_decomposition) = S ((S (S (m + m))) * c)) /\ exists wpp_beta_quotient_successor_decomposition_right_entry. b = wpp_beta_quotient_successor_decomposition_right_entry * S ((S (S (m + m))) * c) + (wpp_right_factor_successor_decomposition))) /\ ((exists wpp_trace_code_successor_decomposition_prefix wpp_trace_scale_successor_decomposition_prefix. ((((exists wpp_beta_height_successor_decomposition_prefix_start. wpp_beta_height_successor_decomposition_prefix_start + S (1) = S ((S (0)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_start. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_start * S ((S (0)) * wpp_trace_scale_successor_decomposition_prefix) + (1))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_terminal. wpp_beta_height_successor_decomposition_prefix_terminal + S (wpp_prefix_product_successor_decomposition) = S ((S (m + m)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_terminal. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_terminal * S ((S (m + m)) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_prefix_product_successor_decomposition))) /\ forall wpp_index_successor_decomposition_prefix. (exists wpp_gap_successor_decomposition_prefix_bound. wpp_gap_successor_decomposition_prefix_bound + S (wpp_index_successor_decomposition_prefix) = m + m) -> exists wpp_factor_successor_decomposition_prefix wpp_prefix_successor_decomposition_prefix wpp_successor_successor_decomposition_prefix. ((((exists wpp_beta_height_successor_decomposition_prefix_factor. wpp_beta_height_successor_decomposition_prefix_factor + S (wpp_factor_successor_decomposition_prefix) = S ((S (wpp_index_successor_decomposition_prefix)) * c)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_factor. b = wpp_beta_quotient_successor_decomposition_prefix_factor * S ((S (wpp_index_successor_decomposition_prefix)) * c) + (wpp_factor_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_prefix. wpp_beta_height_successor_decomposition_prefix_prefix + S (wpp_prefix_successor_decomposition_prefix) = S ((S (wpp_index_successor_decomposition_prefix)) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_prefix. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_prefix * S ((S (wpp_index_successor_decomposition_prefix)) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_prefix_successor_decomposition_prefix))) /\ ((((exists wpp_beta_height_successor_decomposition_prefix_successor. wpp_beta_height_successor_decomposition_prefix_successor + S (wpp_successor_successor_decomposition_prefix) = S ((S (S (wpp_index_successor_decomposition_prefix))) * wpp_trace_scale_successor_decomposition_prefix)) /\ exists wpp_beta_quotient_successor_decomposition_prefix_successor. wpp_trace_code_successor_decomposition_prefix = wpp_beta_quotient_successor_decomposition_prefix_successor * S ((S (S (wpp_index_successor_decomposition_prefix))) * wpp_trace_scale_successor_decomposition_prefix) + (wpp_successor_successor_decomposition_prefix))) /\ wpp_successor_successor_decomposition_prefix = wpp_prefix_successor_decomposition_prefix * wpp_factor_successor_decomposition_prefix)))))) /\ Q = (wpp_prefix_product_successor_decomposition * wpp_left_factor_successor_decomposition) * wpp_right_factor_successor_decomposition))
  29. 0029specialize beta_product_double_succ_decompose b
  30. 0030specialize beta_product_double_succ_decompose c
  31. 0031specialize beta_product_double_succ_decompose (m + m)
  32. 0032specialize beta_product_double_succ_decompose (S m + S m)
  33. 0033specialize beta_product_double_succ_decompose Q
  34. 0034apply beta_product_double_succ_decompose
  35. 0035exact hdouble
  36. 0036exact hproduct
  37. 0037cases hdecomposition
  38. 0038cases hdecomposition_witness
  39. 0039cases hdecomposition_witness_witness
  40. 0040cases hdecomposition_witness_witness_witness
  41. 0041cases hdecomposition_witness_witness_witness_right
  42. 0042cases hdecomposition_witness_witness_witness_right_right
  43. 0043have hpairs_all : forall wpp_pair_all_successor_pairs wpp_left_all_successor_pairs wpp_right_all_successor_pairs. (exists wpp_gap_all_successor_pairs_pair_bound. wpp_gap_all_successor_pairs_pair_bound + S (wpp_pair_all_successor_pairs) = S m) -> (((exists wpp_beta_height_all_successor_pairs_left_entry. wpp_beta_height_all_successor_pairs_left_entry + S (wpp_left_all_successor_pairs) = S ((S ((wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_all_successor_pairs_left_entry. b = wpp_beta_quotient_all_successor_pairs_left_entry * S ((S ((wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c) + (wpp_left_all_successor_pairs))) -> (((exists wpp_beta_height_all_successor_pairs_right_entry. wpp_beta_height_all_successor_pairs_right_entry + S (wpp_right_all_successor_pairs) = S ((S (S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c)) /\ exists wpp_beta_quotient_all_successor_pairs_right_entry. b = wpp_beta_quotient_all_successor_pairs_right_entry * S ((S (S (wpp_pair_all_successor_pairs + wpp_pair_all_successor_pairs))) * c) + (wpp_right_all_successor_pairs))) -> (exists wpp_mod_left_all_successor_pairs_pair_mod wpp_mod_right_all_successor_pairs_pair_mod. (wpp_left_all_successor_pairs * wpp_right_all_successor_pairs) + p * wpp_mod_left_all_successor_pairs_pair_mod = (1) + p * wpp_mod_right_all_successor_pairs_pair_mod)
  44. 0044exact hpairs
  45. 0045have hpairs_prefix : forall wpp_pair_prefix_pairs wpp_left_prefix_pairs wpp_right_prefix_pairs. (exists wpp_gap_prefix_pairs_pair_bound. wpp_gap_prefix_pairs_pair_bound + S (wpp_pair_prefix_pairs) = m) -> (((exists wpp_beta_height_prefix_pairs_left_entry. wpp_beta_height_prefix_pairs_left_entry + S (wpp_left_prefix_pairs) = S ((S ((wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_prefix_pairs_left_entry. b = wpp_beta_quotient_prefix_pairs_left_entry * S ((S ((wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c) + (wpp_left_prefix_pairs))) -> (((exists wpp_beta_height_prefix_pairs_right_entry. wpp_beta_height_prefix_pairs_right_entry + S (wpp_right_prefix_pairs) = S ((S (S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c)) /\ exists wpp_beta_quotient_prefix_pairs_right_entry. b = wpp_beta_quotient_prefix_pairs_right_entry * S ((S (S (wpp_pair_prefix_pairs + wpp_pair_prefix_pairs))) * c) + (wpp_right_prefix_pairs))) -> (exists wpp_mod_left_prefix_pairs_pair_mod wpp_mod_right_prefix_pairs_pair_mod. (wpp_left_prefix_pairs * wpp_right_prefix_pairs) + p * wpp_mod_left_prefix_pairs_pair_mod = (1) + p * wpp_mod_right_prefix_pairs_pair_mod)
  46. 0046intro t
  47. 0047intro a
  48. 0048intro d
  49. 0049intro ht
  50. 0050intro ha
  51. 0051intro hd
  52. 0052specialize hpairs_all t
  53. 0053specialize hpairs_all a
  54. 0054specialize hpairs_all d
  55. 0055apply hpairs_all
  56. 0056specialize le_succ (S t)
  57. 0057specialize le_succ m
  58. 0058apply le_succ
  59. 0059exact ht
  60. 0060exact ha
  61. 0061exact hd
  62. 0062have hprefix : exists wpp_mod_left_prefix_congruence wpp_mod_right_prefix_congruence. (x2) + p * wpp_mod_left_prefix_congruence = (1) + p * wpp_mod_right_prefix_congruence
  63. 0063specialize IH x2
  64. 0064apply IH
  65. 0065exact hpairs_prefix
  66. 0066exact hdecomposition_witness_witness_witness_right_right_left
  67. 0067have hlast : exists wpp_mod_left_last_pair_congruence wpp_mod_right_last_pair_congruence. (x * x1) + p * wpp_mod_left_last_pair_congruence = (1) + p * wpp_mod_right_last_pair_congruence
  68. 0068specialize hpairs m
  69. 0069specialize hpairs x
  70. 0070specialize hpairs x1
  71. 0071apply hpairs
  72. 0072specialize le_refl (S m)
  73. 0073exact le_refl
  74. 0074exact hdecomposition_witness_witness_witness_left
  75. 0075exact hdecomposition_witness_witness_witness_right_left
  76. 0076have hfold : exists wpp_mod_left_folded_congruence wpp_mod_right_folded_congruence. (x2 * (x * x1)) + p * wpp_mod_left_folded_congruence = (1 * 1) + p * wpp_mod_right_folded_congruence
  77. 0077specialize mod_eq_mul p
  78. 0078specialize mod_eq_mul x2
  79. 0079specialize mod_eq_mul 1
  80. 0080specialize mod_eq_mul (x * x1)
  81. 0081specialize mod_eq_mul 1
  82. 0082apply mod_eq_mul
  83. 0083exact hprefix
  84. 0084exact hlast
  85. 0085have hone : 1 * 1 = 1
  86. 0086specialize one_mul 1
  87. 0087exact one_mul
  88. 0088rewrite hone at hfold
  89. 0089have hassoc : (x2 * x) * x1 = x2 * (x * x1)
  90. 0090specialize mul_assoc x2
  91. 0091specialize mul_assoc x
  92. 0092specialize mul_assoc x1
  93. 0093exact mul_assoc
  94. 0094rewrite hdecomposition_witness_witness_witness_right_right_right
  95. 0095rewrite hassoc
  96. 0096exact hfold