MC0004

prime_factor_toggle_functional

Fresh, singly divisible and square-divisible branches are disjoint; cancellation of a nonzero p proves exact output uniqueness.

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. ∀ e. ∀ f. ¬p = 0 → PrimeFactorToggle(p,d,e) → PrimeFactorToggle(p,d,f) → e = f

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

Definition DAG

PrimeFactorToggle(p,d,e) · 2

Actual proof prerequisites

multiple_trans · checked external prerequisitemul_left_cancel_nonzero · checked external prerequisiteprime_toggle_square_quotient_divides
Original expanded first-order statement 
forall p d e f. ~(p=0) -> ((((~(exists pvs_factor_toggle_functional_firstfresh_input. (d) = (p) * pvs_factor_toggle_functional_firstfresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_toggle_functional_firstfresh_output. (e) = (p) * pvs_factor_toggle_functional_firstfresh_output)))) \/ (((exists pvs_factor_toggle_functional_firstsquare. (d) = ((p)*(p)) * pvs_factor_toggle_functional_firstsquare) /\ ((e)=(d)))))) -> ((((~(exists pvs_factor_toggle_functional_secondfresh_input. (d) = (p) * pvs_factor_toggle_functional_secondfresh_input)) /\ ((f)=(p)*(d)))) \/ (((((d)=(p)*(f)) /\ (~(exists pvs_factor_toggle_functional_secondfresh_output. (f) = (p) * pvs_factor_toggle_functional_secondfresh_output)))) \/ (((exists pvs_factor_toggle_functional_secondsquare. (d) = ((p)*(p)) * pvs_factor_toggle_functional_secondsquare) /\ ((f)=(d)))))) -> e=f

Complete tactic proof in conservative notation

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

88 script commands · 35 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.

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 toggle square quotient divides
01Fix variables and assumptionsL1–7

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

  1. L1
    intro p
  2. L2
    intro d
  3. L3
    intro e
  4. L4
    intro f
  5. L5
    intro hp
  6. L6
    intro he
  7. L7
    intro hf
02Separate the logical casesL8–11

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

  1. L8
    cases he
  2. L9
    cases he_left
  3. L10
    cases hf
  4. L11
    cases hf_left
03Calculate and transport equalitiesL12–12

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

  1. L12
    trans p*d
04Use earlier factsL13–13

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

  1. L13
    exact he_left_right
05Calculate and transport equalitiesL14–14

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

  1. L14
    symm
06Use earlier factsL15–15

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

  1. L15
    exact hf_left_right
07Separate the logical casesL16–18

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

  1. L16
    cases hf_right
  2. L17
    cases hf_right_left
  3. L18
    exfalso
08Use earlier factsL19–19

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

  1. L19
    apply he_left_left
09Construct an explicit witnessL20–20

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

  1. L20
    exists f
10Use earlier factsL21–21

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

  1. L21
    exact hf_right_left_left
11Separate the logical casesL22–23

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

  1. L22
    cases hf_right_right
  2. L23
    exfalso
12Use earlier factsL24–29

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

  1. L24
    apply he_left_left
  2. L25
    specialize multiple_trans (p*p)
  3. L26
    specialize multiple_trans (p)
  4. L27
    specialize multiple_trans (d)
  5. L28
    apply multiple_trans
  6. L29
    exact hf_right_right_left
13Construct an explicit witnessL30–30

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

  1. L30
    exists p
14Calculate and transport equalitiesL31–31

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

  1. L31
    refl
15Separate the logical casesL32–36

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

  1. L32
    cases he_right
  2. L33
    cases he_right_left
  3. L34
    cases hf
  4. L35
    cases hf_left
  5. L36
    exfalso
16Use earlier factsL37–37

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

  1. L37
    apply hf_left_left
17Construct an explicit witnessL38–38

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

  1. L38
    exists e
18Use earlier factsL39–39

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

  1. L39
    exact he_right_left_left
19Separate the logical casesL40–41

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

  1. L40
    cases hf_right
  2. L41
    cases hf_right_left
20Use earlier factsL42–46

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

  1. L42
    specialize mul_left_cancel_nonzero (p)
  2. L43
    specialize mul_left_cancel_nonzero (e)
  3. L44
    specialize mul_left_cancel_nonzero (f)
  4. L45
    apply mul_left_cancel_nonzero
  5. L46
    exact hp
21Calculate and transport equalitiesL47–48

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

  1. L47
    trans d
  2. L48
    symm
22Use earlier factsL49–50

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

  1. L49
    exact he_right_left_left
  2. L50
    exact hf_right_left_left
23Separate the logical casesL51–52

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

  1. L51
    cases hf_right_right
  2. L52
    exfalso
24Use earlier factsL53–60

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

  1. L53
    apply he_right_left_right
  2. L54
    specialize prime_toggle_square_quotient_divides (p)
  3. L55
    specialize prime_toggle_square_quotient_divides (d)
  4. L56
    specialize prime_toggle_square_quotient_divides (e)
  5. L57
    apply prime_toggle_square_quotient_divides
  6. L58
    exact hp
  7. L59
    exact he_right_left_left
  8. L60
    exact hf_right_right_left
25Separate the logical casesL61–64

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

  1. L61
    cases he_right_right
  2. L62
    cases hf
  3. L63
    cases hf_left
  4. L64
    exfalso
26Use earlier factsL65–70

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

  1. L65
    apply hf_left_left
  2. L66
    specialize multiple_trans (p*p)
  3. L67
    specialize multiple_trans (p)
  4. L68
    specialize multiple_trans (d)
  5. L69
    apply multiple_trans
  6. L70
    exact he_right_right_left
27Construct an explicit witnessL71–71

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

  1. L71
    exists p
28Calculate and transport equalitiesL72–72

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

  1. L72
    refl
29Separate the logical casesL73–75

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

  1. L73
    cases hf_right
  2. L74
    cases hf_right_left
  3. L75
    exfalso
30Use earlier factsL76–83

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

  1. L76
    apply hf_right_left_right
  2. L77
    specialize prime_toggle_square_quotient_divides (p)
  3. L78
    specialize prime_toggle_square_quotient_divides (d)
  4. L79
    specialize prime_toggle_square_quotient_divides (f)
  5. L80
    apply prime_toggle_square_quotient_divides
  6. L81
    exact hp
  7. L82
    exact hf_right_left_left
  8. L83
    exact he_right_right_left
31Separate the logical casesL84–84

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

  1. L84
    cases hf_right_right
32Calculate and transport equalitiesL85–85

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

  1. L85
    trans d
33Use earlier factsL86–86

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

  1. L86
    exact he_right_right_right
34Calculate and transport equalitiesL87–87

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

  1. L87
    symm
35Use earlier factsL88–88

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

  1. L88
    exact hf_right_right_right

Library-wide reading audit

Original defined command ledger · 88 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro e
  4. 0004intro f
  5. 0005intro hp
  6. 0006intro he
  7. 0007intro hf
  8. 0008cases he
  9. 0009cases he_left
  10. 0010cases hf
  11. 0011cases hf_left
  12. 0012trans p*d
  13. 0013exact he_left_right
  14. 0014symm
  15. 0015exact hf_left_right
  16. 0016cases hf_right
  17. 0017cases hf_right_left
  18. 0018exfalso
  19. 0019apply he_left_left
  20. 0020exists f
  21. 0021exact hf_right_left_left
  22. 0022cases hf_right_right
  23. 0023exfalso
  24. 0024apply he_left_left
  25. 0025specialize multiple_trans (p*p)
  26. 0026specialize multiple_trans (p)
  27. 0027specialize multiple_trans (d)
  28. 0028apply multiple_trans
  29. 0029exact hf_right_right_left
  30. 0030exists p
  31. 0031refl
  32. 0032cases he_right
  33. 0033cases he_right_left
  34. 0034cases hf
  35. 0035cases hf_left
  36. 0036exfalso
  37. 0037apply hf_left_left
  38. 0038exists e
  39. 0039exact he_right_left_left
  40. 0040cases hf_right
  41. 0041cases hf_right_left
  42. 0042specialize mul_left_cancel_nonzero (p)
  43. 0043specialize mul_left_cancel_nonzero (e)
  44. 0044specialize mul_left_cancel_nonzero (f)
  45. 0045apply mul_left_cancel_nonzero
  46. 0046exact hp
  47. 0047trans d
  48. 0048symm
  49. 0049exact he_right_left_left
  50. 0050exact hf_right_left_left
  51. 0051cases hf_right_right
  52. 0052exfalso
  53. 0053apply he_right_left_right
  54. 0054specialize prime_toggle_square_quotient_divides (p)
  55. 0055specialize prime_toggle_square_quotient_divides (d)
  56. 0056specialize prime_toggle_square_quotient_divides (e)
  57. 0057apply prime_toggle_square_quotient_divides
  58. 0058exact hp
  59. 0059exact he_right_left_left
  60. 0060exact hf_right_right_left
  61. 0061cases he_right_right
  62. 0062cases hf
  63. 0063cases hf_left
  64. 0064exfalso
  65. 0065apply hf_left_left
  66. 0066specialize multiple_trans (p*p)
  67. 0067specialize multiple_trans (p)
  68. 0068specialize multiple_trans (d)
  69. 0069apply multiple_trans
  70. 0070exact he_right_right_left
  71. 0071exists p
  72. 0072refl
  73. 0073cases hf_right
  74. 0074cases hf_right_left
  75. 0075exfalso
  76. 0076apply hf_right_left_right
  77. 0077specialize prime_toggle_square_quotient_divides (p)
  78. 0078specialize prime_toggle_square_quotient_divides (d)
  79. 0079specialize prime_toggle_square_quotient_divides (f)
  80. 0080apply prime_toggle_square_quotient_divides
  81. 0081exact hp
  82. 0082exact hf_right_left_left
  83. 0083exact he_right_right_left
  84. 0084cases hf_right_right
  85. 0085trans d
  86. 0086exact he_right_right_right
  87. 0087symm
  88. 0088exact hf_right_right_right