PA007B · theorem

gauss_mixed_sign_scaled_source_impossible

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

Opposite signed representatives cannot share one magnitude when their positive source sum is below p.

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. ∀ h. ∀ a. ∀ x. ∀ y. ∀ m. p = 2 · h + 1 → Prime(p) → ¬Dvd(p,a) → Lt(x + y,p) → ¬x + y = 0 → ModEq(p,a · x,m) → ¬ModEq(p,a · y,2 · h · m)

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 PD0003 Dvd PD0004 Prime PD0008 ModEq

5 occurrences

In local proof propositions

PD0002 Lt PD0008 ModEq

7 occurrences

Exact expanded native-PA statement
forall p h a x y m. p = 2 * h + 1 -> ((~(p = 1) /\ forall gsp_prime_left_collision_prime gsp_prime_right_collision_prime. p = gsp_prime_left_collision_prime * gsp_prime_right_collision_prime -> gsp_prime_left_collision_prime = 1 \/ gsp_prime_right_collision_prime = 1)) -> (~(exists gsp_divisor_factor_collision_multiplier. a = p * gsp_divisor_factor_collision_multiplier)) -> (exists gsp_lt_gap_mixed_sum_bound. gsp_lt_gap_mixed_sum_bound + S (x + y) = p) -> ~(x + y = 0) -> (exists gmp_mod_left_mixed_x_lower gmp_mod_right_mixed_x_lower. (a * x) + p * gmp_mod_left_mixed_x_lower = (m) + p * gmp_mod_right_mixed_x_lower) -> (exists gmp_mod_left_mixed_y_reflected gmp_mod_right_mixed_y_reflected. (a * y) + p * gmp_mod_left_mixed_y_reflected = ((2 * h) * m) + p * gmp_mod_right_mixed_y_reflected) -> false

Proof neighborhood

Direct theorem prerequisites

PA0022 mod_eq_add PA000A mul_add PA000G mul_succ_left PA000F add_comm PA0021 dvd_to_mod_zero PA0024 mod_eq_trans PA003S prime_mod_cancel PA0031 prime_nonzero PA002L one_le_of_ne_zero PA002U mod_eq_bounded_unique

Direct theorem dependents

PA007C gauss_signed_half_magnitude_injective

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

90 script commands · 25 reading checkpoints · 9 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 (8)
mod eq addmul adddvd to mod zeromod eq transprime mod cancelprime nonzeroone le of ne zeromod eq bounded unique
01Fix variables and assumptionsL1–10

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

  1. L1
    intro p
  2. L2
    intro h
  3. L3
    intro a
  4. L4
    intro x
  5. L5
    intro y
  6. L6
    intro m
  7. L7
    intro hpodd
  8. L8
    intro hp
  9. L9
    intro hnotdiv
  10. L10
    intro hsum_bound
02Fix variables and assumptionsL11–13

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

  1. L11
    intro hsum_nonzero
  2. L12
    intro hxlower
  3. L13
    intro hyreflected
03Establish haddL14–22

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

  1. L14
    have hadd : ModEq(p,a · x + a · y,m + 2 · h · m)Definitions: ModEq(p,a · x + a · y,m + 2 · h · m)Original native command in the exact edition
  2. L15
    specialize mod_eq_add p
  3. L16
    specialize mod_eq_add (a * x)
  4. L17
    specialize mod_eq_add m
  5. L18
    specialize mod_eq_add (a * y)
  6. L19
    specialize mod_eq_add (2 * h) * m
  7. L20
    apply mod_eq_add
  8. L21
    exact hxlower
  9. L22
    exact hyreflected
04Separate the logical casesL23–24

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

  1. L23
    cases hadd
  2. L24
    cases hadd_witness
05Establish hscaled_multipleL25–25

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

  1. L25
    have hscaled_multiple : ModEq(p,a · (x + y),p · m)Definitions: ModEq(p,a · (x + y),p · m)Original native command in the exact edition
06Construct an explicit witnessL26–27

Supply the displayed value, then prove that it has the required property.

  1. L26
    exists x1
  2. L27
    exists x2
07Calculate and transport equalitiesL28–29

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

  1. L28
    trans (a * x + a * y) + p * x1
  2. L29
    congr
08Use earlier factsL30–30

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

  1. L30
    apply mul_add
09Calculate and transport equalitiesL31–32

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

  1. L31
    refl
  2. L32
    trans (m + (2 * h) * m) + p * x2
10Use earlier factsL33–33

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

  1. L33
    exact hadd_witness_witness
11Calculate and transport equalitiesL34–37

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

  1. L34
    congr
  2. L35
    rewrite hpodd
  3. L36
    simp [mul_succ_left, add_comm]
  4. L37
    refl
12Establish hmultiple_zeroL38–41

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

  1. L38
    have hmultiple_zero : ModEq(p,p · m,0)Definitions: ModEq(p,p · m,0)Original native command in the exact edition
  2. L39
    specialize dvd_to_mod_zero p
  3. L40
    specialize dvd_to_mod_zero (p * m)
  4. L41
    apply dvd_to_mod_zero
13Construct an explicit witnessL42–42

Supply the displayed value, then prove that it has the required property.

  1. L42
    exists m
14Calculate and transport equalitiesL43–43

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

  1. L43
    refl
15Establish hscaled_zeroL44–51

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

  1. L44
    have hscaled_zero : ModEq(p,a · (x + y),0)Definitions: ModEq(p,a · (x + y),0)Original native command in the exact edition
  2. L45
    specialize mod_eq_trans p
  3. L46
    specialize mod_eq_trans (a * (x + y))
  4. L47
    specialize mod_eq_trans (p * m)
  5. L48
    specialize mod_eq_trans 0
  6. L49
    apply mod_eq_trans
  7. L50
    exact hscaled_multiple
  8. L51
    exact hmultiple_zero
16Separate the logical casesL52–53

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

  1. L52
    cases hscaled_zero
  2. L53
    cases hscaled_zero_witness
17Establish hscaled_factor_zeroL54–54

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

  1. L54
    have hscaled_factor_zero : ModEq(p,a · (x + y),a · 0)Definitions: ModEq(p,a · (x + y),a · 0)Original native command in the exact edition
18Construct an explicit witnessL55–56

Supply the displayed value, then prove that it has the required property.

  1. L55
    exists x3
  2. L56
    exists x4
19Calculate and transport equalitiesL57–57

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

  1. L57
    trans 0 + p * x4
20Use earlier factsL58–58

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

  1. L58
    exact hscaled_zero_witness_witness
21Calculate and transport equalitiesL59–61

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

  1. L59
    congr
  2. L60
    simp
  3. L61
    refl
22Establish hsum_zero_modL62–70

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

  1. L62
    have hsum_zero_mod : ModEq(p,x + y,0)Definitions: ModEq(p,x + y,0)Original native command in the exact edition
  2. L63
    specialize prime_mod_cancel p
  3. L64
    specialize prime_mod_cancel a
  4. L65
    specialize prime_mod_cancel (x + y)
  5. L66
    specialize prime_mod_cancel 0
  6. L67
    apply prime_mod_cancel
  7. L68
    exact hp
  8. L69
    exact hnotdiv
  9. L70
    exact hscaled_factor_zero
23Establish hp0L71–76

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

  1. L71
    have hp0 : ~(p = 0)
  2. L72
    intro hpzero
  3. L73
    specialize prime_nonzero p
  4. L74
    apply prime_nonzero
  5. L75
    exact hp
  6. L76
    exact hpzero
24Establish hzero_boundL77–80

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply one le of ne zero.

  1. L77
    have hzero_bound : Lt(0,p)Definitions: Lt(0,p)Original native command in the exact edition
  2. L78
    specialize one_le_of_ne_zero p
  3. L79
    apply one_le_of_ne_zero
  4. L80
    exact hp0
25Establish hsum_zeroL81–90

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

  1. L81
    have hsum_zero : x + y = 0
  2. L82
    specialize mod_eq_bounded_unique p
  3. L83
    specialize mod_eq_bounded_unique (x + y)
  4. L84
    specialize mod_eq_bounded_unique 0
  5. L85
    apply mod_eq_bounded_unique
  6. L86
    exact hsum_bound
  7. L87
    exact hzero_bound
  8. L88
    exact hsum_zero_mod
  9. L89
    apply hsum_nonzero
  10. L90
    exact hsum_zero

Library-wide reading audit

Original defined command ledger · 90 lines
  1. 0001intro p
  2. 0002intro h
  3. 0003intro a
  4. 0004intro x
  5. 0005intro y
  6. 0006intro m
  7. 0007intro hpodd
  8. 0008intro hp
  9. 0009intro hnotdiv
  10. 0010intro hsum_bound
  11. 0011intro hsum_nonzero
  12. 0012intro hxlower
  13. 0013intro hyreflected
  14. 0014have hadd : ModEq(p,a · x + a · y,m + 2 · h · m)
    Exact native replay linehave hadd : exists gmp_mod_left_mixed_added gmp_mod_right_mixed_added. (a * x + a * y) + p * gmp_mod_left_mixed_added = (m + (2 * h) * m) + p * gmp_mod_right_mixed_added
  15. 0015specialize mod_eq_add p
  16. 0016specialize mod_eq_add (a * x)
  17. 0017specialize mod_eq_add m
  18. 0018specialize mod_eq_add (a * y)
  19. 0019specialize mod_eq_add (2 * h) * m
  20. 0020apply mod_eq_add
  21. 0021exact hxlower
  22. 0022exact hyreflected
  23. 0023cases hadd
  24. 0024cases hadd_witness
  25. 0025have hscaled_multiple : ModEq(p,a · (x + y),p · m)
    Exact native replay linehave hscaled_multiple : exists gmp_mod_left_mixed_scaled_sum_multiple gmp_mod_right_mixed_scaled_sum_multiple. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_multiple = (p * m) + p * gmp_mod_right_mixed_scaled_sum_multiple
  26. 0026exists x1
  27. 0027exists x2
  28. 0028trans (a * x + a * y) + p * x1
  29. 0029congr
  30. 0030apply mul_add
  31. 0031refl
  32. 0032trans (m + (2 * h) * m) + p * x2
  33. 0033exact hadd_witness_witness
  34. 0034congr
  35. 0035rewrite hpodd
  36. 0036simp [mul_succ_left, add_comm]
  37. 0037refl
  38. 0038have hmultiple_zero : ModEq(p,p · m,0)
    Exact native replay linehave hmultiple_zero : exists gmp_mod_left_mixed_multiple_zero gmp_mod_right_mixed_multiple_zero. (p * m) + p * gmp_mod_left_mixed_multiple_zero = (0) + p * gmp_mod_right_mixed_multiple_zero
  39. 0039specialize dvd_to_mod_zero p
  40. 0040specialize dvd_to_mod_zero (p * m)
  41. 0041apply dvd_to_mod_zero
  42. 0042exists m
  43. 0043refl
  44. 0044have hscaled_zero : ModEq(p,a · (x + y),0)
    Exact native replay linehave hscaled_zero : exists gmp_mod_left_mixed_scaled_sum_zero gmp_mod_right_mixed_scaled_sum_zero. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_zero = (0) + p * gmp_mod_right_mixed_scaled_sum_zero
  45. 0045specialize mod_eq_trans p
  46. 0046specialize mod_eq_trans (a * (x + y))
  47. 0047specialize mod_eq_trans (p * m)
  48. 0048specialize mod_eq_trans 0
  49. 0049apply mod_eq_trans
  50. 0050exact hscaled_multiple
  51. 0051exact hmultiple_zero
  52. 0052cases hscaled_zero
  53. 0053cases hscaled_zero_witness
  54. 0054have hscaled_factor_zero : ModEq(p,a · (x + y),a · 0)
    Exact native replay linehave hscaled_factor_zero : exists gmp_mod_left_mixed_scaled_sum_factor_zero gmp_mod_right_mixed_scaled_sum_factor_zero. (a * (x + y)) + p * gmp_mod_left_mixed_scaled_sum_factor_zero = (a * 0) + p * gmp_mod_right_mixed_scaled_sum_factor_zero
  55. 0055exists x3
  56. 0056exists x4
  57. 0057trans 0 + p * x4
  58. 0058exact hscaled_zero_witness_witness
  59. 0059congr
  60. 0060simp
  61. 0061refl
  62. 0062have hsum_zero_mod : ModEq(p,x + y,0)
    Exact native replay linehave hsum_zero_mod : exists gmp_mod_left_mixed_sum_zero gmp_mod_right_mixed_sum_zero. (x + y) + p * gmp_mod_left_mixed_sum_zero = (0) + p * gmp_mod_right_mixed_sum_zero
  63. 0063specialize prime_mod_cancel p
  64. 0064specialize prime_mod_cancel a
  65. 0065specialize prime_mod_cancel (x + y)
  66. 0066specialize prime_mod_cancel 0
  67. 0067apply prime_mod_cancel
  68. 0068exact hp
  69. 0069exact hnotdiv
  70. 0070exact hscaled_factor_zero
  71. 0071have hp0 : ~(p = 0)
  72. 0072intro hpzero
  73. 0073specialize prime_nonzero p
  74. 0074apply prime_nonzero
  75. 0075exact hp
  76. 0076exact hpzero
  77. 0077have hzero_bound : Lt(0,p)
    Exact native replay linehave hzero_bound : exists gsp_lt_gap_mixed_zero_bound. gsp_lt_gap_mixed_zero_bound + S 0 = p
  78. 0078specialize one_le_of_ne_zero p
  79. 0079apply one_le_of_ne_zero
  80. 0080exact hp0
  81. 0081have hsum_zero : x + y = 0
  82. 0082specialize mod_eq_bounded_unique p
  83. 0083specialize mod_eq_bounded_unique (x + y)
  84. 0084specialize mod_eq_bounded_unique 0
  85. 0085apply mod_eq_bounded_unique
  86. 0086exact hsum_bound
  87. 0087exact hzero_bound
  88. 0088exact hsum_zero_mod
  89. 0089apply hsum_nonzero
  90. 0090exact hsum_zero