PA00AK · theorem

bounded_mod_inverse_unique

Stable checked-use theorem · independently closed

Two bounded inverses of the same residue are equal.

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. ∀ x. ∀ y. ∀ z. Lt(y,p) → Lt(z,p) → BalancedInverse(p,x,y) → BalancedInverse(p,x,z) → y = z

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 PD0031 BalancedInverse

4 occurrences

In local proof propositions

PD0008 ModEq

4 occurrences

Exact expanded native-PA statement
forall p x y z. (exists wip_strict_gap_unique_y_bound. wip_strict_gap_unique_y_bound + S y = p) -> (exists wip_strict_gap_unique_z_bound. wip_strict_gap_unique_z_bound + S z = p) -> (exists wip_mod_left_unique_xy wip_mod_right_unique_xy. x * y + p * wip_mod_left_unique_xy = 1 + p * wip_mod_right_unique_xy) -> (exists wip_mod_left_unique_xz wip_mod_right_unique_xz. x * z + p * wip_mod_left_unique_xz = 1 + p * wip_mod_right_unique_xz) -> y = z

Proof neighborhood

Direct theorem prerequisites

PA003L mod_eq_symm PA0020 mod_eq_mul_left PA001Y mod_eq_mul_right PA000B mul_assoc PA000H mul_comm PA0002 mul_one PA000M one_mul PA0024 mod_eq_trans PA002U mod_eq_bounded_unique

Direct theorem dependents

PA00AL bounded_inverse_index_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

62 script commands · 9 reading checkpoints · 7 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 (9)
mod eq symmmod eq mul leftmod eq mul rightmul assocmul commmul oneone mulmod eq transmod eq bounded unique
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro x
  3. L3
    intro y
  4. L4
    intro z
  5. L5
    intro hy
  6. L6
    intro hz
  7. L7
    intro hxy
  8. L8
    intro hxz
02Establish hreverseL9–14

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

  1. L9
    have hreverse : ModEq(p,1,x · z)Definitions: ModEq(p,1,x · z)Original native command in the exact edition
  2. L10
    specialize mod_eq_symm p
  3. L11
    specialize mod_eq_symm (x * z)
  4. L12
    specialize mod_eq_symm 1
  5. L13
    apply mod_eq_symm
  6. L14
    exact hxz
03Establish hleftscaledL15–21

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

  1. L15
    have hleftscaled : ModEq(p,y · 1,y · (x · z))Definitions: ModEq(p,y · 1,y · (x · z))Original native command in the exact edition
  2. L16
    specialize mod_eq_mul_left p
  3. L17
    specialize mod_eq_mul_left 1
  4. L18
    specialize mod_eq_mul_left (x * z)
  5. L19
    specialize mod_eq_mul_left y
  6. L20
    apply mod_eq_mul_left
  7. L21
    exact hreverse
04Establish hrightscaledL22–28

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

  1. L22
    have hrightscaled : ModEq(p,x · y · z,1 · z)Definitions: ModEq(p,x · y · z,1 · z)Original native command in the exact edition
  2. L23
    specialize mod_eq_mul_right p
  3. L24
    specialize mod_eq_mul_right (x * y)
  4. L25
    specialize mod_eq_mul_right 1
  5. L26
    specialize mod_eq_mul_right z
  6. L27
    apply mod_eq_mul_right
  7. L28
    exact hxy
05Establish hleftL29–31

Establish this local claim before using it. It is not an additional assumption.

  1. L29
    have hleft : y * 1 = y
  2. L30
    specialize mul_one y
  3. L31
    exact mul_one
06Establish hmiddleL32–41

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

  1. L32
    have hmiddle : y * (x * z) = (x * y) * z
  2. L33
    trans (y * x) * z
  3. L34
    symm
  4. L35
    specialize mul_assoc y
  5. L36
    specialize mul_assoc x
  6. L37
    specialize mul_assoc z
  7. L38
    apply mul_assoc
  8. L39
    congr
  9. L40
    apply mul_comm
  10. L41
    refl
07Establish hrightL42–47

Establish this local claim before using it. It is not an additional assumption.

  1. L42
    have hright : 1 * z = z
  2. L43
    specialize one_mul z
  3. L44
    exact one_mul
  4. L45
    rewrite hleft at hleftscaled
  5. L46
    rewrite hmiddle at hleftscaled
  6. L47
    rewrite hright at hrightscaled
08Establish hyzL48–57

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

  1. L48
  2. L49
    specialize mod_eq_trans p
  3. L50
    specialize mod_eq_trans y
  4. L51
    specialize mod_eq_trans ((x * y) * z)
  5. L52
    specialize mod_eq_trans z
  6. L53
    apply mod_eq_trans
  7. L54
    exact hleftscaled
  8. L55
    exact hrightscaled
  9. L56
    specialize mod_eq_bounded_unique p
  10. L57
    specialize mod_eq_bounded_unique y
09Use earlier factsL58–62

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

  1. L58
    specialize mod_eq_bounded_unique z
  2. L59
    apply mod_eq_bounded_unique
  3. L60
    exact hy
  4. L61
    exact hz
  5. L62
    exact hyz

Library-wide reading audit

Original defined command ledger · 62 lines
  1. 0001intro p
  2. 0002intro x
  3. 0003intro y
  4. 0004intro z
  5. 0005intro hy
  6. 0006intro hz
  7. 0007intro hxy
  8. 0008intro hxz
  9. 0009have hreverse : ModEq(p,1,x · z)
    Exact native replay linehave hreverse : exists wip_mod_left_unique_reverse_xz wip_mod_right_unique_reverse_xz. 1 + p * wip_mod_left_unique_reverse_xz = x * z + p * wip_mod_right_unique_reverse_xz
  10. 0010specialize mod_eq_symm p
  11. 0011specialize mod_eq_symm (x * z)
  12. 0012specialize mod_eq_symm 1
  13. 0013apply mod_eq_symm
  14. 0014exact hxz
  15. 0015have hleftscaled : ModEq(p,y · 1,y · (x · z))
    Exact native replay linehave hleftscaled : exists wip_mod_left_unique_left_scaled wip_mod_right_unique_left_scaled. y * 1 + p * wip_mod_left_unique_left_scaled = y * (x * z) + p * wip_mod_right_unique_left_scaled
  16. 0016specialize mod_eq_mul_left p
  17. 0017specialize mod_eq_mul_left 1
  18. 0018specialize mod_eq_mul_left (x * z)
  19. 0019specialize mod_eq_mul_left y
  20. 0020apply mod_eq_mul_left
  21. 0021exact hreverse
  22. 0022have hrightscaled : ModEq(p,x · y · z,1 · z)
    Exact native replay linehave hrightscaled : exists wip_mod_left_unique_right_scaled wip_mod_right_unique_right_scaled. (x * y) * z + p * wip_mod_left_unique_right_scaled = 1 * z + p * wip_mod_right_unique_right_scaled
  23. 0023specialize mod_eq_mul_right p
  24. 0024specialize mod_eq_mul_right (x * y)
  25. 0025specialize mod_eq_mul_right 1
  26. 0026specialize mod_eq_mul_right z
  27. 0027apply mod_eq_mul_right
  28. 0028exact hxy
  29. 0029have hleft : y * 1 = y
  30. 0030specialize mul_one y
  31. 0031exact mul_one
  32. 0032have hmiddle : y * (x * z) = (x * y) * z
  33. 0033trans (y * x) * z
  34. 0034symm
  35. 0035specialize mul_assoc y
  36. 0036specialize mul_assoc x
  37. 0037specialize mul_assoc z
  38. 0038apply mul_assoc
  39. 0039congr
  40. 0040apply mul_comm
  41. 0041refl
  42. 0042have hright : 1 * z = z
  43. 0043specialize one_mul z
  44. 0044exact one_mul
  45. 0045rewrite hleft at hleftscaled
  46. 0046rewrite hmiddle at hleftscaled
  47. 0047rewrite hright at hrightscaled
  48. 0048have hyz : ModEq(p,y,z)
    Exact native replay linehave hyz : exists wip_mod_left_unique_result wip_mod_right_unique_result. y + p * wip_mod_left_unique_result = z + p * wip_mod_right_unique_result
  49. 0049specialize mod_eq_trans p
  50. 0050specialize mod_eq_trans y
  51. 0051specialize mod_eq_trans ((x * y) * z)
  52. 0052specialize mod_eq_trans z
  53. 0053apply mod_eq_trans
  54. 0054exact hleftscaled
  55. 0055exact hrightscaled
  56. 0056specialize mod_eq_bounded_unique p
  57. 0057specialize mod_eq_bounded_unique y
  58. 0058specialize mod_eq_bounded_unique z
  59. 0059apply mod_eq_bounded_unique
  60. 0060exact hy
  61. 0061exact hz
  62. 0062exact hyz