PA0079

prime_scaled_same_target_unique

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

A nonzero prime residue multiplier is injective when two bounded sources have one modular target.

Exact expanded PA statement

forall p a x y t. ((~(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_collision_x_bound. gsp_lt_gap_collision_x_bound + S x = p) -> (exists gsp_lt_gap_collision_y_bound. gsp_lt_gap_collision_y_bound + S y = p) -> (exists gmp_mod_left_same_target_x gmp_mod_right_same_target_x. (a * x) + p * gmp_mod_left_same_target_x = (t) + p * gmp_mod_right_same_target_x) -> (exists gmp_mod_left_same_target_y gmp_mod_right_same_target_y. (a * y) + p * gmp_mod_left_same_target_y = (t) + p * gmp_mod_right_same_target_y) -> x = y

Structural proof guide

Generated structural guide

A nonzero prime residue multiplier is injective when two bounded sources have one modular target.

Use the direct prerequisites mod_eq_symm, mod_eq_trans, prime_mod_cancel, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by intermediate claims (3).

Referenced ingredients

PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Direct dependents

PA007A gauss_same_sign_scaled_source_unique

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 x
  4. 0004intro y
  5. 0005intro t
  6. 0006intro hp
  7. 0007intro hnotdiv
  8. 0008intro hxbound
  9. 0009intro hybound
  10. 0010intro hxtarget
  11. 0011intro hytarget
  12. 0012have hreverse : exists gmp_mod_left_same_target_reverse gmp_mod_right_same_target_reverse. (t) + p * gmp_mod_left_same_target_reverse = (a * y) + p * gmp_mod_right_same_target_reverse
  13. 0013specialize mod_eq_symm p
  14. 0014specialize mod_eq_symm (a * y)
  15. 0015specialize mod_eq_symm t
  16. 0016apply mod_eq_symm
  17. 0017exact hytarget
  18. 0018have hscaled : exists gmp_mod_left_same_target_scaled gmp_mod_right_same_target_scaled. (a * x) + p * gmp_mod_left_same_target_scaled = (a * y) + p * gmp_mod_right_same_target_scaled
  19. 0019specialize mod_eq_trans p
  20. 0020specialize mod_eq_trans (a * x)
  21. 0021specialize mod_eq_trans t
  22. 0022specialize mod_eq_trans (a * y)
  23. 0023apply mod_eq_trans
  24. 0024exact hxtarget
  25. 0025exact hreverse
  26. 0026have hcanceled : exists gmp_mod_left_same_target_canceled gmp_mod_right_same_target_canceled. (x) + p * gmp_mod_left_same_target_canceled = (y) + p * gmp_mod_right_same_target_canceled
  27. 0027specialize prime_mod_cancel p
  28. 0028specialize prime_mod_cancel a
  29. 0029specialize prime_mod_cancel x
  30. 0030specialize prime_mod_cancel y
  31. 0031apply prime_mod_cancel
  32. 0032exact hp
  33. 0033exact hnotdiv
  34. 0034exact hscaled
  35. 0035specialize mod_eq_bounded_unique p
  36. 0036specialize mod_eq_bounded_unique x
  37. 0037specialize mod_eq_bounded_unique y
  38. 0038apply mod_eq_bounded_unique
  39. 0039exact hxbound
  40. 0040exact hybound
  41. 0041exact hcanceled