BT003X

mod_eq_to_remainder_decomposition

Stable · empty-context checked

A bounded balanced residue has a directed quotient/remainder witness.

Exact expanded PA statement

forall m b x. ~(m = 0) -> (exists h. h + S x = m) -> (exists u v. b + m * u = x + m * v) -> exists q. b = q * m + x

Structural proof guide

A bounded balanced residue has a directed quotient/remainder witness.

Direct prerequisites: division_remainder_exists, add_comm, mul_comm, mod_eq_trans, mod_eq_bounded_unique. The authored body proceeds by case analysis (3), intermediate claims (4), equality transport (1).

Proof neighborhood

Direct dependencies

BT001P division_remainder_exists BT0002 add_comm BT0006 mul_comm BT003Q mod_eq_trans BT003W mod_eq_bounded_unique

Direct dependents

BT0045 beta_at_of_mod_eq_bound

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  1. 0001intro m
  2. 0002intro b
  3. 0003intro x
  4. 0004intro hm
  5. 0005intro hx
  6. 0006intro hbx
  7. 0007have hdiv : exists q r. b = m * q + r /\ exists h. h + S r = m
  8. 0008specialize division_remainder_exists m
  9. 0009specialize division_remainder_exists b
  10. 0010apply division_remainder_exists
  11. 0011exact hm
  12. 0012cases hdiv
  13. 0013cases hdiv_witness
  14. 0014cases hdiv_witness_witness
  15. 0015have hremb : exists u v. x2 + m * u = b + m * v
  16. 0016exists x1
  17. 0017exists 0
  18. 0018trans m * x1 + x2
  19. 0019apply add_comm
  20. 0020trans b
  21. 0021symm
  22. 0022exact hdiv_witness_witness_left
  23. 0023symm
  24. 0024rewrite PA5
  25. 0025apply PA3
  26. 0026have hremx : exists u v. x2 + m * u = x + m * v
  27. 0027specialize mod_eq_trans m
  28. 0028specialize mod_eq_trans x2
  29. 0029specialize mod_eq_trans b
  30. 0030specialize mod_eq_trans x
  31. 0031apply mod_eq_trans
  32. 0032exact hremb
  33. 0033exact hbx
  34. 0034have hrx : x2 = x
  35. 0035specialize mod_eq_bounded_unique m
  36. 0036specialize mod_eq_bounded_unique x2
  37. 0037specialize mod_eq_bounded_unique x
  38. 0038apply mod_eq_bounded_unique
  39. 0039exact hdiv_witness_witness_right
  40. 0040exact hx
  41. 0041exact hremx
  42. 0042exists x1
  43. 0043trans m * x1 + x2
  44. 0044exact hdiv_witness_witness_left
  45. 0045trans x1 * m + x2
  46. 0046congr
  47. 0047apply mul_comm
  48. 0048refl
  49. 0049congr
  50. 0050refl
  51. 0051exact hrx