TS001C · theorem body

affine_collision_difference_linear_or_opposite

Alpha v34 checked-use · independently kernel and Lean verified; not Stable

Every affine collision and both absolute coordinate differences yield exactly one of the constructive same-sign or opposite-sign linear congruences.

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. ∀ r. ∀ a. ∀ b. ∀ c. ∀ d. ∀ x. ∀ y. ModEq(p,r · a + b,r · c + d) → a = c + x ∨ c = a + x → b = d + y ∨ d = b + y → ModEq(p,r · x,y) ∨ ModEq(p,r · x + y,0)

Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.

Definitions used by this theorem

In the theorem statement

PD0008 ModEq

In local proof propositions

none
Exact expanded first-order statement
forall p r a b c d x y. (exists ftcn_left_collision ftcn_right_collision. (r * a + b) + (p) * ftcn_left_collision = (r * c + d) + (p) * ftcn_right_collision) -> (((a) = (c) + (x) \/ (c) = (a) + (x))) -> (((b) = (d) + (y) \/ (d) = (b) + (y))) -> ((exists ftcn_left_linear ftcn_right_linear. (r * x) + (p) * ftcn_left_linear = (y) + (p) * ftcn_right_linear) \/ (exists ftcn_left_opposite_linear ftcn_right_opposite_linear. (r * x + y) + (p) * ftcn_left_opposite_linear = (0) + (p) * ftcn_right_opposite_linear))

Proof neighborhood

Direct theorem prerequisites

mul_add · Stable closed add_assoc · Stable closed add_comm · Stable closed mod_eq_add_cancel_left · Alpha closed mod_eq_symm · Stable closed

Direct theorem dependents

TS001D affine_collision_absolute_difference_norm_multiple

Definition-aware tactic body

Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.

Read the argument

Proof checkpoints

116 script commands · 26 reading checkpoints · 8 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.

01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro r
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro c
  6. L6
    intro d
  7. L7
    intro x
  8. L8
    intro y
  9. L9
    intro hcollision
  10. L10
    intro hfirst
02Fix variables and assumptionsL11–11

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

  1. L11
    intro hsecond
03Separate the logical casesL12–13

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L12
    cases hfirst
  2. L13
    cases hsecond
04Calculate and transport equalitiesL14–15

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

  1. L14
    rewrite hfirst_left at hcollision
  2. L15
    rewrite hsecond_left at hcollision
05Establish hleftL16–25

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

  1. L16
    have hleft : r * (c + x) + (d + y) = (r * c + d) + (r * x + y)
  2. L17
    simp [mul_add, add_assoc, add_comm]
  3. L18
    trans (r * x + d) + (y + r * c)
  4. L19
    symm
  5. L20
    apply add_assoc
  6. L21
    trans (d + r * x) + (y + r * c)
  7. L22
    congr
  8. L23
    apply add_comm
  9. L24
    refl
  10. L25
    apply add_assoc
06Calculate and transport equalitiesL26–26

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

  1. L26
    rewrite hleft at hcollision
07Separate the logical casesL27–27

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L27
    right
08Use earlier factsL28–32

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

  1. L28
    specialize mod_eq_add_cancel_left p
  2. L29
    specialize mod_eq_add_cancel_left (r * c + d)
  3. L30
    specialize mod_eq_add_cancel_left (r * x + y)
  4. L31
    specialize mod_eq_add_cancel_left 0
  5. L32
    apply mod_eq_add_cancel_left
09Establish hzeroL33–38

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

  1. L33
    have hzero : (r * c + d) + 0 = r * c + d
  2. L34
    simp
  3. L35
    rewrite hzero
  4. L36
    exact hcollision
  5. L37
    rewrite hfirst_left at hcollision
  6. L38
    rewrite hsecond_right at hcollision
10Establish hleftL39–48

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

  1. L39
    have hleft : r * (c + x) + b = (r * c + b) + r * x
  2. L40
    simp [mul_add, add_assoc, add_comm]
  3. L41
    trans (r * x + b) + r * c
  4. L42
    symm
  5. L43
    apply add_assoc
  6. L44
    trans (b + r * x) + r * c
  7. L45
    congr
  8. L46
    apply add_comm
  9. L47
    refl
  10. L48
    apply add_assoc
11Establish hrightL49–53

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

  1. L49
    have hright : r * c + (b + y) = (r * c + b) + y
  2. L50
    symm
  3. L51
    apply add_assoc
  4. L52
    rewrite hleft at hcollision
  5. L53
    rewrite hright at hcollision
12Separate the logical casesL54–54

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L54
    left
13Use earlier factsL55–60

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

  1. L55
    specialize mod_eq_add_cancel_left p
  2. L56
    specialize mod_eq_add_cancel_left (r * c + b)
  3. L57
    specialize mod_eq_add_cancel_left (r * x)
  4. L58
    specialize mod_eq_add_cancel_left y
  5. L59
    apply mod_eq_add_cancel_left
  6. L60
    exact hcollision
14Separate the logical casesL61–61

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L61
    cases hsecond
15Calculate and transport equalitiesL62–63

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

  1. L62
    rewrite hfirst_right at hcollision
  2. L63
    rewrite hsecond_left at hcollision
16Establish hleftL64–66

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

  1. L64
    have hleft : r * a + (d + y) = (r * a + d) + y
  2. L65
    symm
  3. L66
    apply add_assoc
17Establish hrightL67–76

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

  1. L67
    have hright : r * (a + x) + d = (r * a + d) + r * x
  2. L68
    simp [mul_add, add_assoc, add_comm]
  3. L69
    trans (r * x + d) + r * a
  4. L70
    symm
  5. L71
    apply add_assoc
  6. L72
    trans (d + r * x) + r * a
  7. L73
    congr
  8. L74
    apply add_comm
  9. L75
    refl
  10. L76
    apply add_assoc
18Calculate and transport equalitiesL77–78

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

  1. L77
    rewrite hleft at hcollision
  2. L78
    rewrite hright at hcollision
19Separate the logical casesL79–79

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L79
    left
20Use earlier factsL80–89

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

  1. L80
    specialize mod_eq_symm p
  2. L81
    specialize mod_eq_symm y
  3. L82
    specialize mod_eq_symm (r * x)
  4. L83
    apply mod_eq_symm
  5. L84
    specialize mod_eq_add_cancel_left p
  6. L85
    specialize mod_eq_add_cancel_left (r * a + d)
  7. L86
    specialize mod_eq_add_cancel_left y
  8. L87
    specialize mod_eq_add_cancel_left (r * x)
  9. L88
    apply mod_eq_add_cancel_left
  10. L89
    exact hcollision
21Calculate and transport equalitiesL90–91

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

  1. L90
    rewrite hfirst_right at hcollision
  2. L91
    rewrite hsecond_right at hcollision
22Establish hrightL92–101

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

  1. L92
    have hright : r * (a + x) + (b + y) = (r * a + b) + (r * x + y)
  2. L93
    simp [mul_add, add_assoc, add_comm]
  3. L94
    trans (r * x + b) + (y + r * a)
  4. L95
    symm
  5. L96
    apply add_assoc
  6. L97
    trans (b + r * x) + (y + r * a)
  7. L98
    congr
  8. L99
    apply add_comm
  9. L100
    refl
  10. L101
    apply add_assoc
23Calculate and transport equalitiesL102–102

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

  1. L102
    rewrite hright at hcollision
24Separate the logical casesL103–103

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L103
    right
25Use earlier factsL104–112

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

  1. L104
    specialize mod_eq_symm p
  2. L105
    specialize mod_eq_symm 0
  3. L106
    specialize mod_eq_symm (r * x + y)
  4. L107
    apply mod_eq_symm
  5. L108
    specialize mod_eq_add_cancel_left p
  6. L109
    specialize mod_eq_add_cancel_left (r * a + b)
  7. L110
    specialize mod_eq_add_cancel_left 0
  8. L111
    specialize mod_eq_add_cancel_left (r * x + y)
  9. L112
    apply mod_eq_add_cancel_left
26Establish hzeroL113–116

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

  1. L113
    have hzero : (r * a + b) + 0 = r * a + b
  2. L114
    simp
  3. L115
    rewrite hzero
  4. L116
    exact hcollision

Library-wide reading audit

Original defined command ledger · 116 lines
  1. 0001intro p
  2. 0002intro r
  3. 0003intro a
  4. 0004intro b
  5. 0005intro c
  6. 0006intro d
  7. 0007intro x
  8. 0008intro y
  9. 0009intro hcollision
  10. 0010intro hfirst
  11. 0011intro hsecond
  12. 0012cases hfirst
  13. 0013cases hsecond
  14. 0014rewrite hfirst_left at hcollision
  15. 0015rewrite hsecond_left at hcollision
  16. 0016have hleft : r * (c + x) + (d + y) = (r * c + d) + (r * x + y)
  17. 0017simp [mul_add, add_assoc, add_comm]
  18. 0018trans (r * x + d) + (y + r * c)
  19. 0019symm
  20. 0020apply add_assoc
  21. 0021trans (d + r * x) + (y + r * c)
  22. 0022congr
  23. 0023apply add_comm
  24. 0024refl
  25. 0025apply add_assoc
  26. 0026rewrite hleft at hcollision
  27. 0027right
  28. 0028specialize mod_eq_add_cancel_left p
  29. 0029specialize mod_eq_add_cancel_left (r * c + d)
  30. 0030specialize mod_eq_add_cancel_left (r * x + y)
  31. 0031specialize mod_eq_add_cancel_left 0
  32. 0032apply mod_eq_add_cancel_left
  33. 0033have hzero : (r * c + d) + 0 = r * c + d
  34. 0034simp
  35. 0035rewrite hzero
  36. 0036exact hcollision
  37. 0037rewrite hfirst_left at hcollision
  38. 0038rewrite hsecond_right at hcollision
  39. 0039have hleft : r * (c + x) + b = (r * c + b) + r * x
  40. 0040simp [mul_add, add_assoc, add_comm]
  41. 0041trans (r * x + b) + r * c
  42. 0042symm
  43. 0043apply add_assoc
  44. 0044trans (b + r * x) + r * c
  45. 0045congr
  46. 0046apply add_comm
  47. 0047refl
  48. 0048apply add_assoc
  49. 0049have hright : r * c + (b + y) = (r * c + b) + y
  50. 0050symm
  51. 0051apply add_assoc
  52. 0052rewrite hleft at hcollision
  53. 0053rewrite hright at hcollision
  54. 0054left
  55. 0055specialize mod_eq_add_cancel_left p
  56. 0056specialize mod_eq_add_cancel_left (r * c + b)
  57. 0057specialize mod_eq_add_cancel_left (r * x)
  58. 0058specialize mod_eq_add_cancel_left y
  59. 0059apply mod_eq_add_cancel_left
  60. 0060exact hcollision
  61. 0061cases hsecond
  62. 0062rewrite hfirst_right at hcollision
  63. 0063rewrite hsecond_left at hcollision
  64. 0064have hleft : r * a + (d + y) = (r * a + d) + y
  65. 0065symm
  66. 0066apply add_assoc
  67. 0067have hright : r * (a + x) + d = (r * a + d) + r * x
  68. 0068simp [mul_add, add_assoc, add_comm]
  69. 0069trans (r * x + d) + r * a
  70. 0070symm
  71. 0071apply add_assoc
  72. 0072trans (d + r * x) + r * a
  73. 0073congr
  74. 0074apply add_comm
  75. 0075refl
  76. 0076apply add_assoc
  77. 0077rewrite hleft at hcollision
  78. 0078rewrite hright at hcollision
  79. 0079left
  80. 0080specialize mod_eq_symm p
  81. 0081specialize mod_eq_symm y
  82. 0082specialize mod_eq_symm (r * x)
  83. 0083apply mod_eq_symm
  84. 0084specialize mod_eq_add_cancel_left p
  85. 0085specialize mod_eq_add_cancel_left (r * a + d)
  86. 0086specialize mod_eq_add_cancel_left y
  87. 0087specialize mod_eq_add_cancel_left (r * x)
  88. 0088apply mod_eq_add_cancel_left
  89. 0089exact hcollision
  90. 0090rewrite hfirst_right at hcollision
  91. 0091rewrite hsecond_right at hcollision
  92. 0092have hright : r * (a + x) + (b + y) = (r * a + b) + (r * x + y)
  93. 0093simp [mul_add, add_assoc, add_comm]
  94. 0094trans (r * x + b) + (y + r * a)
  95. 0095symm
  96. 0096apply add_assoc
  97. 0097trans (b + r * x) + (y + r * a)
  98. 0098congr
  99. 0099apply add_comm
  100. 0100refl
  101. 0101apply add_assoc
  102. 0102rewrite hright at hcollision
  103. 0103right
  104. 0104specialize mod_eq_symm p
  105. 0105specialize mod_eq_symm 0
  106. 0106specialize mod_eq_symm (r * x + y)
  107. 0107apply mod_eq_symm
  108. 0108specialize mod_eq_add_cancel_left p
  109. 0109specialize mod_eq_add_cancel_left (r * a + b)
  110. 0110specialize mod_eq_add_cancel_left 0
  111. 0111specialize mod_eq_add_cancel_left (r * x + y)
  112. 0112apply mod_eq_add_cancel_left
  113. 0113have hzero : (r * a + b) + 0 = r * a + b
  114. 0114simp
  115. 0115rewrite hzero
  116. 0116exact hcollision