PA0079

prime_scaled_same_target_unique

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

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

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

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-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

Read the argument

Proof checkpoints

41 script commands · 6 reading checkpoints · 3 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (4)
mod eq symmmod eq transprime mod cancelmod eq bounded unique
01Fix variables and assumptionsL1–10

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro p
  2. L2
    intro a
  3. L3
    intro x
  4. L4
    intro y
  5. L5
    intro t
  6. L6
    intro hp
  7. L7
    intro hnotdiv
  8. L8
    intro hxbound
  9. L9
    intro hybound
  10. L10
    intro hxtarget
02Fix variables and assumptionsL11–11

Work with arbitrary variables or the premises of the current implication.

  1. L11
    intro hytarget
03Establish hreverseL12–17

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L12
    have 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
  2. L13
    specialize mod_eq_symm p
  3. L14
    specialize mod_eq_symm (a * y)
  4. L15
    specialize mod_eq_symm t
  5. L16
    apply mod_eq_symm
  6. L17
    exact hytarget
04Establish hscaledL18–25

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L18
    have 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
  2. L19
    specialize mod_eq_trans p
  3. L20
    specialize mod_eq_trans (a * x)
  4. L21
    specialize mod_eq_trans t
  5. L22
    specialize mod_eq_trans (a * y)
  6. L23
    apply mod_eq_trans
  7. L24
    exact hxtarget
  8. L25
    exact hreverse
05Establish hcanceledL26–35

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mod cancel.

  1. L26
    have 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
  2. L27
    specialize prime_mod_cancel p
  3. L28
    specialize prime_mod_cancel a
  4. L29
    specialize prime_mod_cancel x
  5. L30
    specialize prime_mod_cancel y
  6. L31
    apply prime_mod_cancel
  7. L32
    exact hp
  8. L33
    exact hnotdiv
  9. L34
    exact hscaled
  10. L35
    specialize mod_eq_bounded_unique p
06Use earlier factsL36–41

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L36
    specialize mod_eq_bounded_unique x
  2. L37
    specialize mod_eq_bounded_unique y
  3. L38
    apply mod_eq_bounded_unique
  4. L39
    exact hxbound
  5. L40
    exact hybound
  6. L41
    exact hcanceled

Library-wide reading audit

Original exact command ledger · 41 lines
  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