TS0026 · theorem body

three_mod_four_prime_norm_divisor_forces_second_coordinate

Alpha v34 checked-use · independently kernel and Lean verified; 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.

Statement with defined notation

∀ p. ∀ n. ∀ a. ∀ b. p = S n → Prime(p) → Mod4Three(p) → Dvd(p,a · a + b · b) → Dvd(p,b)

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

PD0003 Dvd PD0004 Prime PD0012 Mod4Three

In local proof propositions

PD0003 Dvd PD0005 Coprime PD0010 Odd PD0021 QRes
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

prime_coprime_or_divides · Stable closed multiple_refl · Stable closed mod4_three_is_odd · Stable closed TS0024 prime_divisible_two_square_norm_unit_coordinate_yields_negative_one_root TS0025 three_mod_four_prime_has_no_negative_one_root

Direct theorem dependents

TS0027 three_mod_four_prime_divides_two_square_norm_divides_both

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

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.

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 (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 : Coprime(p,b) ∨ Dvd(p,b)Definitions: Coprime(p,b)Dvd(p,b)Original native command in the exact edition
  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 : ¬Dvd(p,b)Definitions: Dvd(p,b)Original native command in the exact edition
  2. L17
    intro hdivides
05Establish hpdividesL18–20

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

  1. L18
    have hpdivides : Dvd(p,p)Definitions: Dvd(p,p)Original native command in the exact edition
  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
  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
  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 defined 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 : Coprime(p,b) ∨ Dvd(p,b)
    Exact native replay linehave 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 : ¬Dvd(p,b)
    Exact native replay linehave hunit : ~(exists k. b = p * k)
  17. 0017intro hdivides
  18. 0018have hpdivides : Dvd(p,p)
    Exact native replay linehave 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 : Odd(p)
    Exact native replay linehave 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 : QRes(p,n)
    Exact native replay linehave 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