DI0003

divisor_complement_functional

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

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. ∀ q. ∀ r. DivisorComplement(n,d,q) → DivisorComplement(n,d,r) → q = r

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

Definition DAG

DivisorComplement(n,d,q) · 2

Actual proof prerequisites

mul_left_cancel_nonzero · checked external prerequisite
Original expanded first-order 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

Complete tactic proof in conservative notation

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

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.

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–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 defined 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