MC0003

prime_factor_toggle_exists

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

Two constructive divisibility decisions supply the added factor, a genuine quotient, or a fixed prime-square multiple.

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

forall p d. ~(p=0) -> exists e. ((((~(exists pvs_factor_toggle_existsfresh_input. (d) = (p) * pvs_factor_toggle_existsfresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_toggle_existsfresh_output. (e) = (p) * pvs_factor_toggle_existsfresh_output)))) \/ (((exists pvs_factor_toggle_existssquare. (d) = ((p)*(p)) * pvs_factor_toggle_existssquare) /\ ((e)=(d))))))

Constructive proof overview

Generated structural guide

Two constructive divisibility decisions supply the added factor, a genuine quotient, or a fixed prime-square multiple.

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

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

Proof neighborhood

Direct dependencies

multiple_decidable_nonzero Stable theorem; checked-use authorized mul_assoc Stable theorem; checked-use authorized

Direct dependents

MC0008 divisor_prime_toggle_exists

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

41 script commands · 20 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–3

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro hp
02Establish hdL4–8

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

  1. L4
    have hd : (exists pvs_factor_total_yes. (d) = (p) * pvs_factor_total_yes) \/ ~(exists pvs_factor_total_no. (d) = (p) * pvs_factor_total_no)
  2. L5
    specialize multiple_decidable_nonzero (p)
  3. L6
    specialize multiple_decidable_nonzero (d)
  4. L7
    apply multiple_decidable_nonzero
  5. L8
    exact hp
03Separate the logical casesL9–10

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

  1. L9
    cases hd
  2. L10
    cases hd_left
04Establish hqL11–15

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

  1. L11
    have hq : (exists pvs_factor_total_quotient_yes. (x) = (p) * pvs_factor_total_quotient_yes) \/ ~(exists pvs_factor_total_quotient_no. (x) = (p) * pvs_factor_total_quotient_no)
  2. L12
    specialize multiple_decidable_nonzero (p)
  3. L13
    specialize multiple_decidable_nonzero (x)
  4. L14
    apply multiple_decidable_nonzero
  5. L15
    exact hp
05Separate the logical casesL16–17

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

  1. L16
    cases hq
  2. L17
    cases hq_left
06Construct an explicit witnessL18–18

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

  1. L18
    exists d
07Separate the logical casesL19–21

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

  1. L19
    right
  2. L20
    right
  3. L21
    split
08Construct an explicit witnessL22–22

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

  1. L22
    exists x1
09Calculate and transport equalitiesL23–23

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

  1. L23
    trans p*x
10Use earlier factsL24–24

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

  1. L24
    exact hd_left_witness
11Calculate and transport equalitiesL25–28

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

  1. L25
    trans p*(p*x1)
  2. L26
    rewrite hq_left_witness
  3. L27
    refl
  4. L28
    symm
12Use earlier factsL29–29

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

  1. L29
    apply mul_assoc
13Calculate and transport equalitiesL30–30

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

  1. L30
    refl
14Construct an explicit witnessL31–31

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

  1. L31
    exists x
15Separate the logical casesL32–34

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

  1. L32
    right
  2. L33
    left
  3. L34
    split
16Use earlier factsL35–36

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

  1. L35
    exact hd_left_witness
  2. L36
    exact hq_right
17Construct an explicit witnessL37–37

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

  1. L37
    exists p*d
18Separate the logical casesL38–39

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

  1. L38
    left
  2. L39
    split
19Use earlier factsL40–40

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

  1. L40
    exact hd_right
20Calculate and transport equalitiesL41–41

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

  1. L41
    refl

Library-wide reading audit

Original exact command ledger · 41 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro hp
  4. 0004have hd : (exists pvs_factor_total_yes. (d) = (p) * pvs_factor_total_yes) \/ ~(exists pvs_factor_total_no. (d) = (p) * pvs_factor_total_no)
  5. 0005specialize multiple_decidable_nonzero (p)
  6. 0006specialize multiple_decidable_nonzero (d)
  7. 0007apply multiple_decidable_nonzero
  8. 0008exact hp
  9. 0009cases hd
  10. 0010cases hd_left
  11. 0011have hq : (exists pvs_factor_total_quotient_yes. (x) = (p) * pvs_factor_total_quotient_yes) \/ ~(exists pvs_factor_total_quotient_no. (x) = (p) * pvs_factor_total_quotient_no)
  12. 0012specialize multiple_decidable_nonzero (p)
  13. 0013specialize multiple_decidable_nonzero (x)
  14. 0014apply multiple_decidable_nonzero
  15. 0015exact hp
  16. 0016cases hq
  17. 0017cases hq_left
  18. 0018exists d
  19. 0019right
  20. 0020right
  21. 0021split
  22. 0022exists x1
  23. 0023trans p*x
  24. 0024exact hd_left_witness
  25. 0025trans p*(p*x1)
  26. 0026rewrite hq_left_witness
  27. 0027refl
  28. 0028symm
  29. 0029apply mul_assoc
  30. 0030refl
  31. 0031exists x
  32. 0032right
  33. 0033left
  34. 0034split
  35. 0035exact hd_left_witness
  36. 0036exact hq_right
  37. 0037exists p*d
  38. 0038left
  39. 0039split
  40. 0040exact hd_right
  41. 0041refl