DI0001

positive_divisor_quotient_exists_unique

Every divisor of a positive input has a unique actual positive quotient, itself a divisor bounded by the input.

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 complementary quotient is witnessed by n=d*q at positive divisors. The actual permutation covers indices zero through n, fixing zero and nondivisors. This is the involution foundation for the separate cancellation and full G007 inversion proofs, not an assumed divisor bijection.

Exact theorem in conservative defined notation

∀ n. ∀ d. ¬n = 0 → Dvd(d,n) → ∃ x. n = d · x ∧ (¬x = 0 ∧ (Dvd(x,n) ∧ (Le(x,n) ∧ (∀ y. n = d · y → y = x))))

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

Definition DAG

Le(a,b) · 1Dvd(d,n) · 2

Actual proof prerequisites

factor_nonzero_right · checked external prerequisitemul_comm · checked external prerequisitedivisor_le_nonzero · checked external prerequisitemul_left_cancel_nonzero · checked external prerequisitefactor_nonzero_left · checked external prerequisite
Original expanded first-order statement 
forall n d. ~(n=0) -> (exists pvs_factor_quotient_input. (n) = (d) * pvs_factor_quotient_input) -> exists q. (((n=d*q) /\ (((~(q=0)) /\ (((exists pvs_factor_quotient_divisor. (n) = (q) * pvs_factor_quotient_divisor) /\ (((exists pvs_le_gap_quotient_bound. pvs_le_gap_quotient_bound + (q) = (n)) /\ (forall r. n=d*r -> r=q)))))))))

Complete tactic proof in conservative notation

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

49 script commands · 23 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.

01Fix variables and assumptionsL1–4

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

  1. L1
    intro n
  2. L2
    intro d
  3. L3
    intro hn
  4. L4
    intro hd
02Separate the logical casesL5–5

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

  1. L5
    cases hd
03Construct an explicit witnessL6–6

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

  1. L6
    exists x
04Separate the logical casesL7–7

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

  1. L7
    split
05Use earlier factsL8–8

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

  1. L8
    exact hd_witness
06Separate the logical casesL9–9

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

  1. L9
    split
07Fix variables and assumptionsL10–10

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

  1. L10
    intro hqzero
08Use earlier factsL11–17

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

  1. L11
    specialize factor_nonzero_right (n)
  2. L12
    specialize factor_nonzero_right (d)
  3. L13
    specialize factor_nonzero_right (x)
  4. L14
    apply factor_nonzero_right
  5. L15
    exact hn
  6. L16
    exact hd_witness
  7. L17
    exact hqzero
09Separate the logical casesL18–18

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

  1. L18
    split
10Construct an explicit witnessL19–19

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

  1. L19
    exists d
11Calculate and transport equalitiesL20–20

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

  1. L20
    trans d*x
12Use earlier factsL21–22

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

  1. L21
    exact hd_witness
  2. L22
    apply mul_comm
13Separate the logical casesL23–23

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

  1. L23
    split
14Use earlier factsL24–27

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

  1. L24
    specialize divisor_le_nonzero (x)
  2. L25
    specialize divisor_le_nonzero (n)
  3. L26
    apply divisor_le_nonzero
  4. L27
    exact hn
15Construct an explicit witnessL28–28

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

  1. L28
    exists d
16Calculate and transport equalitiesL29–29

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

  1. L29
    trans d*x
17Use earlier factsL30–31

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

  1. L30
    exact hd_witness
  2. L31
    apply mul_comm
18Fix variables and assumptionsL32–33

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

  1. L32
    intro r
  2. L33
    intro hr
19Use earlier factsL34–37

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

  1. L34
    specialize mul_left_cancel_nonzero (d)
  2. L35
    specialize mul_left_cancel_nonzero (r)
  3. L36
    specialize mul_left_cancel_nonzero (x)
  4. L37
    apply mul_left_cancel_nonzero
20Fix variables and assumptionsL38–38

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

  1. L38
    intro hdzero
21Use earlier factsL39–45

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

  1. L39
    specialize factor_nonzero_left (n)
  2. L40
    specialize factor_nonzero_left (d)
  3. L41
    specialize factor_nonzero_left (x)
  4. L42
    apply factor_nonzero_left
  5. L43
    exact hn
  6. L44
    exact hd_witness
  7. L45
    exact hdzero
22Calculate and transport equalitiesL46–47

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

  1. L46
    trans n
  2. L47
    symm
23Use earlier factsL48–49

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

  1. L48
    exact hr
  2. L49
    exact hd_witness

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro n
  2. 0002intro d
  3. 0003intro hn
  4. 0004intro hd
  5. 0005cases hd
  6. 0006exists x
  7. 0007split
  8. 0008exact hd_witness
  9. 0009split
  10. 0010intro hqzero
  11. 0011specialize factor_nonzero_right (n)
  12. 0012specialize factor_nonzero_right (d)
  13. 0013specialize factor_nonzero_right (x)
  14. 0014apply factor_nonzero_right
  15. 0015exact hn
  16. 0016exact hd_witness
  17. 0017exact hqzero
  18. 0018split
  19. 0019exists d
  20. 0020trans d*x
  21. 0021exact hd_witness
  22. 0022apply mul_comm
  23. 0023split
  24. 0024specialize divisor_le_nonzero (x)
  25. 0025specialize divisor_le_nonzero (n)
  26. 0026apply divisor_le_nonzero
  27. 0027exact hn
  28. 0028exists d
  29. 0029trans d*x
  30. 0030exact hd_witness
  31. 0031apply mul_comm
  32. 0032intro r
  33. 0033intro hr
  34. 0034specialize mul_left_cancel_nonzero (d)
  35. 0035specialize mul_left_cancel_nonzero (r)
  36. 0036specialize mul_left_cancel_nonzero (x)
  37. 0037apply mul_left_cancel_nonzero
  38. 0038intro hdzero
  39. 0039specialize factor_nonzero_left (n)
  40. 0040specialize factor_nonzero_left (d)
  41. 0041specialize factor_nonzero_left (x)
  42. 0042apply factor_nonzero_left
  43. 0043exact hn
  44. 0044exact hd_witness
  45. 0045exact hdzero
  46. 0046trans n
  47. 0047symm
  48. 0048exact hr
  49. 0049exact hd_witness