MC0003

prime_factor_toggle_exists

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

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

∀ p. ∀ d. ¬p = 0 → ∃ x. PrimeFactorToggle(p,d,x)

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

Definition DAG

PrimeFactorToggle(p,d,e) · 1Dvd(d,n) · 4

Actual proof prerequisites

multiple_decidable_nonzero · checked external prerequisitemul_assoc · checked external prerequisite
Original expanded first-order 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))))))

Complete tactic proof in conservative notation

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

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.

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–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 : Dvd(p,d) ∨ ¬Dvd(p,d)Definitions: Dvd(p,d)Original native command in the exact edition
  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 : Dvd(p,x) ∨ ¬Dvd(p,x)Definitions: Dvd(p,x)Original native command in the exact edition
  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 defined command ledger · 41 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro hp
  4. 0004have hd : Dvd(p,d) ∨ ¬Dvd(p,d)
  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 : Dvd(p,x) ∨ ¬Dvd(p,x)
  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