PF0011 · theorem body

pythagorean_two_mod_four_not_square

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

No natural square is congruent to two modulo four, by uniqueness of bounded constructive remainders.

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

forall z q. z * z = 4 * q + 2 -> false

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

none

In local proof propositions

none
Exact expanded first-order statement
forall z q. z * z = 4 * q + 2 -> false

Proof neighborhood

Direct theorem prerequisites

square_mod_four_zero_or_one · Alpha closed division_remainder_unique · Stable closed

Direct theorem dependents

PF0012 pythagorean_triple_legs_not_both_odd

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

44 script commands · 20 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.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro z
  2. L2
    intro q
  3. L3
    intro htwo
02Use earlier factsL4–4

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

  1. L4
    specialize square_mod_four_zero_or_one z
03Separate the logical casesL5–6

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

  1. L5
    cases square_mod_four_zero_or_one
  2. L6
    cases square_mod_four_zero_or_one_left
04Establish huniqueL7–15

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

  1. L7
    have hunique : q = x /\ 2 = 0
  2. L8
    specialize division_remainder_unique 4
  3. L9
    specialize division_remainder_unique (z * z)
  4. L10
    specialize division_remainder_unique q
  5. L11
    specialize division_remainder_unique 2
  6. L12
    specialize division_remainder_unique x
  7. L13
    specialize division_remainder_unique 0
  8. L14
    apply division_remainder_unique
  9. L15
    exact htwo
05Construct an explicit witnessL16–16

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

  1. L16
    exists 1
06Calculate and transport equalitiesL17–17

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

  1. L17
    norm_num
07Use earlier factsL18–18

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

  1. L18
    exact square_mod_four_zero_or_one_left_witness
08Construct an explicit witnessL19–19

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

  1. L19
    exists 3
09Calculate 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
10Separate the logical casesL21–21

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

  1. L21
    cases hunique
11Use earlier factsL22–23

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

  1. L22
    apply PA1
  2. L23
    exact hunique_right
12Separate the logical casesL24–24

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

  1. L24
    cases square_mod_four_zero_or_one_right
13Establish huniqueL25–33

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

  1. L25
    have hunique : q = x /\ 2 = 1
  2. L26
    specialize division_remainder_unique 4
  3. L27
    specialize division_remainder_unique (z * z)
  4. L28
    specialize division_remainder_unique q
  5. L29
    specialize division_remainder_unique 2
  6. L30
    specialize division_remainder_unique x
  7. L31
    specialize division_remainder_unique 1
  8. L32
    apply division_remainder_unique
  9. L33
    exact htwo
14Construct an explicit witnessL34–34

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

  1. L34
    exists 1
15Calculate and transport equalitiesL35–35

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

  1. L35
    norm_num
16Use earlier factsL36–36

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

  1. L36
    exact square_mod_four_zero_or_one_right_witness
17Construct an explicit witnessL37–37

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

  1. L37
    exists 2
18Calculate and transport equalitiesL38–38

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

  1. L38
    norm_num
19Separate the logical casesL39–39

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

  1. L39
    cases hunique
20Establish hzeroL40–44

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

  1. L40
    have hzero : 1 = 0
  2. L41
    apply PA2
  3. L42
    exact hunique_right
  4. L43
    apply PA1
  5. L44
    exact hzero

Library-wide reading audit

Original defined command ledger · 44 lines
  1. 0001intro z
  2. 0002intro q
  3. 0003intro htwo
  4. 0004specialize square_mod_four_zero_or_one z
  5. 0005cases square_mod_four_zero_or_one
  6. 0006cases square_mod_four_zero_or_one_left
  7. 0007have hunique : q = x /\ 2 = 0
  8. 0008specialize division_remainder_unique 4
  9. 0009specialize division_remainder_unique (z * z)
  10. 0010specialize division_remainder_unique q
  11. 0011specialize division_remainder_unique 2
  12. 0012specialize division_remainder_unique x
  13. 0013specialize division_remainder_unique 0
  14. 0014apply division_remainder_unique
  15. 0015exact htwo
  16. 0016exists 1
  17. 0017norm_num
  18. 0018exact square_mod_four_zero_or_one_left_witness
  19. 0019exists 3
  20. 0020norm_num
  21. 0021cases hunique
  22. 0022apply PA1
  23. 0023exact hunique_right
  24. 0024cases square_mod_four_zero_or_one_right
  25. 0025have hunique : q = x /\ 2 = 1
  26. 0026specialize division_remainder_unique 4
  27. 0027specialize division_remainder_unique (z * z)
  28. 0028specialize division_remainder_unique q
  29. 0029specialize division_remainder_unique 2
  30. 0030specialize division_remainder_unique x
  31. 0031specialize division_remainder_unique 1
  32. 0032apply division_remainder_unique
  33. 0033exact htwo
  34. 0034exists 1
  35. 0035norm_num
  36. 0036exact square_mod_four_zero_or_one_right_witness
  37. 0037exists 2
  38. 0038norm_num
  39. 0039cases hunique
  40. 0040have hzero : 1 = 0
  41. 0041apply PA2
  42. 0042exact hunique_right
  43. 0043apply PA1
  44. 0044exact hzero