PA007B

gauss_mixed_sign_scaled_source_impossible

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

Opposite signed representatives cannot share one magnitude when their positive source sum is below p.

Exact expanded PA statement

forall p h a x y m. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_collision_prime gsp_prime_right_collision_prime. p = gsp_prime_left_collision_prime * gsp_prime_right_collision_prime -> gsp_prime_left_collision_prime = 1 \/ gsp_prime_right_collision_prime = 1)) -> (~(exists gsp_divisor_factor_collision_multiplier. a = p * gsp_divisor_factor_collision_multiplier)) -> (exists gsp_lt_gap_mixed_sum_bound. gsp_lt_gap_mixed_sum_bound + S (x + y) = p) -> ~(x + y = 0) -> (exists gmp_mod_left_mixed_x_lower gmp_mod_right_mixed_x_lower. (a * x) + p * gmp_mod_left_mixed_x_lower = (m) + p * gmp_mod_right_mixed_x_lower) -> (exists gmp_mod_left_mixed_y_reflected gmp_mod_right_mixed_y_reflected. (a * y) + p * gmp_mod_left_mixed_y_reflected = ((2 * h) * m) + p * gmp_mod_right_mixed_y_reflected) -> false

Structural proof guide

Generated structural guide

Opposite signed representatives cannot share one magnitude when their positive source sum is below p.

Use the direct prerequisites mod_eq_add, mul_add, mul_succ_left, add_comm, dvd_to_mod_zero, mod_eq_trans, prime_mod_cancel, prime_nonzero, one_le_of_ne_zero, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by case analysis (4), intermediate claims (9), equality transport (1), certified simplification (2).

Referenced ingredients

PA0022 mod_eq_add PA000A mul_add PA000G mul_succ_left PA000F add_comm PA0021 dvd_to_mod_zero PA0024 mod_eq_trans PA003S prime_mod_cancel PA0031 prime_nonzero PA002L one_le_of_ne_zero PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA0022 mod_eq_add PA000A mul_add PA000G mul_succ_left PA000F add_comm PA0021 dvd_to_mod_zero PA0024 mod_eq_trans PA003S prime_mod_cancel PA0031 prime_nonzero PA002L one_le_of_ne_zero PA002U mod_eq_bounded_unique

Direct dependents

PA007C gauss_signed_half_magnitude_injective

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 a
  4. 0004intro x
  5. 0005intro y
  6. 0006intro m
  7. 0007intro hpodd
  8. 0008intro hp
  9. 0009intro hnotdiv
  10. 0010intro hsum_bound
  11. 0011intro hsum_nonzero
  12. 0012intro hxlower
  13. 0013intro hyreflected
  14. 0014have hadd : exists gmp_mod_left_mixed_added gmp_mod_right_mixed_added. (a * x + a * y) + p * gmp_mod_left_mixed_added = (m + (2 * h) * m) + p * gmp_mod_right_mixed_added
  15. 0015specialize mod_eq_add p
  16. 0016specialize mod_eq_add (a * x)
  17. 0017specialize mod_eq_add m
  18. 0018specialize mod_eq_add (a * y)
  19. 0019specialize mod_eq_add (2 * h) * m
  20. 0020apply mod_eq_add
  21. 0021exact hxlower
  22. 0022exact hyreflected
  23. 0023cases hadd
  24. 0024cases hadd_witness
  25. 0025have hscaled_multiple : exists gmp_mod_left_mixed_scaled_sum_multiple gmp_mod_right_mixed_scaled_sum_multiple. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_multiple = (p * m) + p * gmp_mod_right_mixed_scaled_sum_multiple
  26. 0026exists x1
  27. 0027exists x2
  28. 0028trans (a * x + a * y) + p * x1
  29. 0029congr
  30. 0030apply mul_add
  31. 0031refl
  32. 0032trans (m + (2 * h) * m) + p * x2
  33. 0033exact hadd_witness_witness
  34. 0034congr
  35. 0035rewrite hpodd
  36. 0036simp [mul_succ_left, add_comm]
  37. 0037refl
  38. 0038have hmultiple_zero : exists gmp_mod_left_mixed_multiple_zero gmp_mod_right_mixed_multiple_zero. (p * m) + p * gmp_mod_left_mixed_multiple_zero = (0) + p * gmp_mod_right_mixed_multiple_zero
  39. 0039specialize dvd_to_mod_zero p
  40. 0040specialize dvd_to_mod_zero (p * m)
  41. 0041apply dvd_to_mod_zero
  42. 0042exists m
  43. 0043refl
  44. 0044have hscaled_zero : exists gmp_mod_left_mixed_scaled_sum_zero gmp_mod_right_mixed_scaled_sum_zero. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_zero = (0) + p * gmp_mod_right_mixed_scaled_sum_zero
  45. 0045specialize mod_eq_trans p
  46. 0046specialize mod_eq_trans (a * (x + y))
  47. 0047specialize mod_eq_trans (p * m)
  48. 0048specialize mod_eq_trans 0
  49. 0049apply mod_eq_trans
  50. 0050exact hscaled_multiple
  51. 0051exact hmultiple_zero
  52. 0052cases hscaled_zero
  53. 0053cases hscaled_zero_witness
  54. 0054have hscaled_factor_zero : exists gmp_mod_left_mixed_scaled_sum_factor_zero gmp_mod_right_mixed_scaled_sum_factor_zero. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_factor_zero = (a * 0) + p * gmp_mod_right_mixed_scaled_sum_factor_zero
  55. 0055exists x3
  56. 0056exists x4
  57. 0057trans 0 + p * x4
  58. 0058exact hscaled_zero_witness_witness
  59. 0059congr
  60. 0060simp
  61. 0061refl
  62. 0062have hsum_zero_mod : exists gmp_mod_left_mixed_sum_zero gmp_mod_right_mixed_sum_zero. (x + y) + p * gmp_mod_left_mixed_sum_zero = (0) + p * gmp_mod_right_mixed_sum_zero
  63. 0063specialize prime_mod_cancel p
  64. 0064specialize prime_mod_cancel a
  65. 0065specialize prime_mod_cancel (x + y)
  66. 0066specialize prime_mod_cancel 0
  67. 0067apply prime_mod_cancel
  68. 0068exact hp
  69. 0069exact hnotdiv
  70. 0070exact hscaled_factor_zero
  71. 0071have hp0 : ~(p = 0)
  72. 0072intro hpzero
  73. 0073specialize prime_nonzero p
  74. 0074apply prime_nonzero
  75. 0075exact hp
  76. 0076exact hpzero
  77. 0077have hzero_bound : exists gsp_lt_gap_mixed_zero_bound. gsp_lt_gap_mixed_zero_bound + S 0 = p
  78. 0078specialize one_le_of_ne_zero p
  79. 0079apply one_le_of_ne_zero
  80. 0080exact hp0
  81. 0081have hsum_zero : x + y = 0
  82. 0082specialize mod_eq_bounded_unique p
  83. 0083specialize mod_eq_bounded_unique (x + y)
  84. 0084specialize mod_eq_bounded_unique 0
  85. 0085apply mod_eq_bounded_unique
  86. 0086exact hsum_bound
  87. 0087exact hzero_bound
  88. 0088exact hsum_zero_mod
  89. 0089apply hsum_nonzero
  90. 0090exact hsum_zero