PA007A

gauss_same_sign_scaled_source_unique

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

Equal lower signs or equal reflected signs force equality of the bounded source residues.

Exact expanded PA statement

forall p h a x y m. ((~(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_sign_x_lower gmp_mod_right_same_sign_x_lower. (a * x) + p * gmp_mod_left_same_sign_x_lower = (m) + p * gmp_mod_right_same_sign_x_lower) /\ (exists gmp_mod_left_same_sign_y_lower gmp_mod_right_same_sign_y_lower. (a * y) + p * gmp_mod_left_same_sign_y_lower = (m) + p * gmp_mod_right_same_sign_y_lower)) \/ ((exists gmp_mod_left_same_sign_x_reflected gmp_mod_right_same_sign_x_reflected. (a * x) + p * gmp_mod_left_same_sign_x_reflected = ((2 * h) * m) + p * gmp_mod_right_same_sign_x_reflected) /\ (exists gmp_mod_left_same_sign_y_reflected gmp_mod_right_same_sign_y_reflected. (a * y) + p * gmp_mod_left_same_sign_y_reflected = ((2 * h) * m) + p * gmp_mod_right_same_sign_y_reflected)))) -> x = y

Structural proof guide

Generated structural guide

Equal lower signs or equal reflected signs force equality of the bounded source residues.

Use the direct prerequisites prime_scaled_same_target_unique as previously established PA formulas.

The proof proceeds by case analysis (3).

Referenced ingredients

PA0079 prime_scaled_same_target_unique

Proof neighborhood

Direct dependencies

PA0079 prime_scaled_same_target_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 hp
  8. 0008intro hnotdiv
  9. 0009intro hxbound
  10. 0010intro hybound
  11. 0011intro hsame
  12. 0012cases hsame
  13. 0013cases hsame_left
  14. 0014specialize prime_scaled_same_target_unique p
  15. 0015specialize prime_scaled_same_target_unique a
  16. 0016specialize prime_scaled_same_target_unique x
  17. 0017specialize prime_scaled_same_target_unique y
  18. 0018specialize prime_scaled_same_target_unique m
  19. 0019apply prime_scaled_same_target_unique
  20. 0020exact hp
  21. 0021exact hnotdiv
  22. 0022exact hxbound
  23. 0023exact hybound
  24. 0024exact hsame_left_left
  25. 0025exact hsame_left_right
  26. 0026cases hsame_right
  27. 0027specialize prime_scaled_same_target_unique p
  28. 0028specialize prime_scaled_same_target_unique a
  29. 0029specialize prime_scaled_same_target_unique x
  30. 0030specialize prime_scaled_same_target_unique y
  31. 0031specialize prime_scaled_same_target_unique (2 * h) * m
  32. 0032apply prime_scaled_same_target_unique
  33. 0033exact hp
  34. 0034exact hnotdiv
  35. 0035exact hxbound
  36. 0036exact hybound
  37. 0037exact hsame_right_left
  38. 0038exact hsame_right_right