BT00U0

four_power_central_recurrence_step

Alpha body-checked · checked-use disabled

A weighted central recurrence equation advances the strict four-power lower bound.

Exact expanded PA statement

forall n q c d. (exists bcf_lt_gap_bfpcrs_source. bcf_lt_gap_bfpcrs_source + S (q) = n * c) -> S n * d = (2 * S (n + n)) * c -> (exists bcf_lt_gap_bfpcrs_result. bcf_lt_gap_bfpcrs_result + S (q * 4) = S n * d)

Structural proof guide

A weighted central recurrence equation advances the strict four-power lower bound.

Direct prerequisites: add_eq_zero_right, add_comm, mul_comm, mul_assoc, mul_add, add_mul, mul_lt_mul_right_nonzero, lt_trans. The authored body proceeds by case analysis (1), intermediate claims (7), equality transport (3), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT000L add_eq_zero_right BT0002 add_comm BT0006 mul_comm BT0008 mul_assoc BT0007 mul_add BT000B add_mul BT00TY mul_lt_mul_right_nonzero BT001F lt_trans

Direct dependents

BT00U4 four_pow_lt_mul_central_binom

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 q
  3. 0003intro c
  4. 0004intro d
  5. 0005intro hstrict
  6. 0006intro hrecurrence
  7. 0007have hc : ~(c = 0)
  8. 0008intro hc_zero
  9. 0009cases hstrict
  10. 0010apply PA1
  11. 0011specialize add_eq_zero_right x
  12. 0012specialize add_eq_zero_right (S q)
  13. 0013apply add_eq_zero_right
  14. 0014trans n * c
  15. 0015exact hstrict_witness
  16. 0016rewrite hc_zero
  17. 0017apply PA5
  18. 0018have hscaled : exists bcf_lt_gap_bfpcrs_scaled. bcf_lt_gap_bfpcrs_scaled + S (q * 4) = (n * c) * 4
  19. 0019specialize mul_lt_mul_right_nonzero q
  20. 0020specialize mul_lt_mul_right_nonzero (n * c)
  21. 0021specialize mul_lt_mul_right_nonzero 4
  22. 0022apply mul_lt_mul_right_nonzero
  23. 0023exact hstrict
  24. 0024intro hfour_zero
  25. 0025apply PA1
  26. 0026exact hfour_zero
  27. 0027have hfour : 4 * n = 2 * n + 2 * n
  28. 0028trans (2 + 2) * n
  29. 0029congr
  30. 0030norm_num
  31. 0031refl
  32. 0032apply add_mul
  33. 0033have hcoefficient : exists bcf_lt_gap_bfpcrs_coefficient. bcf_lt_gap_bfpcrs_coefficient + S (4 * n) = 2 * S (n + n)
  34. 0034exists 1
  35. 0035trans S (1 + 4 * n)
  36. 0036apply PA4
  37. 0037trans S (4 * n + 1)
  38. 0038congr
  39. 0039apply add_comm
  40. 0040trans 4 * n + 2
  41. 0041symm
  42. 0042apply PA4
  43. 0043trans (2 * n + 2 * n) + 2
  44. 0044congr
  45. 0045exact hfour
  46. 0046refl
  47. 0047trans 2 * (n + n) + 2
  48. 0048congr
  49. 0049symm
  50. 0050apply mul_add
  51. 0051refl
  52. 0052symm
  53. 0053apply PA6
  54. 0054have hcoefficient_product : exists bcf_lt_gap_bfpcrs_coefficient_product. bcf_lt_gap_bfpcrs_coefficient_product + S ((4 * n) * c) = (2 * S (n + n)) * c
  55. 0055specialize mul_lt_mul_right_nonzero (4 * n)
  56. 0056specialize mul_lt_mul_right_nonzero (2 * S (n + n))
  57. 0057specialize mul_lt_mul_right_nonzero c
  58. 0058apply mul_lt_mul_right_nonzero
  59. 0059exact hcoefficient
  60. 0060exact hc
  61. 0061have hshuffle : (n * c) * 4 = (4 * n) * c
  62. 0062trans 4 * (n * c)
  63. 0063apply mul_comm
  64. 0064symm
  65. 0065apply mul_assoc
  66. 0066have hgap : exists bcf_lt_gap_bfpcrs_gap. bcf_lt_gap_bfpcrs_gap + S ((n * c) * 4) = S n * d
  67. 0067rewrite hshuffle
  68. 0068rewrite hrecurrence
  69. 0069exact hcoefficient_product
  70. 0070specialize lt_trans (q * 4)
  71. 0071specialize lt_trans ((n * c) * 4)
  72. 0072specialize lt_trans (S n * d)
  73. 0073apply lt_trans
  74. 0074exact hscaled
  75. 0075exact hgap