TS0028 · theorem body

prime_is_two_squares_iff_two_or_one_mod_four

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

A prime has a natural two-square representation exactly when it is two or congruent to one modulo four.

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. Prime(p) → ((∃ x. ∃ y. p = x · x + y · y) → p = 2 ∨ Mod4One(p)) ∧ (p = 2 ∨ Mod4One(p) → ∃ x. ∃ y. p = x · x + y · y)

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

PD0004 Prime PD0011 Mod4One

In local proof propositions

PD0011 Mod4One PD0012 Mod4Three
Exact expanded first-order statement
forall p. ((~(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_first_prime_iff_left ftsc_second_prime_iff_left. (p) = ftsc_first_prime_iff_left * ftsc_first_prime_iff_left + ftsc_second_prime_iff_left * ftsc_second_prime_iff_left) -> (p = 2 \/ (exists ftsc_four_one_ftsc_prime. (p) = 4 * ftsc_four_one_ftsc_prime + 1))) /\ ((p = 2 \/ (exists ftsc_four_one_ftsc_prime. (p) = 4 * ftsc_four_one_ftsc_prime + 1)) -> (exists ftsc_first_prime_iff_right ftsc_second_prime_iff_right. (p) = ftsc_first_prime_iff_right * ftsc_first_prime_iff_right + ftsc_second_prime_iff_right * ftsc_second_prime_iff_right)))

Proof neighborhood

Direct theorem prerequisites

TS0021 prime_mod_four_trichotomy TS0004 sum_two_squares_not_four_mod_three prime_nonzero · Stable closed nonzero_is_succ · Stable closed TS001O prime_mod_four_one_is_sum_of_two_squares

Direct theorem dependents

none

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

49 script commands · 21 reading checkpoints · 3 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 (3)
prime mod four trichotomysum two squares not four mod threeprime mod four one is sum of two squares
01Fix variables and assumptionsL1–2

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

  1. L1
    intro p
  2. L2
    intro hprime
02Establish hcasesL3–6

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

  1. L3
    have hcases : p = 2 ∨ (Mod4One(p) ∨ Mod4Three(p))Definitions: Mod4One(p)Mod4Three(p)Original native command in the exact edition
  2. L4
    specialize prime_mod_four_trichotomy p
  3. L5
    apply prime_mod_four_trichotomy
  4. L6
    exact hprime
03Separate the logical casesL7–7

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

  1. L7
    split
04Fix variables and assumptionsL8–8

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

  1. L8
    intro hrepresentation
05Separate the logical casesL9–10

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

  1. L9
    cases hcases
  2. L10
    left
06Use earlier factsL11–11

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

  1. L11
    exact hcases_left
07Separate the logical casesL12–13

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

  1. L12
    cases hcases_right
  2. L13
    right
08Use earlier factsL14–14

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

  1. L14
    exact hcases_right_left
09Separate the logical casesL15–18

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

  1. L15
    exfalso
  2. L16
    cases hrepresentation
  3. L17
    cases hrepresentation_witness
  4. L18
    cases hcases_right_right
10Use earlier factsL19–21

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

  1. L19
    specialize sum_two_squares_not_four_mod_three x
  2. L20
    specialize sum_two_squares_not_four_mod_three x1
  3. L21
    apply sum_two_squares_not_four_mod_three
11Construct an explicit witnessL22–22

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

  1. L22
    exists x2
12Calculate and transport equalitiesL23–24

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

  1. L23
    trans p
  2. L24
    symm
13Use earlier factsL25–26

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

  1. L25
    exact hrepresentation_witness_witness
  2. L26
    exact hcases_right_right_witness
14Fix variables and assumptionsL27–27

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

  1. L27
    intro hallowed
15Separate the logical casesL28–28

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

  1. L28
    cases hallowed
16Construct an explicit witnessL29–30

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

  1. L29
    exists 1
  2. L30
    exists 1
17Calculate and transport equalitiesL31–32

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

  1. L31
    rewrite hallowed_left
  2. L32
    norm_num
18Establish hnonzeroL33–38

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

  1. L33
    have hnonzero : ~(p = 0)
  2. L34
    intro hzero
  3. L35
    specialize prime_nonzero p
  4. L36
    apply prime_nonzero
  5. L37
    exact hprime
  6. L38
    exact hzero
19Establish hsuccessorL39–42

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

  1. L39
    have hsuccessor : exists n. p = S n
  2. L40
    specialize nonzero_is_succ p
  3. L41
    apply nonzero_is_succ
  4. L42
    exact hnonzero
20Separate the logical casesL43–43

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

  1. L43
    cases hsuccessor
21Use earlier factsL44–49

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

  1. L44
    specialize prime_mod_four_one_is_sum_of_two_squares p
  2. L45
    specialize prime_mod_four_one_is_sum_of_two_squares x
  3. L46
    apply prime_mod_four_one_is_sum_of_two_squares
  4. L47
    exact hsuccessor_witness
  5. L48
    exact hprime
  6. L49
    exact hallowed_right

Library-wide reading audit

Original defined command ledger · 49 lines
  1. 0001intro p
  2. 0002intro hprime
  3. 0003have hcases : p = 2 ∨ (Mod4One(p) ∨ Mod4Three(p))
    Exact native replay linehave hcases : p = 2 \/ ((exists ftsc_four_one_ftsc_prime. (p) = 4 * ftsc_four_one_ftsc_prime + 1) \/ (exists ftsc_four_three_ftsc_prime. (p) = 4 * ftsc_four_three_ftsc_prime + 3))
  4. 0004specialize prime_mod_four_trichotomy p
  5. 0005apply prime_mod_four_trichotomy
  6. 0006exact hprime
  7. 0007split
  8. 0008intro hrepresentation
  9. 0009cases hcases
  10. 0010left
  11. 0011exact hcases_left
  12. 0012cases hcases_right
  13. 0013right
  14. 0014exact hcases_right_left
  15. 0015exfalso
  16. 0016cases hrepresentation
  17. 0017cases hrepresentation_witness
  18. 0018cases hcases_right_right
  19. 0019specialize sum_two_squares_not_four_mod_three x
  20. 0020specialize sum_two_squares_not_four_mod_three x1
  21. 0021apply sum_two_squares_not_four_mod_three
  22. 0022exists x2
  23. 0023trans p
  24. 0024symm
  25. 0025exact hrepresentation_witness_witness
  26. 0026exact hcases_right_right_witness
  27. 0027intro hallowed
  28. 0028cases hallowed
  29. 0029exists 1
  30. 0030exists 1
  31. 0031rewrite hallowed_left
  32. 0032norm_num
  33. 0033have hnonzero : ~(p = 0)
  34. 0034intro hzero
  35. 0035specialize prime_nonzero p
  36. 0036apply prime_nonzero
  37. 0037exact hprime
  38. 0038exact hzero
  39. 0039have hsuccessor : exists n. p = S n
  40. 0040specialize nonzero_is_succ p
  41. 0041apply nonzero_is_succ
  42. 0042exact hnonzero
  43. 0043cases hsuccessor
  44. 0044specialize prime_mod_four_one_is_sum_of_two_squares p
  45. 0045specialize prime_mod_four_one_is_sum_of_two_squares x
  46. 0046apply prime_mod_four_one_is_sum_of_two_squares
  47. 0047exact hsuccessor_witness
  48. 0048exact hprime
  49. 0049exact hallowed_right