theorem eSHP.table_8_prime_gap_test (p g : ℕ) (h : (p, g) ∈ table_8) (htest : p < 30) : prime_gap_record p g

theorem eSHP.table_8_prime_gap (p g : ℕ) (h : (p, g) ∈ table_8) : prime_gap_record p g

theorem eSHP.table_8_prime_gap_complete_test (p g : ℕ) (hp : p ≤ 30) (hrecord : prime_gap_record p g) : (p, g) ∈ table_8

theorem eSHP.table_8_prime_gap_complete (p g : ℕ) (hp : p ≤ 4 * 10 ^ 18) (hrecord : prime_gap_record p g) : (p, g) ∈ table_8

theorem eSHP.exists_prime_gap_record_le (n : ℕ) : ∃ (m : ℕ), nth_prime m ≤ nth_prime n ∧ nth_prime_gap n ≤ nth_prime_gap m ∧ prime_gap_record (nth_prime m) (nth_prime_gap m)

theorem eSHP.max_prime_gap (n : ℕ) (hp : nth_prime n ≤ 4 * 10 ^ 18) : nth_prime_gap n ≤ 1476

theorem eSHP.table_9_prime_gap_test (g P : ℕ) (h : (g, P) ∈ table_9) (htest : P < 30) : first_gap_record g P

theorem eSHP.table_9_prime_gap (g P : ℕ) (h : (g, P) ∈ table_9) : first_gap_record g P

theorem eSHP.table_9_prime_gap_complete_test (g P : ℕ) (hg : g < 8) (hg' : 0 < g) (hrecord : first_gap_record g P) : (g, P) ∈ table_9

theorem eSHP.table_9_prime_gap_complete (g P : ℕ) (hg : g < 1346) (hg' : 0 < g) (hrecord : first_gap_record g P) : (g, P) ∈ table_9

theorem eSHP.exists_prime_gap (g : ℕ) (hg : g ∈ Set.Ico 1 1476) (hg' : Even g ∨ g = 1) : first_gap g ≤ 3278018069102480227