MC0005

prime_factor_toggle_symmetric

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

Adding and removing a fresh factor reverse each other, while the witnessed square-divisible branch is fixed.

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 d e. ((((~(exists pvs_factor_toggle_symmetric_firstfresh_input. (d) = (p) * pvs_factor_toggle_symmetric_firstfresh_input)) /\ ((e)=(p)*(d)))) \/ (((((d)=(p)*(e)) /\ (~(exists pvs_factor_toggle_symmetric_firstfresh_output. (e) = (p) * pvs_factor_toggle_symmetric_firstfresh_output)))) \/ (((exists pvs_factor_toggle_symmetric_firstsquare. (d) = ((p)*(p)) * pvs_factor_toggle_symmetric_firstsquare) /\ ((e)=(d)))))) -> ((((~(exists pvs_factor_toggle_symmetric_secondfresh_input. (e) = (p) * pvs_factor_toggle_symmetric_secondfresh_input)) /\ ((d)=(p)*(e)))) \/ (((((e)=(p)*(d)) /\ (~(exists pvs_factor_toggle_symmetric_secondfresh_output. (d) = (p) * pvs_factor_toggle_symmetric_secondfresh_output)))) \/ (((exists pvs_factor_toggle_symmetric_secondsquare. (e) = ((p)*(p)) * pvs_factor_toggle_symmetric_secondsquare) /\ ((d)=(e))))))

Constructive proof overview

Generated structural guide

Adding and removing a fresh factor reverse each other, while the witnessed square-divisible branch is fixed.

The unchanged tactic script uses 0 declared prerequisites and contains 28 exact native proof lines.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

MC000A divisor_prime_toggle_symmetric

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

28 script commands · 10 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.

01Fix variables and assumptionsL1–4

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 h
02Separate the logical casesL5–9

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

  1. L5
    cases h
  2. L6
    cases h_left
  3. L7
    right
  4. L8
    left
  5. L9
    split
03Use earlier factsL10–11

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

  1. L10
    exact h_left_right
  2. L11
    exact h_left_left
04Separate the logical casesL12–15

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

  1. L12
    cases h_right
  2. L13
    cases h_right_left
  3. L14
    left
  4. L15
    split
05Use earlier factsL16–17

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

  1. L16
    exact h_right_left_right
  2. L17
    exact h_right_left_left
06Separate the logical casesL18–18

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

  1. L18
    cases h_right_right
07Calculate and transport equalitiesL19–23

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

  1. L19
    rewrite h_right_right_right
  2. L20
    rewrite h_right_right_right
  3. L21
    rewrite h_right_right_right
  4. L22
    rewrite h_right_right_right
  5. L23
    rewrite h_right_right_right
08Separate the logical casesL24–26

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

  1. L24
    right
  2. L25
    right
  3. L26
    split
09Use earlier factsL27–27

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

  1. L27
    exact h_right_right_left
10Calculate and transport equalitiesL28–28

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

  1. L28
    refl

Library-wide reading audit

Original exact command ledger · 28 lines
  1. 0001intro p
  2. 0002intro d
  3. 0003intro e
  4. 0004intro h
  5. 0005cases h
  6. 0006cases h_left
  7. 0007right
  8. 0008left
  9. 0009split
  10. 0010exact h_left_right
  11. 0011exact h_left_left
  12. 0012cases h_right
  13. 0013cases h_right_left
  14. 0014left
  15. 0015split
  16. 0016exact h_right_left_right
  17. 0017exact h_right_left_left
  18. 0018cases h_right_right
  19. 0019rewrite h_right_right_right
  20. 0020rewrite h_right_right_right
  21. 0021rewrite h_right_right_right
  22. 0022rewrite h_right_right_right
  23. 0023rewrite h_right_right_right
  24. 0024right
  25. 0025right
  26. 0026split
  27. 0027exact h_right_right_left
  28. 0028refl