PC0032

prime_bit_choice_functional

The primality indicator is uniquely zero or one, without a classical principle.

Alpha v34 checked-use · first admitted v27 · independently kernel and Lean verified; not Stable

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.

These are the exact finite integer inequalities with constant 8, for every N≥2. The proof uses constructive binomial and primorial infrastructure; it does not assume logarithms, asymptotic estimates, the prime number theorem, or a factorization oracle.

Exact theorem in conservative defined notation

∀ i. ∀ e. ∀ f. Prime(S i) ∧ e = 1 ∨ ¬Prime(S i) ∧ e = 0 → Prime(S i) ∧ f = 1 ∨ ¬Prime(S i) ∧ f = 0 → e = f

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Prime(p) · 4

Actual proof prerequisites

none
Original expanded first-order statement 
forall i e f. (((((~(S (i) = 1) /\ forall bpr_left_pc_choice_functional_left_prime bpr_right_pc_choice_functional_left_prime. S (i) = bpr_left_pc_choice_functional_left_prime * bpr_right_pc_choice_functional_left_prime -> bpr_left_pc_choice_functional_left_prime = 1 \/ bpr_right_pc_choice_functional_left_prime = 1)) /\ e = 1) \/ (~((~(S (i) = 1) /\ forall bpr_left_pc_choice_functional_left_prime bpr_right_pc_choice_functional_left_prime. S (i) = bpr_left_pc_choice_functional_left_prime * bpr_right_pc_choice_functional_left_prime -> bpr_left_pc_choice_functional_left_prime = 1 \/ bpr_right_pc_choice_functional_left_prime = 1)) /\ e = 0))) -> (((((~(S (i) = 1) /\ forall bpr_left_pc_choice_functional_right_prime bpr_right_pc_choice_functional_right_prime. S (i) = bpr_left_pc_choice_functional_right_prime * bpr_right_pc_choice_functional_right_prime -> bpr_left_pc_choice_functional_right_prime = 1 \/ bpr_right_pc_choice_functional_right_prime = 1)) /\ f = 1) \/ (~((~(S (i) = 1) /\ forall bpr_left_pc_choice_functional_right_prime bpr_right_pc_choice_functional_right_prime. S (i) = bpr_left_pc_choice_functional_right_prime * bpr_right_pc_choice_functional_right_prime -> bpr_left_pc_choice_functional_right_prime = 1 \/ bpr_right_pc_choice_functional_right_prime = 1)) /\ f = 0))) -> e = f

Complete tactic proof in conservative notation

All 28 original proof lines are preserved. Only local proposition formulas are abbreviated; every abbreviation has an exact binder-safe expansion check. The linked exact edition contains the unchanged replay script.

Read the argument

Proof checkpoints

28 script commands · 15 reading checkpoints · 0 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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

01Fix variables and assumptionsL1–5

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

  1. L1
    intro i
  2. L2
    intro e
  3. L3
    intro f
  4. L4
    intro he
  5. L5
    intro hf
02Separate the logical casesL6–9

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

  1. L6
    cases he
  2. L7
    cases he_left
  3. L8
    cases hf
  4. L9
    cases hf_left
03Calculate and transport equalitiesL10–10

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L10
    trans 1
04Use earlier factsL11–11

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

  1. L11
    exact he_left_right
05Calculate and transport equalitiesL12–12

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L12
    symm
06Use earlier factsL13–13

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

  1. L13
    exact hf_left_right
07Separate the logical casesL14–15

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

  1. L14
    cases hf_right
  2. L15
    exfalso
08Use earlier factsL16–17

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

  1. L16
    apply hf_right_left
  2. L17
    exact he_left_left
09Separate the logical casesL18–21

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

  1. L18
    cases he_right
  2. L19
    cases hf
  3. L20
    cases hf_left
  4. L21
    exfalso
10Use earlier factsL22–23

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

  1. L22
    apply he_right_left
  2. L23
    exact hf_left_left
11Separate the logical casesL24–24

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

  1. L24
    cases hf_right
12Calculate and transport equalitiesL25–25

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L25
    trans 0
13Use earlier factsL26–26

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

  1. L26
    exact he_right_right
14Calculate and transport equalitiesL27–27

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L27
    symm
15Use earlier factsL28–28

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

  1. L28
    exact hf_right_right

Library-wide reading audit

Original defined command ledger · 28 lines
  1. 0001intro i
  2. 0002intro e
  3. 0003intro f
  4. 0004intro he
  5. 0005intro hf
  6. 0006cases he
  7. 0007cases he_left
  8. 0008cases hf
  9. 0009cases hf_left
  10. 0010trans 1
  11. 0011exact he_left_right
  12. 0012symm
  13. 0013exact hf_left_right
  14. 0014cases hf_right
  15. 0015exfalso
  16. 0016apply hf_right_left
  17. 0017exact he_left_left
  18. 0018cases he_right
  19. 0019cases hf
  20. 0020cases hf_left
  21. 0021exfalso
  22. 0022apply he_right_left
  23. 0023exact hf_left_left
  24. 0024cases hf_right
  25. 0025trans 0
  26. 0026exact he_right_right
  27. 0027symm
  28. 0028exact hf_right_right