BT010J

floor_third_double_gap_package

Alpha body-checked · checked-use disabled

Package the two exact additive gaps used by the three-range split.

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 h. s + g = q /\ q + h = n + n

Structural proof guide

Package the two exact additive gaps used by the three-range split.

Direct prerequisites: floor_sqrt_third_quotient_gap_exists, third_quotient_double_gap_exists. The authored body proceeds by case analysis (2), intermediate claims (2).

Proof neighborhood

Direct dependencies

BT010G floor_sqrt_third_quotient_gap_exists BT010I third_quotient_double_gap_exists

Direct dependents

BT0114 central_binom_le_of_no_bertrand_prime

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 hfirst : exists g. s + g = q
  9. 0009specialize floor_sqrt_third_quotient_gap_exists n
  10. 0010specialize floor_sqrt_third_quotient_gap_exists s
  11. 0011specialize floor_sqrt_third_quotient_gap_exists q
  12. 0012specialize floor_sqrt_third_quotient_gap_exists r
  13. 0013apply floor_sqrt_third_quotient_gap_exists
  14. 0014exact hpositive
  15. 0015exact hfloor
  16. 0016exact hdivision
  17. 0017cases hfirst
  18. 0018have hsecond : exists h. q + h = n + n
  19. 0019specialize third_quotient_double_gap_exists n
  20. 0020specialize third_quotient_double_gap_exists q
  21. 0021specialize third_quotient_double_gap_exists r
  22. 0022apply third_quotient_double_gap_exists
  23. 0023exact hdivision
  24. 0024cases hsecond
  25. 0025exists x
  26. 0026exists x1
  27. 0027split
  28. 0028exact hfirst_witness
  29. 0029exact hsecond_witness