PA002D · theorem

positive_quotient_gap_impossible

Stable checked-use theorem · independently closed

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.

Statement with defined notation

∀ m. ∀ q. ∀ q2. ∀ r. ∀ s. ∀ k. Lt(r,m) → S k + q = q2 → ¬m · q + r = m · q2 + s

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt

1 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-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)

Proof neighborhood

Direct theorem prerequisites

PA000F add_comm PA0009 add_assoc PA000A mul_add PA002B add_left_cancel PA002C lt_not_eq_add_middle

Direct theorem dependents

PA002E division_remainder_unique

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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