PC0032

prime_bit_choice_functional

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

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

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 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

Constructive proof overview

Generated structural guide

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

The unchanged tactic script uses 0 declared prerequisites and contains 28 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

PC0033 prime_bit_prefix_equal_entry

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

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.

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 exact 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