PA0079 · theorem

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.

Statement with defined notation

∀ p. ∀ a. ∀ x. ∀ y. ∀ t. Prime(p) → ¬Dvd(p,a) → Lt(x,p) → Lt(y,p) → ModEq(p,a · x,t) → ModEq(p,a · y,t) → x = y

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt PD0003 Dvd PD0004 Prime PD0008 ModEq

6 occurrences

In local proof propositions

PD0008 ModEq

3 occurrences

Exact expanded native-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

Proof neighborhood

Direct theorem prerequisites

PA003L mod_eq_symm PA0024 mod_eq_trans PA003S prime_mod_cancel PA002U mod_eq_bounded_unique

Direct theorem dependents

PA007A gauss_same_sign_scaled_source_unique

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 : ModEq(p,t,a · y)Definitions: ModEq(p,t,a · y)Original native command in the exact edition
  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 : ModEq(p,a · x,a · y)Definitions: ModEq(p,a · x,a · y)Original native command in the exact edition
  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 : ModEq(p,x,y)Definitions: ModEq(p,x,y)Original native command in the exact edition
  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 defined 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 : ModEq(p,t,a · y)
    Exact native replay linehave 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 : ModEq(p,a · x,a · y)
    Exact native replay linehave 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 : ModEq(p,x,y)
    Exact native replay linehave 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