MC0009

divisor_prime_toggle_functional

The actual positive-divisor toggle and omitted-index identity define one output for every natural index.

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. ∀ e. ∀ f. Prime(p) → DivisorPrimeToggle(n,p,d,e) → DivisorPrimeToggle(n,p,d,f) → e = f

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

Definition DAG

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

Actual proof prerequisites

prime_factor_toggle_functionalprime_nonzero · checked external prerequisite
Original expanded first-order statement 
forall n p d e f. (~((p) = 1) /\ forall pvs_left_divisor_functional_prime pvs_right_divisor_functional_prime. (p) = pvs_left_divisor_functional_prime * pvs_right_divisor_functional_prime -> pvs_left_divisor_functional_prime = 1 \/ pvs_right_divisor_functional_prime = 1) -> ((((~((d)=0)) /\ (((exists pvs_factor_divisor_functional_firstdivisor. (n) = (d) * pvs_factor_divisor_functional_firstdivisor) /\ ((((~(exists pvs_factor_divisor_functional_firsttogglefresh_input. (d) = (p) * pvs_factor_divisor_functional_firsttogglefresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_divisor_functional_firsttogglefresh_output. (e) = (p) * pvs_factor_divisor_functional_firsttogglefresh_output)))) \/ (((exists pvs_factor_divisor_functional_firsttogglesquare. (d) = ((p)*(p)) * pvs_factor_divisor_functional_firsttogglesquare) /\ ((e)=(d)))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_divisor_functional_firstnondivisor. (n) = (d) * pvs_factor_divisor_functional_firstnondivisor)) /\ ((e)=(d))))) -> ((((~((d)=0)) /\ (((exists pvs_factor_divisor_functional_seconddivisor. (n) = (d) * pvs_factor_divisor_functional_seconddivisor) /\ ((((~(exists pvs_factor_divisor_functional_secondtogglefresh_input. (d) = (p) * pvs_factor_divisor_functional_secondtogglefresh_input)) /\ ((f)=(p)*(d)))) \/ (((((d)=(p)*(f)) /\ (~(exists pvs_factor_divisor_functional_secondtogglefresh_output. (f) = (p) * pvs_factor_divisor_functional_secondtogglefresh_output)))) \/ (((exists pvs_factor_divisor_functional_secondtogglesquare. (d) = ((p)*(p)) * pvs_factor_divisor_functional_secondtogglesquare) /\ ((f)=(d)))))))))) \/ ((((d)=0 \/ ~(exists pvs_factor_divisor_functional_secondnondivisor. (n) = (d) * pvs_factor_divisor_functional_secondnondivisor)) /\ ((f)=(d))))) -> e=f

Complete tactic proof in conservative notation

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

48 script commands · 14 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 factor toggle functional
01Fix variables and assumptionsL1–8

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 e
  5. L5
    intro f
  6. L6
    intro hp
  7. L7
    intro he
  8. L8
    intro hf
02Separate the logical casesL9–14

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

  1. L9
    cases he
  2. L10
    cases he_left
  3. L11
    cases he_left_right
  4. L12
    cases hf
  5. L13
    cases hf_left
  6. L14
    cases hf_left_right
03Use earlier factsL15–19

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

  1. L15
    specialize prime_factor_toggle_functional (p)
  2. L16
    specialize prime_factor_toggle_functional (d)
  3. L17
    specialize prime_factor_toggle_functional (e)
  4. L18
    specialize prime_factor_toggle_functional (f)
  5. L19
    apply prime_factor_toggle_functional
04Fix variables and assumptionsL20–20

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

  1. L20
    intro hzero
05Use earlier factsL21–26

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

  1. L21
    specialize prime_nonzero (p)
  2. L22
    apply prime_nonzero
  3. L23
    exact hp
  4. L24
    exact hzero
  5. L25
    exact he_left_right_right
  6. L26
    exact hf_left_right_right
06Separate the logical casesL27–29

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

  1. L27
    cases hf_right
  2. L28
    exfalso
  3. L29
    cases hf_right_left
07Use earlier factsL30–33

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

  1. L30
    apply he_left_left
  2. L31
    exact hf_right_left_left
  3. L32
    apply hf_right_left_right
  4. L33
    exact he_left_right_left
08Separate the logical casesL34–39

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

  1. L34
    cases he_right
  2. L35
    cases hf
  3. L36
    cases hf_left
  4. L37
    cases hf_left_right
  5. L38
    exfalso
  6. L39
    cases he_right_left
09Use earlier factsL40–43

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

  1. L40
    apply hf_left_left
  2. L41
    exact he_right_left_left
  3. L42
    apply he_right_left_right
  4. L43
    exact hf_left_right_left
10Separate the logical casesL44–44

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

  1. L44
    cases hf_right
11Calculate and transport equalitiesL45–45

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

  1. L45
    trans d
12Use earlier factsL46–46

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

  1. L46
    exact he_right_right
13Calculate and transport equalitiesL47–47

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

  1. L47
    symm
14Use earlier factsL48–48

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

  1. L48
    exact hf_right_right

Library-wide reading audit

Original defined command ledger · 48 lines
  1. 0001intro n
  2. 0002intro p
  3. 0003intro d
  4. 0004intro e
  5. 0005intro f
  6. 0006intro hp
  7. 0007intro he
  8. 0008intro hf
  9. 0009cases he
  10. 0010cases he_left
  11. 0011cases he_left_right
  12. 0012cases hf
  13. 0013cases hf_left
  14. 0014cases hf_left_right
  15. 0015specialize prime_factor_toggle_functional (p)
  16. 0016specialize prime_factor_toggle_functional (d)
  17. 0017specialize prime_factor_toggle_functional (e)
  18. 0018specialize prime_factor_toggle_functional (f)
  19. 0019apply prime_factor_toggle_functional
  20. 0020intro hzero
  21. 0021specialize prime_nonzero (p)
  22. 0022apply prime_nonzero
  23. 0023exact hp
  24. 0024exact hzero
  25. 0025exact he_left_right_right
  26. 0026exact hf_left_right_right
  27. 0027cases hf_right
  28. 0028exfalso
  29. 0029cases hf_right_left
  30. 0030apply he_left_left
  31. 0031exact hf_right_left_left
  32. 0032apply hf_right_left_right
  33. 0033exact he_left_right_left
  34. 0034cases he_right
  35. 0035cases hf
  36. 0036cases hf_left
  37. 0037cases hf_left_right
  38. 0038exfalso
  39. 0039cases he_right_left
  40. 0040apply hf_left_left
  41. 0041exact he_right_left_left
  42. 0042apply he_right_left_right
  43. 0043exact hf_left_right_left
  44. 0044cases hf_right
  45. 0045trans d
  46. 0046exact he_right_right
  47. 0047symm
  48. 0048exact hf_right_right