PA001K

gcd_balanced_bezout_exists_up_to

Stable checked-use theorem · independently closed

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

Exact expanded PA statement

forall B b. (exists t. t + b = B) -> forall a. exists d. ((((exists x. a = d * x) /\ (exists y. b = d * y)) /\ forall c. (exists u. a = c * u) -> (exists v. b = c * v) -> exists w. d = c * w) /\ exists xp yp xn yn. a * xp + b * yp = d + (a * xn + b * yn))

Structural proof guide

Generated structural guide

Bounded Euclidean descent simultaneously constructs a relational gcd and balanced natural Bezout witnesses.

Use the direct prerequisites zero_add, le_zero, le_eq_or_lt, le_of_succ_le_succ, division_remainder_exists, is_gcd_zero_right, is_gcd_euclid_forward, balanced_bezout_euclid_step as previously established PA formulas.

The proof proceeds by structural induction (1), case analysis (10), intermediate claims (9), equality transport (4), certified simplification (1).

Referenced ingredients

PA0001 zero_add PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001F is_gcd_zero_right PA001H is_gcd_euclid_forward PA001J balanced_bezout_euclid_step

Proof neighborhood

Direct dependencies

PA0001 zero_add PA001B le_zero PA000W le_eq_or_lt PA000V le_of_succ_le_succ PA001D division_remainder_exists PA001F is_gcd_zero_right PA001H is_gcd_euclid_forward PA001J balanced_bezout_euclid_step

Direct dependents

PA001L gcd_balanced_bezout_exists

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 B
  2. 0002induction B
  3. 0003intro b
  4. 0004intro hb
  5. 0005intro a
  6. 0006have hb0 : b = 0
  7. 0007apply le_zero
  8. 0008exact hb
  9. 0009exists a
  10. 0010split
  11. 0011rewrite hb0
  12. 0012rewrite hb0
  13. 0013specialize is_gcd_zero_right a
  14. 0014exact is_gcd_zero_right
  15. 0015exists 1
  16. 0016exists 0
  17. 0017exists 0
  18. 0018exists 0
  19. 0019rewrite hb0
  20. 0020simp [zero_add]
  21. 0021intro b
  22. 0022intro hb
  23. 0023intro a
  24. 0024specialize le_eq_or_lt b
  25. 0025specialize le_eq_or_lt (S B)
  26. 0026have hsplit : b = S B \/ exists k. k + S b = S B
  27. 0027apply le_eq_or_lt
  28. 0028exact hb
  29. 0029cases hsplit
  30. 0030have hb0 : ~(b = 0)
  31. 0031intro hzero
  32. 0032apply PA1
  33. 0033trans b
  34. 0034symm
  35. 0035exact hsplit_left
  36. 0036exact hzero
  37. 0037have hdiv : exists q r. a = b * q + r /\ exists k. k + S r = b
  38. 0038apply division_remainder_exists
  39. 0039exact hb0
  40. 0040cases hdiv
  41. 0041cases hdiv_witness
  42. 0042cases hdiv_witness_witness
  43. 0043have hrB : exists k. k + x1 = B
  44. 0044apply le_of_succ_le_succ
  45. 0045rewrite hsplit_left at hdiv_witness_witness_right
  46. 0046exact hdiv_witness_witness_right
  47. 0047have hsmall : exists d. ((((exists u. b = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. b = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. b * xp + x1 * yp = d + (b * xn + x1 * yn))
  48. 0048specialize IH x1
  49. 0049have hall : forall z. exists d. ((((exists u. z = d * u) /\ (exists v. x1 = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. x1 = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + x1 * yp = d + (z * xn + x1 * yn))
  50. 0050apply IH
  51. 0051exact hrB
  52. 0052specialize hall b
  53. 0053exact hall
  54. 0054cases hsmall
  55. 0055cases hsmall_witness
  56. 0056cases hsmall_witness_right
  57. 0057cases hsmall_witness_right_witness
  58. 0058cases hsmall_witness_right_witness_witness
  59. 0059cases hsmall_witness_right_witness_witness_witness
  60. 0060exists x2
  61. 0061split
  62. 0062apply is_gcd_euclid_forward
  63. 0063exact hdiv_witness_witness_left
  64. 0064exact hsmall_witness_left
  65. 0065exists x4
  66. 0066exists x3 + x * x6
  67. 0067exists x6
  68. 0068exists x5 + x * x4
  69. 0069apply balanced_bezout_euclid_step
  70. 0070exact hdiv_witness_witness_left
  71. 0071exact hsmall_witness_right_witness_witness_witness_witness
  72. 0072have hbB : exists k. k + b = B
  73. 0073apply le_of_succ_le_succ
  74. 0074exact hsplit_right
  75. 0075specialize IH b
  76. 0076have hall : forall z. exists d. ((((exists u. z = d * u) /\ (exists v. b = d * v)) /\ forall c. (exists s. z = c * s) -> (exists t. b = c * t) -> exists w. d = c * w) /\ exists xp yp xn yn. z * xp + b * yp = d + (z * xn + b * yn))
  77. 0077apply IH
  78. 0078exact hbB
  79. 0079specialize hall a
  80. 0080exact hall