TS0020

prime_is_two_or_odd

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

Every prime is constructively either the exceptional prime two or an odd number.

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 first-order arithmetic statement

forall p. ((~(p = 1) /\ forall frm_prime_left_ftsc_prime frm_prime_right_ftsc_prime. p = frm_prime_left_ftsc_prime * frm_prime_right_ftsc_prime -> frm_prime_left_ftsc_prime = 1 \/ frm_prime_right_ftsc_prime = 1)) -> (p = 2 \/ (exists ftsc_odd_ftsc_prime. (p) = 2 * ftsc_odd_ftsc_prime + 1))

Constructive proof overview

Generated structural guide

Every prime is constructively either the exceptional prime two or an odd number.

The unchanged tactic script uses 2 declared prerequisites and contains 26 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

parity_cases Stable theorem; checked-use authorized mul_one Stable theorem; checked-use authorized

Direct dependents

TS0021 prime_mod_four_trichotomy

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

26 script commands · 10 reading checkpoints · 2 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.

01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hprime
02Separate the logical casesL3–3

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

  1. L3
    cases hprime
03Use earlier factsL4–4

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

  1. L4
    specialize parity_cases p
04Separate the logical casesL5–7

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

  1. L5
    cases parity_cases
  2. L6
    cases parity_cases_witness
  3. L7
    left
05Establish hfactorL8–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hprime right.

  1. L8
    have hfactor : 2 = 1 \/ x = 1
  2. L9
    specialize hprime_right 2
  3. L10
    specialize hprime_right x
  4. L11
    apply hprime_right
  5. L12
    exact parity_cases_witness_left
06Separate the logical casesL13–14

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

  1. L13
    cases hfactor
  2. L14
    exfalso
07Establish hzeroL15–23

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply PA2.

  1. L15
    have hzero : 1 = 0
  2. L16
    apply PA2
  3. L17
    exact hfactor_left
  4. L18
    apply PA1
  5. L19
    exact hzero
  6. L20
    rewrite hfactor_right at parity_cases_witness_left
  7. L21
    specialize mul_one 2
  8. L22
    rewrite mul_one at parity_cases_witness_left
  9. L23
    exact parity_cases_witness_left
08Separate the logical casesL24–24

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

  1. L24
    right
09Construct an explicit witnessL25–25

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

  1. L25
    exists x
10Use earlier factsL26–26

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

  1. L26
    exact parity_cases_witness_right

Library-wide reading audit

Original exact command ledger · 26 lines
  1. 0001intro p
  2. 0002intro hprime
  3. 0003cases hprime
  4. 0004specialize parity_cases p
  5. 0005cases parity_cases
  6. 0006cases parity_cases_witness
  7. 0007left
  8. 0008have hfactor : 2 = 1 \/ x = 1
  9. 0009specialize hprime_right 2
  10. 0010specialize hprime_right x
  11. 0011apply hprime_right
  12. 0012exact parity_cases_witness_left
  13. 0013cases hfactor
  14. 0014exfalso
  15. 0015have hzero : 1 = 0
  16. 0016apply PA2
  17. 0017exact hfactor_left
  18. 0018apply PA1
  19. 0019exact hzero
  20. 0020rewrite hfactor_right at parity_cases_witness_left
  21. 0021specialize mul_one 2
  22. 0022rewrite mul_one at parity_cases_witness_left
  23. 0023exact parity_cases_witness_left
  24. 0024right
  25. 0025exists x
  26. 0026exact parity_cases_witness_right