PA007P

gauss_signed_pointwise_mul_scale_mod

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

Signed magnitudes times their 1/r factors are pointwise congruent to the scaled source prefix.

Exact expanded PA statement

forall p h r a b c mb mc sb sc fb fc tb tc. p = S r -> r = 2 * h -> (forall gsp_index_pointwise_signed_prefix. (exists gsp_lt_gap_pointwise_signed_prefix_index_bound. gsp_lt_gap_pointwise_signed_prefix_index_bound + S gsp_index_pointwise_signed_prefix = h) -> (exists gsp_value_pointwise_signed_prefix_entry gsp_magnitude_pointwise_signed_prefix_entry gsp_sign_pointwise_signed_prefix_entry. (((exists ff_h_gsp_pointwise_signed_prefix_entry_source. ff_h_gsp_pointwise_signed_prefix_entry_source + S (gsp_value_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * c)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_source. b = ff_q_gsp_pointwise_signed_prefix_entry_source * S ((S (gsp_index_pointwise_signed_prefix)) * c) + (gsp_value_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_magnitude. ff_h_gsp_pointwise_signed_prefix_entry_magnitude + S (gsp_magnitude_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * mc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_magnitude. mb = ff_q_gsp_pointwise_signed_prefix_entry_magnitude * S ((S (gsp_index_pointwise_signed_prefix)) * mc) + (gsp_magnitude_pointwise_signed_prefix_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_prefix_entry_sign. ff_h_gsp_pointwise_signed_prefix_entry_sign + S (gsp_sign_pointwise_signed_prefix_entry) = S ((S (gsp_index_pointwise_signed_prefix)) * sc)) /\ exists ff_q_gsp_pointwise_signed_prefix_entry_sign. sb = ff_q_gsp_pointwise_signed_prefix_entry_sign * S ((S (gsp_index_pointwise_signed_prefix)) * sc) + (gsp_sign_pointwise_signed_prefix_entry))) /\ ((exists gsp_lt_gap_pointwise_signed_prefix_entry_positive. gsp_lt_gap_pointwise_signed_prefix_entry_positive + S 0 = gsp_magnitude_pointwise_signed_prefix_entry) /\ ((exists gsp_le_gap_pointwise_signed_prefix_entry_bounded. gsp_le_gap_pointwise_signed_prefix_entry_bounded + gsp_magnitude_pointwise_signed_prefix_entry = h) /\ ((gsp_sign_pointwise_signed_prefix_entry = 0 \/ gsp_sign_pointwise_signed_prefix_entry = 1) /\ (((gsp_sign_pointwise_signed_prefix_entry = 0 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_lower gsp_mod_right_pointwise_signed_prefix_entry_lower. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_lower = (gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_lower)) \/ (gsp_sign_pointwise_signed_prefix_entry = 1 /\ (exists gsp_mod_left_pointwise_signed_prefix_entry_reflected gsp_mod_right_pointwise_signed_prefix_entry_reflected. (a * gsp_value_pointwise_signed_prefix_entry) + p * gsp_mod_left_pointwise_signed_prefix_entry_reflected = ((2 * h) * gsp_magnitude_pointwise_signed_prefix_entry) + p * gsp_mod_right_pointwise_signed_prefix_entry_reflected))))))))))) -> (forall gspf_index_pointwise_sign_factors gspf_bit_pointwise_sign_factors. (exists gsp_lt_gap_pointwise_sign_factors_bound. gsp_lt_gap_pointwise_sign_factors_bound + S gspf_index_pointwise_sign_factors = h) -> (((exists ff_h_gspf_pointwise_sign_factors_bit. ff_h_gspf_pointwise_sign_factors_bit + S (gspf_bit_pointwise_sign_factors) = S ((S (gspf_index_pointwise_sign_factors)) * sc)) /\ exists ff_q_gspf_pointwise_sign_factors_bit. sb = ff_q_gspf_pointwise_sign_factors_bit * S ((S (gspf_index_pointwise_sign_factors)) * sc) + (gspf_bit_pointwise_sign_factors))) -> (((gspf_bit_pointwise_sign_factors = 0) /\ (((exists gsp_beta_height_gspf_pointwise_sign_factors_one. gsp_beta_height_gspf_pointwise_sign_factors_one + S (1) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists gsp_beta_quotient_gspf_pointwise_sign_factors_one. fb = gsp_beta_quotient_gspf_pointwise_sign_factors_one * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (1)))) \/ ((gspf_bit_pointwise_sign_factors = 1) /\ (((exists ff_h_gspf_pointwise_sign_factors_predecessor. ff_h_gspf_pointwise_sign_factors_predecessor + S (r) = S ((S (gspf_index_pointwise_sign_factors)) * fc)) /\ exists ff_q_gspf_pointwise_sign_factors_predecessor. fb = ff_q_gspf_pointwise_sign_factors_predecessor * S ((S (gspf_index_pointwise_sign_factors)) * fc) + (r)))))) -> (forall fpmp_index_pointwise_products fpmp_left_pointwise_products fpmp_right_pointwise_products fpmp_target_pointwise_products. (exists fpmp_gap_pointwise_products. fpmp_gap_pointwise_products + S fpmp_index_pointwise_products = h) -> (((exists ff_h_fpmp_pointwise_products_left. ff_h_fpmp_pointwise_products_left + S (fpmp_left_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * mc)) /\ exists ff_q_fpmp_pointwise_products_left. mb = ff_q_fpmp_pointwise_products_left * S ((S (fpmp_index_pointwise_products)) * mc) + (fpmp_left_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_right. ff_h_fpmp_pointwise_products_right + S (fpmp_right_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * fc)) /\ exists ff_q_fpmp_pointwise_products_right. fb = ff_q_fpmp_pointwise_products_right * S ((S (fpmp_index_pointwise_products)) * fc) + (fpmp_right_pointwise_products))) -> (((exists ff_h_fpmp_pointwise_products_target. ff_h_fpmp_pointwise_products_target + S (fpmp_target_pointwise_products) = S ((S (fpmp_index_pointwise_products)) * tc)) /\ exists ff_q_fpmp_pointwise_products_target. tb = ff_q_fpmp_pointwise_products_target * S ((S (fpmp_index_pointwise_products)) * tc) + (fpmp_target_pointwise_products))) -> fpmp_target_pointwise_products = fpmp_left_pointwise_products * fpmp_right_pointwise_products) -> (forall fsp_index_pointwise_scale_result fsp_source_pointwise_scale_result fsp_target_pointwise_scale_result. (exists fsp_gap_pointwise_scale_result. fsp_gap_pointwise_scale_result + S fsp_index_pointwise_scale_result = h) -> (((exists fsp_source_height_pointwise_scale_result. fsp_source_height_pointwise_scale_result + S (fsp_source_pointwise_scale_result) = S ((S (fsp_index_pointwise_scale_result)) * c)) /\ exists fsp_source_quotient_pointwise_scale_result. b = fsp_source_quotient_pointwise_scale_result * S ((S (fsp_index_pointwise_scale_result)) * c) + (fsp_source_pointwise_scale_result))) -> (((exists fsp_target_height_pointwise_scale_result. fsp_target_height_pointwise_scale_result + S (fsp_target_pointwise_scale_result) = S ((S (fsp_index_pointwise_scale_result)) * tc)) /\ exists fsp_target_quotient_pointwise_scale_result. tb = fsp_target_quotient_pointwise_scale_result * S ((S (fsp_index_pointwise_scale_result)) * tc) + (fsp_target_pointwise_scale_result))) -> (exists fsp_mod_left_pointwise_scale_result fsp_mod_right_pointwise_scale_result. a * fsp_source_pointwise_scale_result + p * fsp_mod_left_pointwise_scale_result = fsp_target_pointwise_scale_result + p * fsp_mod_right_pointwise_scale_result))

Structural proof guide

Generated structural guide

Signed magnitudes times their 1/r factors are pointwise congruent to the scaled source prefix.

Use the direct prerequisites beta_at_unique, mul_one, mul_comm as previously established PA formulas.

The proof proceeds by case analysis (18), intermediate claims (6), equality transport (5).

Referenced ingredients

PA002F beta_at_unique PA0002 mul_one PA000H mul_comm

Proof neighborhood

Direct dependencies

PA002F beta_at_unique PA0002 mul_one PA000H mul_comm

Direct dependents

PA007R gauss_signed_pointwise_mul_product_mod

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 h
  3. 0003intro r
  4. 0004intro a
  5. 0005intro b
  6. 0006intro c
  7. 0007intro mb
  8. 0008intro mc
  9. 0009intro sb
  10. 0010intro sc
  11. 0011intro fb
  12. 0012intro fc
  13. 0013intro tb
  14. 0014intro tc
  15. 0015intro hp
  16. 0016intro hr
  17. 0017intro hsigned
  18. 0018intro hfactor
  19. 0019intro hmul
  20. 0020intro i
  21. 0021intro v
  22. 0022intro t
  23. 0023intro hi
  24. 0024intro hv
  25. 0025intro ht
  26. 0026have hentry : exists gsp_value_pointwise_signed_entry gsp_magnitude_pointwise_signed_entry gsp_sign_pointwise_signed_entry. (((exists ff_h_gsp_pointwise_signed_entry_source. ff_h_gsp_pointwise_signed_entry_source + S (gsp_value_pointwise_signed_entry) = S ((S (i)) * c)) /\ exists ff_q_gsp_pointwise_signed_entry_source. b = ff_q_gsp_pointwise_signed_entry_source * S ((S (i)) * c) + (gsp_value_pointwise_signed_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_entry_magnitude. ff_h_gsp_pointwise_signed_entry_magnitude + S (gsp_magnitude_pointwise_signed_entry) = S ((S (i)) * mc)) /\ exists ff_q_gsp_pointwise_signed_entry_magnitude. mb = ff_q_gsp_pointwise_signed_entry_magnitude * S ((S (i)) * mc) + (gsp_magnitude_pointwise_signed_entry))) /\ ((((exists ff_h_gsp_pointwise_signed_entry_sign. ff_h_gsp_pointwise_signed_entry_sign + S (gsp_sign_pointwise_signed_entry) = S ((S (i)) * sc)) /\ exists ff_q_gsp_pointwise_signed_entry_sign. sb = ff_q_gsp_pointwise_signed_entry_sign * S ((S (i)) * sc) + (gsp_sign_pointwise_signed_entry))) /\ ((exists gsp_lt_gap_pointwise_signed_entry_positive. gsp_lt_gap_pointwise_signed_entry_positive + S 0 = gsp_magnitude_pointwise_signed_entry) /\ ((exists gsp_le_gap_pointwise_signed_entry_bounded. gsp_le_gap_pointwise_signed_entry_bounded + gsp_magnitude_pointwise_signed_entry = h) /\ ((gsp_sign_pointwise_signed_entry = 0 \/ gsp_sign_pointwise_signed_entry = 1) /\ (((gsp_sign_pointwise_signed_entry = 0 /\ (exists gsp_mod_left_pointwise_signed_entry_lower gsp_mod_right_pointwise_signed_entry_lower. (a * gsp_value_pointwise_signed_entry) + p * gsp_mod_left_pointwise_signed_entry_lower = (gsp_magnitude_pointwise_signed_entry) + p * gsp_mod_right_pointwise_signed_entry_lower)) \/ (gsp_sign_pointwise_signed_entry = 1 /\ (exists gsp_mod_left_pointwise_signed_entry_reflected gsp_mod_right_pointwise_signed_entry_reflected. (a * gsp_value_pointwise_signed_entry) + p * gsp_mod_left_pointwise_signed_entry_reflected = ((2 * h) * gsp_magnitude_pointwise_signed_entry) + p * gsp_mod_right_pointwise_signed_entry_reflected)))))))))
  27. 0027specialize hsigned i
  28. 0028apply hsigned
  29. 0029exact hi
  30. 0030cases hentry
  31. 0031cases hentry_witness
  32. 0032cases hentry_witness_witness
  33. 0033cases hentry_witness_witness_witness
  34. 0034cases hentry_witness_witness_witness_right
  35. 0035cases hentry_witness_witness_witness_right_right
  36. 0036cases hentry_witness_witness_witness_right_right_right
  37. 0037cases hentry_witness_witness_witness_right_right_right_right
  38. 0038cases hentry_witness_witness_witness_right_right_right_right_right
  39. 0039have hvx : v = x
  40. 0040specialize beta_at_unique b
  41. 0041specialize beta_at_unique c
  42. 0042specialize beta_at_unique i
  43. 0043specialize beta_at_unique v
  44. 0044specialize beta_at_unique x
  45. 0045apply beta_at_unique
  46. 0046exact hv
  47. 0047exact hentry_witness_witness_witness_left
  48. 0048have hfactor_case : (((x2 = 0) /\ (((exists gsp_beta_height_pointwise_factor_one. gsp_beta_height_pointwise_factor_one + S (1) = S ((S (i)) * fc)) /\ exists gsp_beta_quotient_pointwise_factor_one. fb = gsp_beta_quotient_pointwise_factor_one * S ((S (i)) * fc) + (1)))) \/ ((x2 = 1) /\ (((exists ff_h_pointwise_factor_r. ff_h_pointwise_factor_r + S (r) = S ((S (i)) * fc)) /\ exists ff_q_pointwise_factor_r. fb = ff_q_pointwise_factor_r * S ((S (i)) * fc) + (r)))))
  49. 0049specialize hfactor i
  50. 0050specialize hfactor x2
  51. 0051apply hfactor
  52. 0052exact hi
  53. 0053exact hentry_witness_witness_witness_right_right_left
  54. 0054cases hentry_witness_witness_witness_right_right_right_right_right_right
  55. 0055cases hentry_witness_witness_witness_right_right_right_right_right_right_left
  56. 0056cases hfactor_case
  57. 0057cases hfactor_case_left
  58. 0058have ht_one : t = x1 * 1
  59. 0059specialize hmul i
  60. 0060specialize hmul x1
  61. 0061specialize hmul 1
  62. 0062specialize hmul t
  63. 0063apply hmul
  64. 0064exact hi
  65. 0065exact hentry_witness_witness_witness_right_left
  66. 0066exact hfactor_case_left_right
  67. 0067exact ht
  68. 0068rewrite hvx
  69. 0069rewrite ht_one
  70. 0070specialize mul_one x1
  71. 0071rewrite mul_one
  72. 0072exact hentry_witness_witness_witness_right_right_right_right_right_right_left_right
  73. 0073cases hfactor_case_right
  74. 0074exfalso
  75. 0075apply PA1
  76. 0076trans x2
  77. 0077symm
  78. 0078exact hfactor_case_right_left
  79. 0079exact hentry_witness_witness_witness_right_right_right_right_right_right_left_left
  80. 0080cases hentry_witness_witness_witness_right_right_right_right_right_right_right
  81. 0081cases hfactor_case
  82. 0082cases hfactor_case_left
  83. 0083exfalso
  84. 0084apply PA1
  85. 0085trans x2
  86. 0086symm
  87. 0087exact hentry_witness_witness_witness_right_right_right_right_right_right_right_left
  88. 0088exact hfactor_case_left_left
  89. 0089cases hfactor_case_right
  90. 0090have ht_r : t = x1 * r
  91. 0091specialize hmul i
  92. 0092specialize hmul x1
  93. 0093specialize hmul r
  94. 0094specialize hmul t
  95. 0095apply hmul
  96. 0096exact hi
  97. 0097exact hentry_witness_witness_witness_right_left
  98. 0098exact hfactor_case_right_right
  99. 0099exact ht
  100. 0100have ht_reflected : t = (2 * h) * x1
  101. 0101trans x1 * r
  102. 0102exact ht_r
  103. 0103trans r * x1
  104. 0104apply mul_comm
  105. 0105congr
  106. 0106exact hr
  107. 0107refl
  108. 0108rewrite hvx
  109. 0109rewrite ht_reflected
  110. 0110exact hentry_witness_witness_witness_right_right_right_right_right_right_right_right