BT00VK

central_binom_strong_upper_step

Alpha body-checked · checked-use disabled

The weighted recurrence preserves the strong factor-two bound.

Exact expanded PA statement

forall n c d q r. (exists bcf_le_gap_bcbsus_source. bcf_le_gap_bcbsus_source + (2 * c) = q) -> S n * d = (2 * S (n + n)) * c -> r = q * 4 -> (exists bcf_le_gap_bcbsus_result. bcf_le_gap_bcbsus_result + (2 * d) = r)

Structural proof guide

The weighted recurrence preserves the strong factor-two bound.

Direct prerequisites: zero_add, add_succ_left, add_assoc, mul_comm, mul_assoc, two_mul_eq_add_self, mul_le_mul_left, mul_le_mul_right, le_trans, succ_ne_zero, mul_le_cancel_left_nonzero. The authored body proceeds by intermediate claims (11), equality transport (13), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left BT0003 add_assoc BT0006 mul_comm BT0008 mul_assoc BT00QU two_mul_eq_add_self BT001L mul_le_mul_left BT001M mul_le_mul_right BT000F le_trans BT000C succ_ne_zero BT00RD mul_le_cancel_left_nonzero

Direct dependents

BT00VM central_binom_strong_upper_of_laws

Formal native tactic body

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

  1. 0001intro n
  2. 0002intro c
  3. 0003intro d
  4. 0004intro q
  5. 0005intro r
  6. 0006intro hsource
  7. 0007intro hrecurrence
  8. 0008intro hpower_step
  9. 0009have hsource_scaled : exists k. k + S (n + n) * (2 * c) = S (n + n) * q
  10. 0010specialize mul_le_mul_left (2 * c)
  11. 0011specialize mul_le_mul_left q
  12. 0012specialize mul_le_mul_left (S (n + n))
  13. 0013apply mul_le_mul_left
  14. 0014exact hsource
  15. 0015have hcombined : exists k. k + S (n + n) * (2 * c) = (2 * S n) * q
  16. 0016specialize le_trans (S (n + n) * (2 * c))
  17. 0017specialize le_trans (S (n + n) * q)
  18. 0018specialize le_trans ((2 * S n) * q)
  19. 0019apply le_trans
  20. 0020exact hsource_scaled
  21. 0021specialize mul_le_mul_right (S (n + n))
  22. 0022specialize mul_le_mul_right (2 * S n)
  23. 0023specialize mul_le_mul_right q
  24. 0024apply mul_le_mul_right
  25. 0025exists 1
  26. 0026specialize two_mul_eq_add_self (S n)
  27. 0027rewrite two_mul_eq_add_self
  28. 0028rewrite PA4
  29. 0029rewrite PA4
  30. 0030specialize add_assoc 1
  31. 0031specialize add_assoc n
  32. 0032specialize add_assoc n
  33. 0033rewrite <- add_assoc
  34. 0034specialize add_succ_left 0
  35. 0035specialize add_succ_left n
  36. 0036rewrite add_succ_left
  37. 0037specialize zero_add n
  38. 0038rewrite zero_add
  39. 0039refl
  40. 0040have hleft_align : (2 * S (n + n)) * c = S (n + n) * (2 * c)
  41. 0041trans 2 * (S (n + n) * c)
  42. 0042apply mul_assoc
  43. 0043trans (S (n + n) * c) * 2
  44. 0044apply mul_comm
  45. 0045trans S (n + n) * (c * 2)
  46. 0046apply mul_assoc
  47. 0047have hcomm_c_two : c * 2 = 2 * c
  48. 0048apply mul_comm
  49. 0049rewrite hcomm_c_two
  50. 0050refl
  51. 0051have hrecurrence_aligned : S n * d = S (n + n) * (2 * c)
  52. 0052trans (2 * S (n + n)) * c
  53. 0053exact hrecurrence
  54. 0054exact hleft_align
  55. 0055have hright_align : (2 * S n) * q = S n * (2 * q)
  56. 0056trans 2 * (S n * q)
  57. 0057apply mul_assoc
  58. 0058trans (S n * q) * 2
  59. 0059apply mul_comm
  60. 0060trans S n * (q * 2)
  61. 0061apply mul_assoc
  62. 0062have hcomm_q_two : q * 2 = 2 * q
  63. 0063apply mul_comm
  64. 0064rewrite hcomm_q_two
  65. 0065refl
  66. 0066rewrite <- hrecurrence_aligned at hcombined
  67. 0067rewrite hright_align at hcombined
  68. 0068have hhalf : exists k. k + d = 2 * q
  69. 0069specialize mul_le_cancel_left_nonzero (S n)
  70. 0070specialize mul_le_cancel_left_nonzero d
  71. 0071specialize mul_le_cancel_left_nonzero (2 * q)
  72. 0072apply mul_le_cancel_left_nonzero
  73. 0073specialize succ_ne_zero n
  74. 0074exact succ_ne_zero
  75. 0075exact hcombined
  76. 0076have hdouble : exists k. k + 2 * d = 2 * (2 * q)
  77. 0077specialize mul_le_mul_left d
  78. 0078specialize mul_le_mul_left (2 * q)
  79. 0079specialize mul_le_mul_left 2
  80. 0080apply mul_le_mul_left
  81. 0081exact hhalf
  82. 0082have hfour : 2 * (2 * q) = q * 4
  83. 0083trans (2 * 2) * q
  84. 0084symm
  85. 0085apply mul_assoc
  86. 0086trans 4 * q
  87. 0087have htwo_two : 2 * 2 = 4
  88. 0088norm_num
  89. 0089rewrite htwo_two
  90. 0090refl
  91. 0091apply mul_comm
  92. 0092rewrite hfour at hdouble
  93. 0093rewrite hpower_step
  94. 0094exact hdouble