BT00W7

linear_square_budget

Alpha body-checked · checked-use disabled

A factorized linear budget lies below a square by an explicit gap.

Exact expanded PA statement

forall a q r t c k d. r = a * q + t -> k = q * r + c -> d + a * c = t * r -> (exists bqb_le_gap_hj32_linear_square_budget. bqb_le_gap_hj32_linear_square_budget + (a * k) = (r * r))

Structural proof guide

A factorized linear budget lies below a square by an explicit gap.

Direct prerequisites: mul_add, mul_assoc, add_assoc, add_comm, add_mul. The authored body proceeds by intermediate claims (8), equality transport (11).

Proof neighborhood

Direct dependencies

BT0007 mul_add BT0008 mul_assoc BT0003 add_assoc BT0002 add_comm BT000B add_mul

Direct dependents

BT00W8 bertrand_scaled_budget_root_32 BT00W9 bertrand_scaled_budget_root_33 BT00WA bertrand_scaled_budget_root_34 BT00WB bertrand_scaled_budget_root_35 BT00WC bertrand_scaled_budget_root_36 BT00WD bertrand_scaled_budget_root_37

Formal native tactic body

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

  1. 0001intro a
  2. 0002intro q
  3. 0003intro r
  4. 0004intro t
  5. 0005intro c
  6. 0006intro k
  7. 0007intro d
  8. 0008intro hr
  9. 0009intro hk
  10. 0010intro hd
  11. 0011exists d
  12. 0012rewrite hk
  13. 0013have hmul_add : a * (q * r + c) = a * (q * r) + a * c
  14. 0014specialize mul_add a
  15. 0015specialize mul_add (q * r)
  16. 0016specialize mul_add c
  17. 0017apply mul_add
  18. 0018rewrite hmul_add
  19. 0019have hassoc_one : d + (a * (q * r) + a * c) = (d + a * (q * r)) + a * c
  20. 0020symm
  21. 0021specialize add_assoc d
  22. 0022specialize add_assoc (a * (q * r))
  23. 0023specialize add_assoc (a * c)
  24. 0024apply add_assoc
  25. 0025rewrite hassoc_one
  26. 0026have hcomm_one : d + a * (q * r) = a * (q * r) + d
  27. 0027specialize add_comm d
  28. 0028specialize add_comm (a * (q * r))
  29. 0029apply add_comm
  30. 0030rewrite hcomm_one
  31. 0031have hassoc_two : (a * (q * r) + d) + a * c = a * (q * r) + (d + a * c)
  32. 0032specialize add_assoc (a * (q * r))
  33. 0033specialize add_assoc d
  34. 0034specialize add_assoc (a * c)
  35. 0035apply add_assoc
  36. 0036rewrite hassoc_two
  37. 0037have hcomm_two : a * (q * r) + (d + a * c) = (d + a * c) + a * (q * r)
  38. 0038specialize add_comm (a * (q * r))
  39. 0039specialize add_comm (d + a * c)
  40. 0040apply add_comm
  41. 0041rewrite hcomm_two
  42. 0042rewrite hd
  43. 0043have hmul_assoc : (a * q) * r = a * (q * r)
  44. 0044specialize mul_assoc a
  45. 0045specialize mul_assoc q
  46. 0046specialize mul_assoc r
  47. 0047apply mul_assoc
  48. 0048rewrite <- hmul_assoc
  49. 0049have hadd_mul : (t + a * q) * r = t * r + (a * q) * r
  50. 0050specialize add_mul t
  51. 0051specialize add_mul (a * q)
  52. 0052specialize add_mul r
  53. 0053apply add_mul
  54. 0054rewrite <- hadd_mul
  55. 0055have hcomm_three : t + a * q = a * q + t
  56. 0056specialize add_comm t
  57. 0057specialize add_comm (a * q)
  58. 0058apply add_comm
  59. 0059rewrite hcomm_three
  60. 0060rewrite <- hr
  61. 0061refl