MC0008

divisor_prime_toggle_exists

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

Decide positive-divisor membership and construct the raw toggle there, using identity at zero and nondivisors.

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 n p d. (~((p) = 1) /\ forall pvs_left_divisor_total_prime pvs_right_divisor_total_prime. (p) = pvs_left_divisor_total_prime * pvs_right_divisor_total_prime -> pvs_left_divisor_total_prime = 1 \/ pvs_right_divisor_total_prime = 1) -> exists e. ((((~((d)=0)) /\ (((exists pvs_factor_divisor_total_resultdivisor. (n) = (d) * pvs_factor_divisor_total_resultdivisor) /\ ((((~(exists pvs_factor_divisor_total_resulttogglefresh_input. (d) = (p) * pvs_factor_divisor_total_resulttogglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_divisor_total_resulttogglefresh_output. (e) = (p) * pvs_factor_divisor_total_resulttogglefresh_output)))) \/ (((exists pvs_factor_divisor_total_resulttogglesquare. (d) = ((p)*(p)) * pvs_factor_divisor_total_resulttogglesquare) /\ ((e)=(d)))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_divisor_total_resultnondivisor. (n) = (d) * pvs_factor_divisor_total_resultnondivisor)) /\ ((e)=(d)))))

Constructive proof overview

Generated structural guide

Decide positive-divisor membership and construct the raw toggle there, using identity at zero and nondivisors.

The unchanged tactic script uses 4 declared prerequisites and contains 44 exact native proof lines.

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

Proof neighborhood

Direct dependencies

eq_decidable Stable theorem; checked-use authorized multiple_decidable_nonzero Stable theorem; checked-use authorized MC0003 prime_factor_toggle_exists prime_nonzero Stable theorem; checked-use authorized

Direct dependents

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

44 script commands · 20 reading checkpoints · 3 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 (1)
prime factor toggle exists
01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro p
  3. L3
    intro d
  4. L4
    intro hp
02Establish hzL5–8

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

  1. L5
    have hz : d=0 \/ ~(d=0)
  2. L6
    specialize eq_decidable (d)
  3. L7
    specialize eq_decidable (0)
  4. L8
    apply eq_decidable
03Separate the logical casesL9–9

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

  1. L9
    cases hz
04Construct an explicit witnessL10–10

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

  1. L10
    exists d
05Separate the logical casesL11–13

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

  1. L11
    right
  2. L12
    split
  3. L13
    left
06Use earlier factsL14–14

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

  1. L14
    exact hz_left
07Calculate and transport equalitiesL15–15

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

  1. L15
    refl
08Establish hdL16–20

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

  1. L16
    have hd : (exists pvs_factor_divisor_total_yes. (n) = (d) * pvs_factor_divisor_total_yes) \/ ~(exists pvs_factor_divisor_total_no. (n) = (d) * pvs_factor_divisor_total_no)
  2. L17
    specialize multiple_decidable_nonzero (d)
  3. L18
    specialize multiple_decidable_nonzero (n)
  4. L19
    apply multiple_decidable_nonzero
  5. L20
    exact hz_right
09Separate the logical casesL21–21

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

  1. L21
    cases hd
10Establish heL22–30

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime factor toggle exists.

  1. L22
    have he : exists e. ((((~(exists pvs_factor_divisor_total_togglefresh_input. (d) = (p) * pvs_factor_divisor_total_togglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_divisor_total_togglefresh_output. (e) = (p) * pvs_factor_divisor_total_togglefresh_output)))) \/ (((exists pvs_factor_divisor_total_togglesquare. (d) = ((p)*(p)) * pvs_factor_divisor_total_togglesquare) /\ ((e)=(d))))))
  2. L23
    specialize prime_factor_toggle_exists (p)
  3. L24
    specialize prime_factor_toggle_exists (d)
  4. L25
    apply prime_factor_toggle_exists
  5. L26
    intro hzero
  6. L27
    specialize prime_nonzero (p)
  7. L28
    apply prime_nonzero
  8. L29
    exact hp
  9. L30
    exact hzero
11Separate the logical casesL31–31

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

  1. L31
    cases he
12Construct an explicit witnessL32–32

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

  1. L32
    exists x
13Separate the logical casesL33–34

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

  1. L33
    left
  2. L34
    split
14Use earlier factsL35–35

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

  1. L35
    exact hz_right
15Separate the logical casesL36–36

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

  1. L36
    split
16Use earlier factsL37–38

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

  1. L37
    exact hd_left
  2. L38
    exact he_witness
17Construct an explicit witnessL39–39

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

  1. L39
    exists d
18Separate the logical casesL40–42

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

  1. L40
    right
  2. L41
    split
  3. L42
    right
19Use earlier factsL43–43

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

  1. L43
    exact hd_right
20Calculate and transport equalitiesL44–44

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

  1. L44
    refl

Library-wide reading audit

Original exact command ledger · 44 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro d
  4. 0004intro hp
  5. 0005have hz : d=0 \/ ~(d=0)
  6. 0006specialize eq_decidable (d)
  7. 0007specialize eq_decidable (0)
  8. 0008apply eq_decidable
  9. 0009cases hz
  10. 0010exists d
  11. 0011right
  12. 0012split
  13. 0013left
  14. 0014exact hz_left
  15. 0015refl
  16. 0016have hd : (exists pvs_factor_divisor_total_yes. (n) = (d) * pvs_factor_divisor_total_yes) \/ ~(exists pvs_factor_divisor_total_no. (n) = (d) * pvs_factor_divisor_total_no)
  17. 0017specialize multiple_decidable_nonzero (d)
  18. 0018specialize multiple_decidable_nonzero (n)
  19. 0019apply multiple_decidable_nonzero
  20. 0020exact hz_right
  21. 0021cases hd
  22. 0022have he : exists e. ((((~(exists pvs_factor_divisor_total_togglefresh_input. (d) = (p) * pvs_factor_divisor_total_togglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_divisor_total_togglefresh_output. (e) = (p) * pvs_factor_divisor_total_togglefresh_output)))) \/ (((exists pvs_factor_divisor_total_togglesquare. (d) = ((p)*(p)) * pvs_factor_divisor_total_togglesquare) /\ ((e)=(d))))))
  23. 0023specialize prime_factor_toggle_exists (p)
  24. 0024specialize prime_factor_toggle_exists (d)
  25. 0025apply prime_factor_toggle_exists
  26. 0026intro hzero
  27. 0027specialize prime_nonzero (p)
  28. 0028apply prime_nonzero
  29. 0029exact hp
  30. 0030exact hzero
  31. 0031cases he
  32. 0032exists x
  33. 0033left
  34. 0034split
  35. 0035exact hz_right
  36. 0036split
  37. 0037exact hd_left
  38. 0038exact he_witness
  39. 0039exists d
  40. 0040right
  41. 0041split
  42. 0042right
  43. 0043exact hd_right
  44. 0044refl