PA00C5

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.

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

Structural proof guide

Generated structural guide

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

Use the direct prerequisites mul_comm, remainder_decomposition_to_mod_eq, mod_eq_symm, mod_eq_trans, mod_eq_bounded_unique as previously established PA formulas.

The proof proceeds by intermediate claims (4).

Referenced ingredients

PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Proof neighborhood

Direct dependencies

PA000H mul_comm PA003C remainder_decomposition_to_mod_eq PA003L mod_eq_symm PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct dependents

PA00C6 odd_signed_division_branch_exact

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.

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.

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 : 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
  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 : 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
  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 : 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
  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 exact 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 : 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 : 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 : 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