PF0011

pythagorean_two_mod_four_not_square

Alpha v34 independently verified · alpha_closed; checked-use authorized; 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.

Exact expanded first-order arithmetic statement

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

Constructive proof overview

Generated structural guide

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

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

square_mod_four_zero_or_one Alpha theorem; checked-use authorized division_remainder_unique Stable theorem; checked-use authorized

Direct dependents

PF0012 pythagorean_triple_legs_not_both_odd

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

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.

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 exact 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