BT010G

floor_sqrt_third_quotient_gap_exists

Alpha body-checked · checked-use disabled

The floor-root cut has an exact additive gap to the third quotient.

Exact expanded PA statement

forall n s q r. (exists bcf_lt_gap_b5rbfsltq_positive. bcf_lt_gap_b5rbfsltq_positive + S (2) = n) -> (((exists bcs_sqrt_lower_gap_b5rbfsltq_floor. bcs_sqrt_lower_gap_b5rbfsltq_floor + (s) * (s) = (n + n)) /\ exists bcs_sqrt_upper_gap_b5rbfsltq_floor. bcs_sqrt_upper_gap_b5rbfsltq_floor + S (n + n) = S (s) * S (s))) -> (((n + n) = (3) * (q) + (r) /\ (exists bcf_lt_gap_b5rbfsltq_division_bound. bcf_lt_gap_b5rbfsltq_division_bound + S (r) = 3))) -> exists g. s + g = q

Structural proof guide

The floor-root cut has an exact additive gap to the third quotient.

Direct prerequisites: add_comm, floor_sqrt_le_third_quotient. The authored body proceeds by case analysis (1), intermediate claims (1), equality transport (1).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT010F floor_sqrt_le_third_quotient

Direct dependents

BT010J floor_third_double_gap_package

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 s
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hpositive
  6. 0006intro hfloor
  7. 0007intro hdivision
  8. 0008have hbound : exists bcf_le_gap_b5rbfsltq_result. bcf_le_gap_b5rbfsltq_result + (s) = q
  9. 0009specialize floor_sqrt_le_third_quotient n
  10. 0010specialize floor_sqrt_le_third_quotient s
  11. 0011specialize floor_sqrt_le_third_quotient q
  12. 0012specialize floor_sqrt_le_third_quotient r
  13. 0013apply floor_sqrt_le_third_quotient
  14. 0014exact hpositive
  15. 0015exact hfloor
  16. 0016exact hdivision
  17. 0017cases hbound
  18. 0018exists x
  19. 0019specialize add_comm s
  20. 0020specialize add_comm x
  21. 0021rewrite add_comm
  22. 0022exact hbound_witness