BT00RC

floor_sqrt_monotone

Alpha body-checked · checked-use disabled

Witness order on inputs is transported monotonically to floor roots.

Exact expanded PA statement

forall x y s t. (((exists bcs_sqrt_lower_gap_monotone_left. bcs_sqrt_lower_gap_monotone_left + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_monotone_left. bcs_sqrt_upper_gap_monotone_left + S (x) = S (s) * S (s))) -> (((exists bcs_sqrt_lower_gap_monotone_right. bcs_sqrt_lower_gap_monotone_right + (t) * (t) = (y)) /\ exists bcs_sqrt_upper_gap_monotone_right. bcs_sqrt_upper_gap_monotone_right + S (y) = S (t) * S (t))) -> (exists k. k + x = y) -> exists k. k + s = t

Structural proof guide

Witness order on inputs is transported monotonically to floor roots.

Direct prerequisites: le_or_lt, mul_le_mul_right, mul_le_mul_left, le_trans, lt_of_lt_of_le, lt_not_le. The authored body proceeds by case analysis (3), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT001G le_or_lt BT001M mul_le_mul_right BT001L mul_le_mul_left BT000F le_trans BT001D lt_of_lt_of_le BT001I lt_not_le

Direct dependents

BT00X0 floor_sqrt_factorized_threshold_thirty_two

Formal native tactic body

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

  1. 0001intro x
  2. 0002intro y
  3. 0003intro s
  4. 0004intro t
  5. 0005intro hs
  6. 0006intro ht
  7. 0007intro hxy
  8. 0008cases hs
  9. 0009cases ht
  10. 0010specialize le_or_lt s
  11. 0011specialize le_or_lt t
  12. 0012cases le_or_lt
  13. 0013exact le_or_lt_left
  14. 0014exfalso
  15. 0015have hone : exists k. k + S t * S t = s * S t
  16. 0016apply mul_le_mul_right
  17. 0017exact le_or_lt_right
  18. 0018have htwo : exists k. k + s * S t = s * s
  19. 0019apply mul_le_mul_left
  20. 0020exact le_or_lt_right
  21. 0021have hsquare : exists k. k + S t * S t = s * s
  22. 0022specialize le_trans (S t * S t)
  23. 0023specialize le_trans (s * S t)
  24. 0024specialize le_trans (s * s)
  25. 0025apply le_trans
  26. 0026exact hone
  27. 0027exact htwo
  28. 0028have hsy : exists k. k + s * s = y
  29. 0029specialize le_trans (s * s)
  30. 0030specialize le_trans x
  31. 0031specialize le_trans y
  32. 0032apply le_trans
  33. 0033exact hs_left
  34. 0034exact hxy
  35. 0035have hylt : exists k. k + S y = s * s
  36. 0036specialize lt_of_lt_of_le y
  37. 0037specialize lt_of_lt_of_le (S t * S t)
  38. 0038specialize lt_of_lt_of_le (s * s)
  39. 0039apply lt_of_lt_of_le
  40. 0040exact ht_right
  41. 0041exact hsquare
  42. 0042specialize lt_not_le y
  43. 0043specialize lt_not_le (s * s)
  44. 0044apply lt_not_le
  45. 0045exact hylt
  46. 0046exact hsy