BT001S

positive_quotient_gap_impossible

Stable checked-use theorem · independently kernel verified

A positive gap between quotients makes two bounded-remainder decompositions unequal.

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 original first-admission records.

Exact expanded PA statement

forall m q q2 r s k. (exists z. z + S r = m) -> S k + q = q2 -> ~(m * q + r = m * q2 + s)

Structural proof guide

A positive gap between quotients makes two bounded-remainder decompositions unequal.

Direct prerequisites: add_comm, add_assoc, mul_add, add_left_cancel, lt_not_eq_add_middle. The authored body proceeds by equality transport (4).

Proof neighborhood

Direct dependencies

BT0002 add_comm BT0003 add_assoc BT0007 mul_add BT000V add_left_cancel BT001K lt_not_eq_add_middle

Direct dependents

BT001U division_remainder_unique

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

Read the argument

Proof checkpoints

34 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.

Named ingredients (5)
add commadd assocmul addadd left cancellt not eq add middle
01Fix variables and assumptionsL1–9

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

  1. L1
    intro m
  2. L2
    intro q
  3. L3
    intro q2
  4. L4
    intro r
  5. L5
    intro s
  6. L6
    intro k
  7. L7
    intro hr
  8. L8
    intro hgap
  9. L9
    intro heq
02Use earlier factsL10–19

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

  1. L10
    specialize lt_not_eq_add_middle r
  2. L11
    specialize lt_not_eq_add_middle m
  3. L12
    specialize lt_not_eq_add_middle (m * k)
  4. L13
    specialize lt_not_eq_add_middle s
  5. L14
    apply lt_not_eq_add_middle
  6. L15
    exact hr
  7. L16
    specialize add_left_cancel (m * q)
  8. L17
    specialize add_left_cancel r
  9. L18
    specialize add_left_cancel ((m * k + m) + s)
  10. L19
    apply add_left_cancel
03Calculate and transport equalitiesL20–20

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

  1. L20
    trans m * q2 + s
04Use earlier factsL21–21

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

  1. L21
    exact heq
05Calculate and transport equalitiesL22–22

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

  1. L22
    rewrite <- hgap
06Use earlier factsL23–24

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

  1. L23
    specialize add_comm S k
  2. L24
    specialize add_comm q
07Calculate and transport equalitiesL25–25

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

  1. L25
    rewrite add_comm
08Use earlier factsL26–28

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

  1. L26
    specialize mul_add m
  2. L27
    specialize mul_add q
  3. L28
    specialize mul_add S k
09Calculate and transport equalitiesL29–30

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

  1. L29
    rewrite mul_add
  2. L30
    rewrite PA6
10Use earlier factsL31–34

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

  1. L31
    specialize add_assoc (m * q)
  2. L32
    specialize add_assoc (m * k + m)
  3. L33
    specialize add_assoc s
  4. L34
    apply add_assoc

Library-wide reading audit

Original exact command ledger · 34 lines
  1. 0001intro m
  2. 0002intro q
  3. 0003intro q2
  4. 0004intro r
  5. 0005intro s
  6. 0006intro k
  7. 0007intro hr
  8. 0008intro hgap
  9. 0009intro heq
  10. 0010specialize lt_not_eq_add_middle r
  11. 0011specialize lt_not_eq_add_middle m
  12. 0012specialize lt_not_eq_add_middle (m * k)
  13. 0013specialize lt_not_eq_add_middle s
  14. 0014apply lt_not_eq_add_middle
  15. 0015exact hr
  16. 0016specialize add_left_cancel (m * q)
  17. 0017specialize add_left_cancel r
  18. 0018specialize add_left_cancel ((m * k + m) + s)
  19. 0019apply add_left_cancel
  20. 0020trans m * q2 + s
  21. 0021exact heq
  22. 0022rewrite <- hgap
  23. 0023specialize add_comm S k
  24. 0024specialize add_comm q
  25. 0025rewrite add_comm
  26. 0026specialize mul_add m
  27. 0027specialize mul_add q
  28. 0028specialize mul_add S k
  29. 0029rewrite mul_add
  30. 0030rewrite PA6
  31. 0031specialize add_assoc (m * q)
  32. 0032specialize add_assoc (m * k + m)
  33. 0033specialize add_assoc s
  34. 0034apply add_assoc