TS0004

sum_two_squares_not_four_mod_three

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

No natural congruent to three modulo four is a sum of two squares.

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 a b. ~(exists fts_four_sum_three. a * a + b * b = 4 * fts_four_sum_three + 3)

Constructive proof overview

Generated structural guide

No natural congruent to three modulo four is a sum of two squares.

The unchanged tactic script uses 2 declared prerequisites and contains 74 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

TS0003 sum_two_squares_mod_four_cases division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

TS0028 prime_is_two_squares_iff_two_or_one_mod_four TS0037 three_mod_four_number_not_equal_represented

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

74 script commands · 33 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 (1)
sum two squares mod four cases
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro hthree
02Separate the logical casesL4–4

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

  1. L4
    cases hthree
03Use earlier factsL5–6

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

  1. L5
    specialize sum_two_squares_mod_four_cases a
  2. L6
    specialize sum_two_squares_mod_four_cases b
04Separate the logical casesL7–9

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

  1. L7
    cases sum_two_squares_mod_four_cases
  2. L8
    cases sum_two_squares_mod_four_cases_left
  3. L9
    cases sum_two_squares_mod_four_cases_left_left
05Establish huniquenessL10–18

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

  1. L10
    have huniqueness : x1 = x /\ 0 = 3
  2. L11
    specialize division_remainder_unique 4
  3. L12
    specialize division_remainder_unique (a * a + b * b)
  4. L13
    specialize division_remainder_unique x1
  5. L14
    specialize division_remainder_unique 0
  6. L15
    specialize division_remainder_unique x
  7. L16
    specialize division_remainder_unique 3
  8. L17
    apply division_remainder_unique
  9. L18
    exact sum_two_squares_mod_four_cases_left_left_witness
06Construct an explicit witnessL19–19

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

  1. L19
    exists 3
07Calculate and transport equalitiesL20–20

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

  1. L20
    norm_num
08Use earlier factsL21–21

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

  1. L21
    exact hthree_witness
09Construct an explicit witnessL22–22

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

  1. L22
    exists 0
10Calculate and transport equalitiesL23–23

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

  1. L23
    norm_num
11Separate the logical casesL24–24

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

  1. L24
    cases huniqueness
12Use earlier factsL25–25

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

  1. L25
    apply PA1
13Calculate and transport equalitiesL26–26

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

  1. L26
    symm
14Use earlier factsL27–27

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

  1. L27
    exact huniqueness_right
15Separate the logical casesL28–28

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

  1. L28
    cases sum_two_squares_mod_four_cases_left_right
16Establish huniquenessL29–37

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

  1. L29
    have huniqueness : x1 = x /\ 1 = 3
  2. L30
    specialize division_remainder_unique 4
  3. L31
    specialize division_remainder_unique (a * a + b * b)
  4. L32
    specialize division_remainder_unique x1
  5. L33
    specialize division_remainder_unique 1
  6. L34
    specialize division_remainder_unique x
  7. L35
    specialize division_remainder_unique 3
  8. L36
    apply division_remainder_unique
  9. L37
    exact sum_two_squares_mod_four_cases_left_right_witness
17Construct an explicit witnessL38–38

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

  1. L38
    exists 2
18Calculate and transport equalitiesL39–39

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

  1. L39
    norm_num
19Use earlier factsL40–40

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

  1. L40
    exact hthree_witness
20Construct an explicit witnessL41–41

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

  1. L41
    exists 0
21Calculate and transport equalitiesL42–42

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

  1. L42
    norm_num
22Separate the logical casesL43–43

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

  1. L43
    cases huniqueness
23Establish hzeroL44–49

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

  1. L44
    have hzero : 0 = 2
  2. L45
    apply PA2
  3. L46
    exact huniqueness_right
  4. L47
    apply PA1
  5. L48
    symm
  6. L49
    exact hzero
24Separate the logical casesL50–50

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

  1. L50
    cases sum_two_squares_mod_four_cases_right
25Establish huniquenessL51–59

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

  1. L51
    have huniqueness : x1 = x /\ 2 = 3
  2. L52
    specialize division_remainder_unique 4
  3. L53
    specialize division_remainder_unique (a * a + b * b)
  4. L54
    specialize division_remainder_unique x1
  5. L55
    specialize division_remainder_unique 2
  6. L56
    specialize division_remainder_unique x
  7. L57
    specialize division_remainder_unique 3
  8. L58
    apply division_remainder_unique
  9. L59
    exact sum_two_squares_mod_four_cases_right_witness
26Construct an explicit witnessL60–60

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

  1. L60
    exists 1
27Calculate and transport equalitiesL61–61

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

  1. L61
    norm_num
28Use earlier factsL62–62

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

  1. L62
    exact hthree_witness
29Construct an explicit witnessL63–63

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

  1. L63
    exists 0
30Calculate and transport equalitiesL64–64

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

  1. L64
    norm_num
31Separate the logical casesL65–65

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

  1. L65
    cases huniqueness
32Establish honeL66–68

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

  1. L66
    have hone : 1 = 2
  2. L67
    apply PA2
  3. L68
    exact huniqueness_right
33Establish hzeroL69–74

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

  1. L69
    have hzero : 0 = 1
  2. L70
    apply PA2
  3. L71
    exact hone
  4. L72
    apply PA1
  5. L73
    symm
  6. L74
    exact hzero

Library-wide reading audit

Original exact command ledger · 74 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro hthree
  4. 0004cases hthree
  5. 0005specialize sum_two_squares_mod_four_cases a
  6. 0006specialize sum_two_squares_mod_four_cases b
  7. 0007cases sum_two_squares_mod_four_cases
  8. 0008cases sum_two_squares_mod_four_cases_left
  9. 0009cases sum_two_squares_mod_four_cases_left_left
  10. 0010have huniqueness : x1 = x /\ 0 = 3
  11. 0011specialize division_remainder_unique 4
  12. 0012specialize division_remainder_unique (a * a + b * b)
  13. 0013specialize division_remainder_unique x1
  14. 0014specialize division_remainder_unique 0
  15. 0015specialize division_remainder_unique x
  16. 0016specialize division_remainder_unique 3
  17. 0017apply division_remainder_unique
  18. 0018exact sum_two_squares_mod_four_cases_left_left_witness
  19. 0019exists 3
  20. 0020norm_num
  21. 0021exact hthree_witness
  22. 0022exists 0
  23. 0023norm_num
  24. 0024cases huniqueness
  25. 0025apply PA1
  26. 0026symm
  27. 0027exact huniqueness_right
  28. 0028cases sum_two_squares_mod_four_cases_left_right
  29. 0029have huniqueness : x1 = x /\ 1 = 3
  30. 0030specialize division_remainder_unique 4
  31. 0031specialize division_remainder_unique (a * a + b * b)
  32. 0032specialize division_remainder_unique x1
  33. 0033specialize division_remainder_unique 1
  34. 0034specialize division_remainder_unique x
  35. 0035specialize division_remainder_unique 3
  36. 0036apply division_remainder_unique
  37. 0037exact sum_two_squares_mod_four_cases_left_right_witness
  38. 0038exists 2
  39. 0039norm_num
  40. 0040exact hthree_witness
  41. 0041exists 0
  42. 0042norm_num
  43. 0043cases huniqueness
  44. 0044have hzero : 0 = 2
  45. 0045apply PA2
  46. 0046exact huniqueness_right
  47. 0047apply PA1
  48. 0048symm
  49. 0049exact hzero
  50. 0050cases sum_two_squares_mod_four_cases_right
  51. 0051have huniqueness : x1 = x /\ 2 = 3
  52. 0052specialize division_remainder_unique 4
  53. 0053specialize division_remainder_unique (a * a + b * b)
  54. 0054specialize division_remainder_unique x1
  55. 0055specialize division_remainder_unique 2
  56. 0056specialize division_remainder_unique x
  57. 0057specialize division_remainder_unique 3
  58. 0058apply division_remainder_unique
  59. 0059exact sum_two_squares_mod_four_cases_right_witness
  60. 0060exists 1
  61. 0061norm_num
  62. 0062exact hthree_witness
  63. 0063exists 0
  64. 0064norm_num
  65. 0065cases huniqueness
  66. 0066have hone : 1 = 2
  67. 0067apply PA2
  68. 0068exact huniqueness_right
  69. 0069have hzero : 0 = 1
  70. 0070apply PA2
  71. 0071exact hone
  72. 0072apply PA1
  73. 0073symm
  74. 0074exact hzero