BT00RI

floor_ceil_complement_budget

Alpha body-checked · checked-use disabled

Floor-square and ceiling budgets imply e<=c and q+e<=n.

Exact expanded PA statement

forall n q s e c. (((exists bcs_sqrt_lower_gap_complement_bridge_floor. bcs_sqrt_lower_gap_complement_bridge_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_complement_bridge_floor. bcs_sqrt_upper_gap_complement_bridge_floor + S (2 * n) = S (s) * S (s))) -> (((exists bcs_lower_gap_complement_bridge_ceil. bcs_lower_gap_complement_bridge_ceil + (s * s) = 6 * (e)) /\ exists bcs_upper_gap_complement_bridge_ceil. bcs_upper_gap_complement_bridge_ceil + S (6 * (e)) = (s * s) + 6)) -> q + c = n -> (exists k. k + 2 * n = 6 * c) -> ((exists bqb_le_gap_complement_bridge_ec. bqb_le_gap_complement_bridge_ec + (e) = (c)) /\ (exists bqb_le_gap_complement_bridge_sum. bqb_le_gap_complement_bridge_sum + (q + e) = (n)))

Structural proof guide

Floor-square and ceiling budgets imply e<=c and q+e<=n.

Direct prerequisites: le_trans, ceil_div_six_le_of_upper, add_le_add_left. The authored body proceeds by case analysis (1), intermediate claims (3), equality transport (1).

Proof neighborhood

Direct dependencies

BT000F le_trans BT00RF ceil_div_six_le_of_upper BT0015 add_le_add_left

Direct dependents

BT00RJ floor_ceil_division_budget

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 s
  4. 0004intro e
  5. 0005intro c
  6. 0006intro hfloor
  7. 0007intro hceil
  8. 0008intro hcomp
  9. 0009intro hbudget
  10. 0010cases hfloor
  11. 0011have hsquare : exists k. k + s * s = 6 * c
  12. 0012specialize le_trans (s * s)
  13. 0013specialize le_trans (2 * n)
  14. 0014specialize le_trans (6 * c)
  15. 0015apply le_trans
  16. 0016exact hfloor_left
  17. 0017exact hbudget
  18. 0018have hec : exists k. k + e = c
  19. 0019specialize ceil_div_six_le_of_upper (s * s)
  20. 0020specialize ceil_div_six_le_of_upper e
  21. 0021specialize ceil_div_six_le_of_upper c
  22. 0022apply ceil_div_six_le_of_upper
  23. 0023exact hceil
  24. 0024exact hsquare
  25. 0025have hsum : exists k. k + (q + e) = q + c
  26. 0026specialize add_le_add_left e
  27. 0027specialize add_le_add_left c
  28. 0028specialize add_le_add_left q
  29. 0029apply add_le_add_left
  30. 0030exact hec
  31. 0031split
  32. 0032exact hec
  33. 0033rewrite <- hcomp
  34. 0034exact hsum