TS0026

three_mod_four_prime_norm_divisor_forces_second_coordinate

Alpha v34 independently verified · alpha_closed; checked-use authorized; not Stable

A three-modulo-four prime dividing a²+b² must divide the second coordinate, by the constructive first supplementary law.

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 first-order arithmetic statement

forall p n a b. p = S n -> ((~(p = 1) /\ forall frm_prime_left_ftsc_prime frm_prime_right_ftsc_prime. p = frm_prime_left_ftsc_prime * frm_prime_right_ftsc_prime -> frm_prime_left_ftsc_prime = 1 \/ frm_prime_right_ftsc_prime = 1)) -> (exists ftsc_four_three_ftsc_prime. (p) = 4 * ftsc_four_three_ftsc_prime + 3) -> (exists ftcn_factor_ftsc_norm. (a * a + b * b) = (p) * ftcn_factor_ftsc_norm) -> (exists ftcn_factor_ftsc_second_result. (b) = (p) * ftcn_factor_ftsc_second_result)

Constructive proof overview

Generated structural guide

A three-modulo-four prime dividing a²+b² must divide the second coordinate, by the constructive first supplementary law.

The unchanged tactic script uses 5 declared prerequisites and contains 51 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

prime_coprime_or_divides Stable theorem; checked-use authorized multiple_refl Stable theorem; checked-use authorized mod4_three_is_odd Stable theorem; checked-use authorized TS0024 prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root TS0025 three_mod_four_prime_has_no_negative_one_root

Direct dependents

TS0027 three_mod_four_prime_divides_two_square_norm_divides_both

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This exact body belongs to a complete independently kernel-checked constructive proof bundle and has Alpha checked-use authority; it does not imply Stable membership.

Read the argument

Proof checkpoints

51 script commands · 11 reading checkpoints · 6 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 (2)
prime divisible two square norm unit coordinate yields negative one rootthree mod four prime has no negative one root
01Fix variables and assumptionsL1–8

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro a
  4. L4
    intro b
  5. L5
    intro hpredecessor
  6. L6
    intro hprime
  7. L7
    intro hthree
  8. L8
    intro hnorm
02Establish hsplitL9–13

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

  1. L9
    have hsplit : (forall d. (exists u. p = d * u) -> (exists v. b = d * v) -> d = 1) \/ (exists k. b = p * k)
  2. L10
    specialize prime_coprime_or_divides p
  3. L11
    specialize prime_coprime_or_divides b
  4. L12
    apply prime_coprime_or_divides
  5. L13
    exact hprime
03Separate the logical casesL14–15

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

  1. L14
    cases hsplit
  2. L15
    exfalso
04Establish hunitL16–17

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

  1. L16
    have hunit : ~(exists k. b = p * k)
  2. L17
    intro hdivides
05Establish hpdividesL18–20

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

  1. L18
    have hpdivides : exists k. p = p * k
  2. L19
    specialize multiple_refl p
  3. L20
    exact multiple_refl
06Establish hponeL21–25

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

  1. L21
    have hpone : p = 1
  2. L22
    specialize hsplit_left p
  3. L23
    apply hsplit_left
  4. L24
    exact hpdivides
  5. L25
    exact hdivides
07Separate the logical casesL26–26

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

  1. L26
    cases hprime
08Use earlier factsL27–28

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

  1. L27
    apply hprime_left
  2. L28
    exact hpone
09Establish hoddL29–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mod4 three is odd.

  1. L29
    have hodd : exists ftsc_odd_ftsc_prime. (p) = 2 * ftsc_odd_ftsc_prime + 1
  2. L30
    specialize mod4_three_is_odd p
  3. L31
    apply mod4_three_is_odd
  4. L32
    exact hthree
10Establish hrootL33–42

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime divisible two square norm unit coordinate yields negative one root.

  1. L33
    have hroot : exists qr_x_ftsc_predecessor. exists qr_u_ftsc_predecessor qr_v_ftsc_predecessor. qr_x_ftsc_predecessor * qr_x_ftsc_predecessor + p * qr_u_ftsc_predecessor = n + p * qr_v_ftsc_predecessor
  2. L34
    specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root p
  3. L35
    specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root n
  4. L36
    specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root a
  5. L37
    specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root b
  6. L38
    apply prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root
  7. L39
    exact hpredecessor
  8. L40
    exact hprime
  9. L41
    exact hnorm
  10. L42
    exact hunit
11Use earlier factsL43–51

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

  1. L43
    specialize three_mod_four_prime_has_no_negative_one_root p
  2. L44
    specialize three_mod_four_prime_has_no_negative_one_root n
  3. L45
    apply three_mod_four_prime_has_no_negative_one_root
  4. L46
    exact hpredecessor
  5. L47
    exact hprime
  6. L48
    exact hodd
  7. L49
    exact hthree
  8. L50
    exact hroot
  9. L51
    exact hsplit_right

Library-wide reading audit

Original exact command ledger · 51 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro a
  4. 0004intro b
  5. 0005intro hpredecessor
  6. 0006intro hprime
  7. 0007intro hthree
  8. 0008intro hnorm
  9. 0009have hsplit : (forall d. (exists u. p = d * u) -> (exists v. b = d * v) -> d = 1) \/ (exists k. b = p * k)
  10. 0010specialize prime_coprime_or_divides p
  11. 0011specialize prime_coprime_or_divides b
  12. 0012apply prime_coprime_or_divides
  13. 0013exact hprime
  14. 0014cases hsplit
  15. 0015exfalso
  16. 0016have hunit : ~(exists k. b = p * k)
  17. 0017intro hdivides
  18. 0018have hpdivides : exists k. p = p * k
  19. 0019specialize multiple_refl p
  20. 0020exact multiple_refl
  21. 0021have hpone : p = 1
  22. 0022specialize hsplit_left p
  23. 0023apply hsplit_left
  24. 0024exact hpdivides
  25. 0025exact hdivides
  26. 0026cases hprime
  27. 0027apply hprime_left
  28. 0028exact hpone
  29. 0029have hodd : exists ftsc_odd_ftsc_prime. (p) = 2 * ftsc_odd_ftsc_prime + 1
  30. 0030specialize mod4_three_is_odd p
  31. 0031apply mod4_three_is_odd
  32. 0032exact hthree
  33. 0033have hroot : exists qr_x_ftsc_predecessor. exists qr_u_ftsc_predecessor qr_v_ftsc_predecessor. qr_x_ftsc_predecessor * qr_x_ftsc_predecessor + p * qr_u_ftsc_predecessor = n + p * qr_v_ftsc_predecessor
  34. 0034specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root p
  35. 0035specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root n
  36. 0036specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root a
  37. 0037specialize prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root b
  38. 0038apply prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root
  39. 0039exact hpredecessor
  40. 0040exact hprime
  41. 0041exact hnorm
  42. 0042exact hunit
  43. 0043specialize three_mod_four_prime_has_no_negative_one_root p
  44. 0044specialize three_mod_four_prime_has_no_negative_one_root n
  45. 0045apply three_mod_four_prime_has_no_negative_one_root
  46. 0046exact hpredecessor
  47. 0047exact hprime
  48. 0048exact hodd
  49. 0049exact hthree
  50. 0050exact hroot
  51. 0051exact hsplit_right