BT0119

prime_of_no_small_prime_divisor_below_square

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

Trial division by primes through B certifies numbers below (B+1)^2.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall B n. ~(n = 0) -> ~(n = 1) -> (exists bpr_gap_bb8pnsp_square. bpr_gap_bb8pnsp_square + S (n) = S B * S B) -> (forall p. ((~(p = 1) /\ forall bpr_left_bb8pnsp_prime bpr_right_bb8pnsp_prime. p = bpr_left_bb8pnsp_prime * bpr_right_bb8pnsp_prime -> bpr_left_bb8pnsp_prime = 1 \/ bpr_right_bb8pnsp_prime = 1)) -> (exists bpr_le_gap_bb8pnsp_bound. bpr_le_gap_bb8pnsp_bound + (p) = (B)) -> ~(exists bpr_quotient_bb8pnsp_divides. n = (p) * bpr_quotient_bb8pnsp_divides)) -> ((~(n = 1) /\ forall bpr_left_bb8pnsp_result bpr_right_bb8pnsp_result. n = bpr_left_bb8pnsp_result * bpr_right_bb8pnsp_result -> bpr_left_bb8pnsp_result = 1 \/ bpr_right_bb8pnsp_result = 1))

Structural proof guide

Trial division by primes through B certifies numbers below (B+1)^2.

Direct prerequisites: prime_decidable, nonprime_has_small_prime_divisor_below_square. The authored body proceeds by case analysis (4), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT003H prime_decidable BT0118 nonprime_has_small_prime_divisor_below_square

Direct dependents

BT011F prime_five BT011G prime_seven BT011H prime_thirteen BT011I prime_twenty_three BT011J prime_forty_three BT011K prime_eighty_three BT011L prime_one_hundred_sixty_three BT011M prime_three_hundred_seventeen BT011N prime_five_hundred_twenty_one

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

26 script commands · 8 reading checkpoints · 1 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

Named ingredients (2)
prime decidablenonprime has small prime divisor below square
01Fix variables and assumptionsL1–6

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro B
  2. L2
    intro n
  3. L3
    intro hn0
  4. L4
    intro hn1
  5. L5
    intro hsquare
  6. L6
    intro hexclude
02Use earlier factsL7–7

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L7
    specialize prime_decidable n
03Separate the logical casesL8–8

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L8
    cases prime_decidable
04Use earlier factsL9–9

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    exact prime_decidable_left
05Separate the logical casesL10–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    exfalso
06Establish hpL11–18

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply nonprime has small prime divisor below square.

  1. L11
    have hp : exists p. ((~(p = 1) /\ forall bpr_left_bb8npsp_prime bpr_right_bb8npsp_prime. p = bpr_left_bb8npsp_prime * bpr_right_bb8npsp_prime -> bpr_left_bb8npsp_prime = 1 \/ bpr_right_bb8npsp_prime = 1)) /\ ((exists bpr_le_gap_bb8npsp_bound. bpr_le_gap_bb8npsp_bound + (p) = (B)) /\ (exists bpr_quotient_bb8npsp_divides. n = (p) * bpr_quotient_bb8npsp_divides))
  2. L12
    specialize nonprime_has_small_prime_divisor_below_square B
  3. L13
    specialize nonprime_has_small_prime_divisor_below_square n
  4. L14
    apply nonprime_has_small_prime_divisor_below_square
  5. L15
    exact hn0
  6. L16
    exact hn1
  7. L17
    exact hsquare
  8. L18
    exact prime_decidable_right
07Separate the logical casesL19–21

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L19
    cases hp
  2. L20
    cases hp_witness
  3. L21
    cases hp_witness_right
08Use earlier factsL22–26

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L22
    specialize hexclude x
  2. L23
    apply hexclude
  3. L24
    exact hp_witness_left
  4. L25
    exact hp_witness_right_left
  5. L26
    exact hp_witness_right_right

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro B
  2. 0002intro n
  3. 0003intro hn0
  4. 0004intro hn1
  5. 0005intro hsquare
  6. 0006intro hexclude
  7. 0007specialize prime_decidable n
  8. 0008cases prime_decidable
  9. 0009exact prime_decidable_left
  10. 0010exfalso
  11. 0011have hp : exists p. ((~(p = 1) /\ forall bpr_left_bb8npsp_prime bpr_right_bb8npsp_prime. p = bpr_left_bb8npsp_prime * bpr_right_bb8npsp_prime -> bpr_left_bb8npsp_prime = 1 \/ bpr_right_bb8npsp_prime = 1)) /\ ((exists bpr_le_gap_bb8npsp_bound. bpr_le_gap_bb8npsp_bound + (p) = (B)) /\ (exists bpr_quotient_bb8npsp_divides. n = (p) * bpr_quotient_bb8npsp_divides))
  12. 0012specialize nonprime_has_small_prime_divisor_below_square B
  13. 0013specialize nonprime_has_small_prime_divisor_below_square n
  14. 0014apply nonprime_has_small_prime_divisor_below_square
  15. 0015exact hn0
  16. 0016exact hn1
  17. 0017exact hsquare
  18. 0018exact prime_decidable_right
  19. 0019cases hp
  20. 0020cases hp_witness
  21. 0021cases hp_witness_right
  22. 0022specialize hexclude x
  23. 0023apply hexclude
  24. 0024exact hp_witness_left
  25. 0025exact hp_witness_right_left
  26. 0026exact hp_witness_right_right