BT00RA

floor_sqrt_total

Alpha body-checked · checked-use disabled

Every natural lies in a constructively selected adjacent-square interval.

Exact expanded PA statement

forall x. exists s. (((exists bcs_sqrt_lower_gap_total_result. bcs_sqrt_lower_gap_total_result + (s) * (s) = (x)) /\ exists bcs_sqrt_upper_gap_total_result. bcs_sqrt_upper_gap_total_result + S (x) = S (s) * S (s)))

Structural proof guide

Every natural lies in a constructively selected adjacent-square interval.

Direct prerequisites: square_lt_successor_square, le_eq_or_lt, zero_add, le_succ. The authored body proceeds by structural induction (1), case analysis (3), intermediate claims (1), equality transport (1), closed numeral normalization (2).

Proof neighborhood

Direct dependencies

BT00R9 square_lt_successor_square BT001C le_eq_or_lt BT0000 zero_add BT0018 le_succ

Direct dependents

BT0115 bertrand_eventually_closed_upper

Formal native tactic body

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

  1. 0001induction x
  2. 0002exists 0
  3. 0003split
  4. 0004exists 0
  5. 0005norm_num
  6. 0006exists 0
  7. 0007norm_num
  8. 0008cases IH
  9. 0009cases IH_witness
  10. 0010have hsplit : S x = S x1 * S x1 \/ exists k. k + S (S x) = S x1 * S x1
  11. 0011specialize le_eq_or_lt (S x)
  12. 0012specialize le_eq_or_lt (S x1 * S x1)
  13. 0013apply le_eq_or_lt
  14. 0014exact IH_witness_right
  15. 0015cases hsplit
  16. 0016exists S x1
  17. 0017split
  18. 0018exists 0
  19. 0019trans S x1 * S x1
  20. 0020apply zero_add
  21. 0021symm
  22. 0022exact hsplit_left
  23. 0023specialize square_lt_successor_square (S x1)
  24. 0024rewrite hsplit_left
  25. 0025exact square_lt_successor_square
  26. 0026exists x1
  27. 0027split
  28. 0028specialize le_succ (x1 * x1)
  29. 0029specialize le_succ x
  30. 0030apply le_succ
  31. 0031exact IH_witness_left
  32. 0032exact hsplit_right