PA00C5 · theorem

canonical_remainder_from_mod

Alpha v34 checked-use theorem · independently closed; not Stable

A bounded value congruent to an exact division input is its canonical remainder.

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

∀ p. ∀ n. ∀ q. ∀ r. ∀ t. n = p · q + r → Lt(r,p) → Lt(t,p) → ModEq(p,n,t) → r = t

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 PD0008 ModEq

3 occurrences

In local proof propositions

PD0008 ModEq

3 occurrences

Exact expanded native-PA statement
forall p n q r t. n = p * q + r -> (exists gsp_lt_gap_gsd_r_below_p. gsp_lt_gap_gsd_r_below_p + S r = p) -> (exists gsp_lt_gap_gsd_canonical_t_below. gsp_lt_gap_gsd_canonical_t_below + S t = p) -> (exists wpp_mod_left_gsd_n_mod_t wpp_mod_right_gsd_n_mod_t. (n) + p * wpp_mod_left_gsd_n_mod_t = (t) + p * wpp_mod_right_gsd_n_mod_t) -> r = t

Proof neighborhood

Direct theorem prerequisites

PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct theorem dependents

PA00C6 odd_signed_division_branch_exact

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

43 script commands · 6 reading checkpoints · 4 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)
mul commremainder decomposition to mod eqmod eq symmmod eq transmod eq bounded unique
01Fix variables and assumptionsL1–9

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro q
  4. L4
    intro r
  5. L5
    intro t
  6. L6
    intro hdivision
  7. L7
    intro hrbelow
  8. L8
    intro htbelow
  9. L9
    intro hnmodt
02Establish hdirectedL10–15

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul comm.

  1. L10
    have hdirected : n = q * p + r
  2. L11
    trans p * q + r
  3. L12
    exact hdivision
  4. L13
    congr
  5. L14
    apply mul_comm
  6. L15
    refl
03Establish hnmodrL16–22

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.

  1. L16
    have hnmodr : ModEq(p,n,r)Definitions: ModEq(p,n,r)Original native command in the exact edition
  2. L17
    specialize remainder_decomposition_to_mod_eq p
  3. L18
    specialize remainder_decomposition_to_mod_eq n
  4. L19
    specialize remainder_decomposition_to_mod_eq q
  5. L20
    specialize remainder_decomposition_to_mod_eq r
  6. L21
    apply remainder_decomposition_to_mod_eq
  7. L22
    exact hdirected
04Establish hrmodnL23–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq symm.

  1. L23
    have hrmodn : ModEq(p,r,n)Definitions: ModEq(p,r,n)Original native command in the exact edition
  2. L24
    specialize mod_eq_symm p
  3. L25
    specialize mod_eq_symm n
  4. L26
    specialize mod_eq_symm r
  5. L27
    apply mod_eq_symm
  6. L28
    exact hnmodr
05Establish hrmodtL29–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod eq trans.

  1. L29
    have hrmodt : ModEq(p,r,t)Definitions: ModEq(p,r,t)Original native command in the exact edition
  2. L30
    specialize mod_eq_trans p
  3. L31
    specialize mod_eq_trans r
  4. L32
    specialize mod_eq_trans n
  5. L33
    specialize mod_eq_trans t
  6. L34
    apply mod_eq_trans
  7. L35
    exact hrmodn
  8. L36
    exact hnmodt
  9. L37
    specialize mod_eq_bounded_unique p
  10. L38
    specialize mod_eq_bounded_unique r
06Use earlier factsL39–43

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

  1. L39
    specialize mod_eq_bounded_unique t
  2. L40
    apply mod_eq_bounded_unique
  3. L41
    exact hrbelow
  4. L42
    exact htbelow
  5. L43
    exact hrmodt

Library-wide reading audit

Original defined command ledger · 43 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro q
  4. 0004intro r
  5. 0005intro t
  6. 0006intro hdivision
  7. 0007intro hrbelow
  8. 0008intro htbelow
  9. 0009intro hnmodt
  10. 0010have hdirected : n = q * p + r
  11. 0011trans p * q + r
  12. 0012exact hdivision
  13. 0013congr
  14. 0014apply mul_comm
  15. 0015refl
  16. 0016have hnmodr : ModEq(p,n,r)
    Exact native replay linehave hnmodr : exists wpp_mod_left_gsd_proof_n_mod_r wpp_mod_right_gsd_proof_n_mod_r. (n) + p * wpp_mod_left_gsd_proof_n_mod_r = (r) + p * wpp_mod_right_gsd_proof_n_mod_r
  17. 0017specialize remainder_decomposition_to_mod_eq p
  18. 0018specialize remainder_decomposition_to_mod_eq n
  19. 0019specialize remainder_decomposition_to_mod_eq q
  20. 0020specialize remainder_decomposition_to_mod_eq r
  21. 0021apply remainder_decomposition_to_mod_eq
  22. 0022exact hdirected
  23. 0023have hrmodn : ModEq(p,r,n)
    Exact native replay linehave hrmodn : exists wpp_mod_left_gsd_proof_r_mod_n wpp_mod_right_gsd_proof_r_mod_n. (r) + p * wpp_mod_left_gsd_proof_r_mod_n = (n) + p * wpp_mod_right_gsd_proof_r_mod_n
  24. 0024specialize mod_eq_symm p
  25. 0025specialize mod_eq_symm n
  26. 0026specialize mod_eq_symm r
  27. 0027apply mod_eq_symm
  28. 0028exact hnmodr
  29. 0029have hrmodt : ModEq(p,r,t)
    Exact native replay linehave hrmodt : exists wpp_mod_left_gsd_proof_r_mod_t wpp_mod_right_gsd_proof_r_mod_t. (r) + p * wpp_mod_left_gsd_proof_r_mod_t = (t) + p * wpp_mod_right_gsd_proof_r_mod_t
  30. 0030specialize mod_eq_trans p
  31. 0031specialize mod_eq_trans r
  32. 0032specialize mod_eq_trans n
  33. 0033specialize mod_eq_trans t
  34. 0034apply mod_eq_trans
  35. 0035exact hrmodn
  36. 0036exact hnmodt
  37. 0037specialize mod_eq_bounded_unique p
  38. 0038specialize mod_eq_bounded_unique r
  39. 0039specialize mod_eq_bounded_unique t
  40. 0040apply mod_eq_bounded_unique
  41. 0041exact hrbelow
  42. 0042exact htbelow
  43. 0043exact hrmodt