PA005K

mod_eq_decidable_nonzero

Stable checked-use theorem · independently closed

Balanced congruence is constructively decidable at nonzero modulus.

Exact expanded PA statement

forall p a b. ~(p = 0) -> (exists qr_u_dec_yes qr_v_dec_yes. a + p * qr_u_dec_yes = b + p * qr_v_dec_yes) \/ ~(exists qr_u_dec_no qr_v_dec_no. a + p * qr_u_dec_no = b + p * qr_v_dec_no)

Structural proof guide

Generated structural guide

Balanced congruence is constructively decidable at nonzero modulus.

Use the direct prerequisites division_remainder_exists, mul_comm, mod_eq_decidable_from_remainders as previously established PA formulas.

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

Referenced ingredients

PA001D division_remainder_exists PA000H mul_comm PA005J mod_eq_decidable_from_remainders

Proof neighborhood

Direct dependencies

PA001D division_remainder_exists PA000H mul_comm PA005J mod_eq_decidable_from_remainders

Direct dependents

PA005L quadratic_residue_search_up_to

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 p
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hp
  5. 0005have hda : exists qa ra. a = p * qa + ra /\ exists ha. ha + S ra = p
  6. 0006specialize division_remainder_exists p
  7. 0007specialize division_remainder_exists a
  8. 0008apply division_remainder_exists
  9. 0009exact hp
  10. 0010cases hda
  11. 0011cases hda_witness
  12. 0012cases hda_witness_witness
  13. 0013have hdb : exists qb rb. b = p * qb + rb /\ exists hb. hb + S rb = p
  14. 0014specialize division_remainder_exists p
  15. 0015specialize division_remainder_exists b
  16. 0016apply division_remainder_exists
  17. 0017exact hp
  18. 0018cases hdb
  19. 0019cases hdb_witness
  20. 0020cases hdb_witness_witness
  21. 0021have ha_comm : a = x * p + x1
  22. 0022trans p * x + x1
  23. 0023exact hda_witness_witness_left
  24. 0024congr
  25. 0025apply mul_comm
  26. 0026refl
  27. 0027have hb_comm : b = x2 * p + x3
  28. 0028trans p * x2 + x3
  29. 0029exact hdb_witness_witness_left
  30. 0030congr
  31. 0031apply mul_comm
  32. 0032refl
  33. 0033specialize mod_eq_decidable_from_remainders p
  34. 0034specialize mod_eq_decidable_from_remainders a
  35. 0035specialize mod_eq_decidable_from_remainders b
  36. 0036specialize mod_eq_decidable_from_remainders x
  37. 0037specialize mod_eq_decidable_from_remainders x1
  38. 0038specialize mod_eq_decidable_from_remainders x2
  39. 0039specialize mod_eq_decidable_from_remainders x3
  40. 0040apply mod_eq_decidable_from_remainders
  41. 0041exact ha_comm
  42. 0042exact hda_witness_witness_right
  43. 0043exact hb_comm
  44. 0044exact hdb_witness_witness_right