BT00PS

bounded_prime_interval_search

Alpha body-checked · checked-use disabled

Bounded search returns a prime witness or an explicit prime-free interval certificate.

Exact expanded PA statement

forall l u. (exists bpi_value_search_witness. ((((~(bpi_value_search_witness = 1) /\ forall frm_prime_left_bpi_search_witness_interval_prime frm_prime_right_bpi_search_witness_interval_prime. bpi_value_search_witness = frm_prime_left_bpi_search_witness_interval_prime * frm_prime_right_bpi_search_witness_interval_prime -> frm_prime_left_bpi_search_witness_interval_prime = 1 \/ frm_prime_right_bpi_search_witness_interval_prime = 1)) /\ ((exists frm_gap_bpi_search_witness_interval_lower. frm_gap_bpi_search_witness_interval_lower + S l = bpi_value_search_witness) /\ (exists frm_weak_gap_bpi_search_witness_interval_upper. frm_weak_gap_bpi_search_witness_interval_upper + bpi_value_search_witness = u))))) \/ (forall bpi_value_search_exclusion. ((exists frm_gap_bpi_search_exclusion_lower. frm_gap_bpi_search_exclusion_lower + S l = bpi_value_search_exclusion) /\ (exists frm_weak_gap_bpi_search_exclusion_upper. frm_weak_gap_bpi_search_exclusion_upper + bpi_value_search_exclusion = u)) -> ~((~(bpi_value_search_exclusion = 1) /\ forall frm_prime_left_bpi_search_exclusion_prime frm_prime_right_bpi_search_exclusion_prime. bpi_value_search_exclusion = frm_prime_left_bpi_search_exclusion_prime * frm_prime_right_bpi_search_exclusion_prime -> frm_prime_left_bpi_search_exclusion_prime = 1 \/ frm_prime_right_bpi_search_exclusion_prime = 1)))

Structural proof guide

Bounded search returns a prime witness or an explicit prime-free interval certificate.

Direct prerequisites: prime_nonzero, le_zero, prime_strictly_above_decidable, le_refl, le_succ, le_eq_or_lt, le_of_succ_le_succ. The authored body proceeds by structural induction (1), case analysis (9), intermediate claims (2), equality transport (3).

Proof neighborhood

Direct dependencies

BT003G prime_nonzero BT000Y le_zero BT00PR prime_strictly_above_decidable BT000E le_refl BT0018 le_succ BT001C le_eq_or_lt BT0017 le_of_succ_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. 0001intro l
  2. 0002induction u
  3. 0003right
  4. 0004intro p
  5. 0005intro hbounds
  6. 0006cases hbounds
  7. 0007intro hp
  8. 0008specialize le_zero p
  9. 0009have hzero : p = 0
  10. 0010apply le_zero
  11. 0011exact hbounds_right
  12. 0012specialize prime_nonzero p
  13. 0013apply prime_nonzero
  14. 0014exact hp
  15. 0015exact hzero
  16. 0016specialize prime_strictly_above_decidable l
  17. 0017specialize prime_strictly_above_decidable (S u)
  18. 0018cases prime_strictly_above_decidable
  19. 0019left
  20. 0020exists S u
  21. 0021cases prime_strictly_above_decidable_left
  22. 0022split
  23. 0023exact prime_strictly_above_decidable_left_left
  24. 0024split
  25. 0025exact prime_strictly_above_decidable_left_right
  26. 0026specialize le_refl (S u)
  27. 0027exact le_refl
  28. 0028cases IH
  29. 0029left
  30. 0030cases IH_left
  31. 0031exists x
  32. 0032cases IH_left_witness
  33. 0033cases IH_left_witness_right
  34. 0034split
  35. 0035exact IH_left_witness_left
  36. 0036split
  37. 0037exact IH_left_witness_right_left
  38. 0038specialize le_succ x
  39. 0039specialize le_succ u
  40. 0040apply le_succ
  41. 0041exact IH_left_witness_right_right
  42. 0042right
  43. 0043intro p
  44. 0044intro hbounds
  45. 0045cases hbounds
  46. 0046intro hp
  47. 0047specialize le_eq_or_lt p
  48. 0048specialize le_eq_or_lt (S u)
  49. 0049have hsplit : p = S u \/ exists h. h + S p = S u
  50. 0050apply le_eq_or_lt
  51. 0051exact hbounds_right
  52. 0052cases hsplit
  53. 0053apply prime_strictly_above_decidable_right
  54. 0054split
  55. 0055rewrite hsplit_left at hp
  56. 0056rewrite hsplit_left at hp
  57. 0057exact hp
  58. 0058rewrite hsplit_left at hbounds_left
  59. 0059exact hbounds_left
  60. 0060specialize IH_right p
  61. 0061apply IH_right
  62. 0062split
  63. 0063exact hbounds_left
  64. 0064specialize le_of_succ_le_succ p
  65. 0065specialize le_of_succ_le_succ u
  66. 0066apply le_of_succ_le_succ
  67. 0067exact hsplit_right
  68. 0068exact hp