BT003F

prime_or_composite

Stable checked-use theorem · independently kernel verified

Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.

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 n. ~(n = 0) -> ~(n = 1) -> ((~(n = 1) /\ forall a b. n = a * b -> a = 1 \/ b = 1) \/ exists c d. ((~(c = 1) /\ ~(d = 1)) /\ n = c * d))

Structural proof guide

Every nonzero nonunit natural is constructively prime or has a nontrivial factor pair.

Direct prerequisites: divisor_le_nonzero, factor_search_up_to. The authored body proceeds by case analysis (6), intermediate claims (1).

Proof neighborhood

Direct dependencies

BT002D divisor_le_nonzero BT003E factor_search_up_to

Direct dependents

BT003H prime_decidable BT003K prime_divisor_exists_up_to BT0118 nonprime_has_small_prime_divisor_below_square

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

38 script commands · 13 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)
divisor le nonzerofactor search up to
01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hn0
  3. L3
    intro hn1
02Use earlier factsL4–5

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

  1. L4
    specialize factor_search_up_to n
  2. L5
    specialize factor_search_up_to n
03Establish hsearchL6–8

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply factor search up to.

  1. L6
    have hsearch : (forall c d. (exists k. k + c = n) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = n) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d)
  2. L7
    apply factor_search_up_to
  3. L8
    exact hn0
04Separate the logical casesL9–11

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

  1. L9
    cases hsearch
  2. L10
    left
  3. L11
    split
05Use earlier factsL12–12

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

  1. L12
    exact hn1
06Fix variables and assumptionsL13–15

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

  1. L13
    intro c
  2. L14
    intro d
  3. L15
    intro hfac
07Use earlier factsL16–22

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

  1. L16
    specialize hsearch_left c
  2. L17
    specialize hsearch_left d
  3. L18
    apply hsearch_left
  4. L19
    specialize divisor_le_nonzero c
  5. L20
    specialize divisor_le_nonzero n
  6. L21
    apply divisor_le_nonzero
  7. L22
    exact hn0
08Construct an explicit witnessL23–23

Supply the displayed value, then prove that it has the required property.

  1. L23
    exists d
09Use earlier factsL24–25

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

  1. L24
    exact hfac
  2. L25
    exact hfac
10Separate the logical casesL26–31

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

  1. L26
    right
  2. L27
    cases hsearch_right
  3. L28
    cases hsearch_right_witness
  4. L29
    cases hsearch_right_witness_witness
  5. L30
    cases hsearch_right_witness_witness_left
  6. L31
    cases hsearch_right_witness_witness_left_left
11Construct an explicit witnessL32–33

Supply the displayed value, then prove that it has the required property.

  1. L32
    exists x
  2. L33
    exists x1
12Separate the logical casesL34–35

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

  1. L34
    split
  2. L35
    split
13Use earlier factsL36–38

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

  1. L36
    exact hsearch_right_witness_witness_left_left_right
  2. L37
    exact hsearch_right_witness_witness_left_right
  3. L38
    exact hsearch_right_witness_witness_right

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro n
  2. 0002intro hn0
  3. 0003intro hn1
  4. 0004specialize factor_search_up_to n
  5. 0005specialize factor_search_up_to n
  6. 0006have hsearch : (forall c d. (exists k. k + c = n) -> n = c * d -> c = 1 \/ d = 1) \/ exists c d. ((((exists k. k + c = n) /\ ~(c = 1)) /\ ~(d = 1)) /\ n = c * d)
  7. 0007apply factor_search_up_to
  8. 0008exact hn0
  9. 0009cases hsearch
  10. 0010left
  11. 0011split
  12. 0012exact hn1
  13. 0013intro c
  14. 0014intro d
  15. 0015intro hfac
  16. 0016specialize hsearch_left c
  17. 0017specialize hsearch_left d
  18. 0018apply hsearch_left
  19. 0019specialize divisor_le_nonzero c
  20. 0020specialize divisor_le_nonzero n
  21. 0021apply divisor_le_nonzero
  22. 0022exact hn0
  23. 0023exists d
  24. 0024exact hfac
  25. 0025exact hfac
  26. 0026right
  27. 0027cases hsearch_right
  28. 0028cases hsearch_right_witness
  29. 0029cases hsearch_right_witness_witness
  30. 0030cases hsearch_right_witness_witness_left
  31. 0031cases hsearch_right_witness_witness_left_left
  32. 0032exists x
  33. 0033exists x1
  34. 0034split
  35. 0035split
  36. 0036exact hsearch_right_witness_witness_left_left_right
  37. 0037exact hsearch_right_witness_witness_left_right
  38. 0038exact hsearch_right_witness_witness_right