BT00X0

floor_sqrt_factorized_threshold_thirty_two

Alpha body-checked · checked-use disabled

The factorized large-input threshold forces every selected root to be at least 32.

Exact expanded PA statement

forall n s. (exists bqb_le_gap_hjas_threshold_input. bqb_le_gap_hjas_threshold_input + (16 * 32) = (n)) -> (((exists bcs_sqrt_lower_gap_hjas_threshold_floor. bcs_sqrt_lower_gap_hjas_threshold_floor + (s) * (s) = (2 * n)) /\ exists bcs_sqrt_upper_gap_hjas_threshold_floor. bcs_sqrt_upper_gap_hjas_threshold_floor + S (2 * n) = S (s) * S (s))) -> (exists bqb_le_gap_hjas_threshold_result. bqb_le_gap_hjas_threshold_result + (32) = (s))

Structural proof guide

The factorized large-input threshold forces every selected root to be at least 32.

Direct prerequisites: thirty_two_square_eq_twice_sixteen_times_thirty_two, zero_add, square_lt_successor_square, mul_le_mul_left, floor_sqrt_monotone. The authored body proceeds by intermediate claims (2), equality transport (1).

Proof neighborhood

Direct dependencies

BT00WY thirty_two_square_eq_twice_sixteen_times_thirty_two BT0000 zero_add BT00R9 square_lt_successor_square BT001L mul_le_mul_left BT00RC floor_sqrt_monotone

Direct dependents

BT00X6 bertrand_main_inequality_factorized_from_total

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 hthreshold
  4. 0004intro hfloor
  5. 0005have hbase : ((exists bcs_sqrt_lower_gap_hjas_threshold_base_floor. bcs_sqrt_lower_gap_hjas_threshold_base_floor + (32) * (32) = (2 * (16 * 32))) /\ exists bcs_sqrt_upper_gap_hjas_threshold_base_floor. bcs_sqrt_upper_gap_hjas_threshold_base_floor + S (2 * (16 * 32)) = S (32) * S (32))
  6. 0006split
  7. 0007exists 0
  8. 0008trans 32 * 32
  9. 0009apply zero_add
  10. 0010exact thirty_two_square_eq_twice_sixteen_times_thirty_two
  11. 0011specialize square_lt_successor_square 32
  12. 0012rewrite thirty_two_square_eq_twice_sixteen_times_thirty_two at square_lt_successor_square
  13. 0013exact square_lt_successor_square
  14. 0014have hscaled : exists bqb_le_gap_hjas_threshold_scaled. bqb_le_gap_hjas_threshold_scaled + (2 * (16 * 32)) = (2 * n)
  15. 0015specialize mul_le_mul_left (16 * 32)
  16. 0016specialize mul_le_mul_left n
  17. 0017specialize mul_le_mul_left 2
  18. 0018apply mul_le_mul_left
  19. 0019exact hthreshold
  20. 0020specialize floor_sqrt_monotone (2 * (16 * 32))
  21. 0021specialize floor_sqrt_monotone (2 * n)
  22. 0022specialize floor_sqrt_monotone 32
  23. 0023specialize floor_sqrt_monotone s
  24. 0024apply floor_sqrt_monotone
  25. 0025exact hbase
  26. 0026exact hfloor
  27. 0027exact hscaled