MC0008

divisor_prime_toggle_exists

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

Alpha v34 checked-use · first admitted v31 · 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.

The input n is positive. Signed code 2 denotes +1, so the actual sum is +1 at n=1 and zero for n>1. The positive-values result permits arbitrary F(0), which the divisor mask excludes. Prime-square multiples contribute zero. Full G007 inversion is established in its separate family.

Exact theorem in conservative defined notation

∀ n. ∀ p. ∀ d. Prime(p) → ∃ x. DivisorPrimeToggle(n,p,d,x)

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

Definition DAG

PrimeFactorToggle(p,d,e) · 1DivisorPrimeToggle(n,p,d,e) · 1Dvd(d,n) · 2Prime(p) · 1

Actual proof prerequisites

eq_decidable · checked external prerequisitemultiple_decidable_nonzero · checked external prerequisiteprime_factor_toggle_existsprime_nonzero · checked external prerequisite
Original expanded first-order 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)))))

Complete tactic proof in conservative notation

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

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.

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

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 : Dvd(d,n) ∨ ¬Dvd(d,n)Definitions: Dvd(d,n)Original native command in the exact edition
  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 : ∃ e. PrimeFactorToggle(p,d,e)Definitions: PrimeFactorToggle(p,d,e)Original native command in the exact edition
  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 defined 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 : Dvd(d,n) ∨ ¬Dvd(d,n)
  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 : ∃ e. PrimeFactorToggle(p,d,e)
  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