PA002U

mod_eq_bounded_unique

Stable checked-use theorem · independently closed

Two balanced-congruent values below the same modulus are equal.

Exact expanded PA statement

forall m a b. (exists ha. ha + S a = m) -> (exists hb. hb + S b = m) -> (exists u v. a + m * u = b + m * v) -> a = b

Structural proof guide

Generated structural guide

Two balanced-congruent values below the same modulus are equal.

Use the direct prerequisites add_comm, division_remainder_unique as previously established PA formulas.

The proof proceeds by case analysis (3), intermediate claims (3).

Referenced ingredients

PA000F add_comm PA002E division_remainder_unique

Proof neighborhood

Direct dependencies

PA000F add_comm PA002E division_remainder_unique

Direct dependents

PA002V mod_eq_to_remainder_decomposition PA005J mod_eq_decidable_from_remainders PA0063 prime_bounded_nonzero_mod_inverse PA00AK bounded_mod_inverse_unique PA0079 prime_scaled_same_target_unique PA007B gauss_mixed_sign_scaled_source_impossible PA008E prime_mul_index_map_injective PA008P prime_scaled_inverse_target_nonzero PA009C prime_scaled_inverse_unique PA00BP odd_prime_one_not_mod_predecessor PA00C5 canonical_remainder_from_mod

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

  1. 0001intro m
  2. 0002intro a
  3. 0003intro b
  4. 0004intro ha
  5. 0005intro hb
  6. 0006intro hab
  7. 0007cases hab
  8. 0008cases hab_witness
  9. 0009have hda : a + m * x = m * x + a
  10. 0010apply add_comm
  11. 0011have hdb : a + m * x = m * x1 + b
  12. 0012trans b + m * x1
  13. 0013exact hab_witness_witness
  14. 0014apply add_comm
  15. 0015specialize division_remainder_unique m
  16. 0016specialize division_remainder_unique (a + m * x)
  17. 0017specialize division_remainder_unique x
  18. 0018specialize division_remainder_unique a
  19. 0019specialize division_remainder_unique x1
  20. 0020specialize division_remainder_unique b
  21. 0021have huniq : x = x1 /\ a = b
  22. 0022apply division_remainder_unique
  23. 0023exact hda
  24. 0024exact ha
  25. 0025exact hdb
  26. 0026exact hb
  27. 0027cases huniq
  28. 0028exact huniq_right