BT00X1

six_block_window_decomposition_above_thirty_two

Alpha body-checked · checked-use disabled

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

Exact expanded PA statement

forall s. (exists bqb_le_gap_hjas_decomposition_source. bqb_le_gap_hjas_decomposition_source + (32) = (s)) -> exists b k. (((exists bqb_le_gap_hjas_decomposition_base_lower. bqb_le_gap_hjas_decomposition_base_lower + (32) = (b)) /\ (exists bqb_le_gap_hjas_decomposition_base_upper. bqb_le_gap_hjas_decomposition_base_upper + (b) = (37))) /\ s = b + 6 * k)

Structural proof guide

Every s>=32 is a six-step iterate of one base root in the exact window 32..37.

Direct prerequisites: division_remainder_exists, succ_ne_zero, le_of_succ_le_succ, le_add_right, add_le_add_left, add_assoc, add_comm. The authored body proceeds by case analysis (4), intermediate claims (4), equality transport (1), closed numeral normalization (1).

Proof neighborhood

Direct dependencies

BT001P division_remainder_exists BT000C succ_ne_zero BT0017 le_of_succ_le_succ BT0013 le_add_right BT0015 add_le_add_left BT0003 add_assoc BT0002 add_comm

Direct dependents

BT00X3 bertrand_hj_envelope_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 s
  2. 0002intro hsource
  3. 0003cases hsource
  4. 0004have hdivision : exists q r. x = 6 * q + r /\ exists h. h + S r = 6
  5. 0005specialize division_remainder_exists 6
  6. 0006specialize division_remainder_exists x
  7. 0007apply division_remainder_exists
  8. 0008intro hzero
  9. 0009specialize succ_ne_zero 5
  10. 0010apply succ_ne_zero
  11. 0011exact hzero
  12. 0012cases hdivision
  13. 0013cases hdivision_witness
  14. 0014cases hdivision_witness_witness
  15. 0015exists 32 + x2
  16. 0016exists x1
  17. 0017split
  18. 0018split
  19. 0019specialize le_add_right 32
  20. 0020specialize le_add_right x2
  21. 0021exact le_add_right
  22. 0022have hremainder : exists bqb_le_gap_hjas_decomposition_remainder_le. bqb_le_gap_hjas_decomposition_remainder_le + (x2) = (5)
  23. 0023specialize le_of_succ_le_succ x2
  24. 0024specialize le_of_succ_le_succ 5
  25. 0025apply le_of_succ_le_succ
  26. 0026exact hdivision_witness_witness_right
  27. 0027have hlifted : exists bqb_le_gap_hjas_decomposition_lifted_upper. bqb_le_gap_hjas_decomposition_lifted_upper + (32 + x2) = (32 + 5)
  28. 0028specialize add_le_add_left x2
  29. 0029specialize add_le_add_left 5
  30. 0030specialize add_le_add_left 32
  31. 0031apply add_le_add_left
  32. 0032exact hremainder
  33. 0033have hthirty_seven : 32 + 5 = 37
  34. 0034norm_num
  35. 0035rewrite hthirty_seven at hlifted
  36. 0036exact hlifted
  37. 0037trans x + 32
  38. 0038symm
  39. 0039exact hsource_witness
  40. 0040trans (6 * x1 + x2) + 32
  41. 0041congr
  42. 0042exact hdivision_witness_witness_left
  43. 0043refl
  44. 0044trans 6 * x1 + (x2 + 32)
  45. 0045specialize add_assoc (6 * x1)
  46. 0046specialize add_assoc x2
  47. 0047specialize add_assoc 32
  48. 0048apply add_assoc
  49. 0049trans 6 * x1 + (32 + x2)
  50. 0050congr
  51. 0051refl
  52. 0052specialize add_comm x2
  53. 0053specialize add_comm 32
  54. 0054apply add_comm
  55. 0055specialize add_comm (6 * x1)
  56. 0056specialize add_comm (32 + x2)
  57. 0057apply add_comm