DI0003

divisor_complement_functional

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

The actual quotient and identity branches are disjoint and determine one output; beta-code equality is not assumed.

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 n d q r. ((((~((d)=0)) /\ ((n)=(d)*(q)))) \/ ((((d)=0 \/ ~(exists pvs_factor_functional_firstnondivisor. (n) = (d) * pvs_factor_functional_firstnondivisor)) /\ ((q)=(d))))) -> ((((~((d)=0)) /\ ((n)=(d)*(r)))) \/ ((((d)=0 \/ ~(exists pvs_factor_functional_secondnondivisor. (n) = (d) * pvs_factor_functional_secondnondivisor)) /\ ((r)=(d))))) -> q=r

Constructive proof overview

Generated structural guide

The actual quotient and identity branches are disjoint and determine one output; beta-code equality is not assumed.

The unchanged tactic script uses 1 declared prerequisite and contains 42 exact native proof lines.

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

Proof neighborhood

Direct dependencies

mul_left_cancel_nonzero Stable theorem; checked-use authorized

Direct dependents

DI0009 divisor_complement_prefix_permutation DI000B divisor_complement_prefix_involution DI000C divisor_complement_prefix_positive_quotient

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

42 script commands · 18 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–6

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

  1. L1
    intro n
  2. L2
    intro d
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro hq
  6. L6
    intro hr
02Separate the logical casesL7–10

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

  1. L7
    cases hq
  2. L8
    cases hq_left
  3. L9
    cases hr
  4. L10
    cases hr_left
03Use earlier factsL11–15

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

  1. L11
    specialize mul_left_cancel_nonzero (d)
  2. L12
    specialize mul_left_cancel_nonzero (q)
  3. L13
    specialize mul_left_cancel_nonzero (r)
  4. L14
    apply mul_left_cancel_nonzero
  5. L15
    exact hq_left_left
04Calculate and transport equalitiesL16–17

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

  1. L16
    trans n
  2. L17
    symm
05Use earlier factsL18–19

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

  1. L18
    exact hq_left_right
  2. L19
    exact hr_left_right
06Separate the logical casesL20–22

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

  1. L20
    cases hr_right
  2. L21
    exfalso
  3. L22
    cases hr_right_left
07Use earlier factsL23–25

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

  1. L23
    apply hq_left_left
  2. L24
    exact hr_right_left_left
  3. L25
    apply hr_right_left_right
08Construct an explicit witnessL26–26

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

  1. L26
    exists q
09Use earlier factsL27–27

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

  1. L27
    exact hq_left_right
10Separate the logical casesL28–32

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

  1. L28
    cases hq_right
  2. L29
    cases hr
  3. L30
    cases hr_left
  4. L31
    exfalso
  5. L32
    cases hq_right_left
11Use earlier factsL33–35

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

  1. L33
    apply hr_left_left
  2. L34
    exact hq_right_left_left
  3. L35
    apply hq_right_left_right
12Construct an explicit witnessL36–36

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

  1. L36
    exists r
13Use earlier factsL37–37

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

  1. L37
    exact hr_left_right
14Separate the logical casesL38–38

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

  1. L38
    cases hr_right
15Calculate and transport equalitiesL39–39

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

  1. L39
    trans d
16Use earlier factsL40–40

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

  1. L40
    exact hq_right_right
17Calculate and transport equalitiesL41–41

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

  1. L41
    symm
18Use earlier factsL42–42

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

  1. L42
    exact hr_right_right

Library-wide reading audit

Original exact command ledger · 42 lines
  1. 0001intro n
  2. 0002intro d
  3. 0003intro q
  4. 0004intro r
  5. 0005intro hq
  6. 0006intro hr
  7. 0007cases hq
  8. 0008cases hq_left
  9. 0009cases hr
  10. 0010cases hr_left
  11. 0011specialize mul_left_cancel_nonzero (d)
  12. 0012specialize mul_left_cancel_nonzero (q)
  13. 0013specialize mul_left_cancel_nonzero (r)
  14. 0014apply mul_left_cancel_nonzero
  15. 0015exact hq_left_left
  16. 0016trans n
  17. 0017symm
  18. 0018exact hq_left_right
  19. 0019exact hr_left_right
  20. 0020cases hr_right
  21. 0021exfalso
  22. 0022cases hr_right_left
  23. 0023apply hq_left_left
  24. 0024exact hr_right_left_left
  25. 0025apply hr_right_left_right
  26. 0026exists q
  27. 0027exact hq_left_right
  28. 0028cases hq_right
  29. 0029cases hr
  30. 0030cases hr_left
  31. 0031exfalso
  32. 0032cases hq_right_left
  33. 0033apply hr_left_left
  34. 0034exact hq_right_left_left
  35. 0035apply hq_right_left_right
  36. 0036exists r
  37. 0037exact hr_left_right
  38. 0038cases hr_right
  39. 0039trans d
  40. 0040exact hq_right_right
  41. 0041symm
  42. 0042exact hr_right_right