MC0007

prime_factor_toggle_preserves_divisor

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

Every actual prime toggle of a divisor of n is again a divisor, provided p itself is a prime divisor of n.

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 p n d e. (~((p) = 1) /\ forall pvs_left_preserve_prime pvs_right_preserve_prime. (p) = pvs_left_preserve_prime * pvs_right_preserve_prime -> pvs_left_preserve_prime = 1 \/ pvs_right_preserve_prime = 1) -> (exists pvs_factor_preserve_p. (n) = (p) * pvs_factor_preserve_p) -> (exists pvs_factor_preserve_d. (n) = (d) * pvs_factor_preserve_d) -> ((((~(exists pvs_factor_preserve_graphfresh_input. (d) = (p) * pvs_factor_preserve_graphfresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_preserve_graphfresh_output. (e) = (p) * pvs_factor_preserve_graphfresh_output)))) \/ (((exists pvs_factor_preserve_graphsquare. (d) = ((p)*(p)) * pvs_factor_preserve_graphsquare) /\ ((e)=(d)))))) -> (exists pvs_factor_preserve_e. (n) = (e) * pvs_factor_preserve_e)

Constructive proof overview

Generated structural guide

Every actual prime toggle of a divisor of n is again a divisor, provided p itself is a prime divisor of n.

The unchanged tactic script uses 3 declared prerequisites and contains 33 exact native proof lines.

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

Proof neighborhood

Direct dependencies

MC0002 prime_toggle_fresh_divisor_product multiple_trans Stable theorem; checked-use authorized mul_comm Stable theorem; checked-use authorized

Direct dependents

MC000A divisor_prime_toggle_symmetric MC000B divisor_prime_toggle_bounded MC0012 mobius_divisor_mask_prime_toggle_negates

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

33 script commands · 12 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.

Named ingredients (1)
prime toggle fresh divisor product
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro d
  4. L4
    intro e
  5. L5
    intro hp
  6. L6
    intro hpn
  7. L7
    intro hdn
  8. L8
    intro he
02Separate the logical casesL9–10

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

  1. L9
    cases he
  2. L10
    cases he_left
03Calculate and transport equalitiesL11–11

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

  1. L11
    rewrite he_left_right
04Use earlier factsL12–19

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

  1. L12
    specialize prime_toggle_fresh_divisor_product (p)
  2. L13
    specialize prime_toggle_fresh_divisor_product (n)
  3. L14
    specialize prime_toggle_fresh_divisor_product (d)
  4. L15
    apply prime_toggle_fresh_divisor_product
  5. L16
    exact hp
  6. L17
    exact hpn
  7. L18
    exact hdn
  8. L19
    exact he_left_left
05Separate the logical casesL20–21

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

  1. L20
    cases he_right
  2. L21
    cases he_right_left
06Use earlier factsL22–26

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

  1. L22
    specialize multiple_trans (d)
  2. L23
    specialize multiple_trans (e)
  3. L24
    specialize multiple_trans (n)
  4. L25
    apply multiple_trans
  5. L26
    exact hdn
07Construct an explicit witnessL27–27

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

  1. L27
    exists p
08Calculate and transport equalitiesL28–28

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

  1. L28
    trans p*e
09Use earlier factsL29–30

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

  1. L29
    exact he_right_left_left
  2. L30
    apply mul_comm
10Separate the logical casesL31–31

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

  1. L31
    cases he_right_right
11Calculate and transport equalitiesL32–32

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

  1. L32
    rewrite he_right_right_right
12Use earlier factsL33–33

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

  1. L33
    exact hdn

Library-wide reading audit

Original exact command ledger · 33 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro d
  4. 0004intro e
  5. 0005intro hp
  6. 0006intro hpn
  7. 0007intro hdn
  8. 0008intro he
  9. 0009cases he
  10. 0010cases he_left
  11. 0011rewrite he_left_right
  12. 0012specialize prime_toggle_fresh_divisor_product (p)
  13. 0013specialize prime_toggle_fresh_divisor_product (n)
  14. 0014specialize prime_toggle_fresh_divisor_product (d)
  15. 0015apply prime_toggle_fresh_divisor_product
  16. 0016exact hp
  17. 0017exact hpn
  18. 0018exact hdn
  19. 0019exact he_left_left
  20. 0020cases he_right
  21. 0021cases he_right_left
  22. 0022specialize multiple_trans (d)
  23. 0023specialize multiple_trans (e)
  24. 0024specialize multiple_trans (n)
  25. 0025apply multiple_trans
  26. 0026exact hdn
  27. 0027exists p
  28. 0028trans p*e
  29. 0029exact he_right_left_left
  30. 0030apply mul_comm
  31. 0031cases he_right_right
  32. 0032rewrite he_right_right_right
  33. 0033exact hdn