TS002O · theorem body

prime_two_or_one_mod_four_is_sum_of_two_squares

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

The exceptional prime two and every prime congruent to one modulo four have explicit constructive two-square representations.

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) → 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

none
Exact expanded first-order statement
forall p. ((~(p = 1) /\ forall frm_prime_left_ftsf_admissible_prime frm_prime_right_ftsf_admissible_prime. p = frm_prime_left_ftsf_admissible_prime * frm_prime_right_ftsf_admissible_prime -> frm_prime_left_ftsf_admissible_prime = 1 \/ frm_prime_right_ftsf_admissible_prime = 1)) -> (p = 2 \/ exists t. p = 4 * t + 1) -> (exists ftsf_first_prime_result ftsf_second_prime_result. (p) = ftsf_first_prime_result * ftsf_first_prime_result + ftsf_second_prime_result * ftsf_second_prime_result)

Proof neighborhood

Direct theorem prerequisites

zero_or_succ · Stable closed prime_nonzero · Stable closed TS001O prime_mod_four_one_is_sum_of_two_squares

Direct theorem dependents

TS002Q beta_admissible_prime_factor_product_is_two_square TS002S beta_grouped_prime_square_factor_product_is_two_square TS003C all_bad_prime_even_two_square_sufficiency_bounded

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

22 script commands · 9 reading checkpoints · 0 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 (1)
prime mod four one is sum of two squares
01Fix variables and assumptionsL1–3

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

  1. L1
    intro p
  2. L2
    intro hprime
  3. L3
    intro hclass
02Separate the logical casesL4–4

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

  1. L4
    cases hclass
03Construct an explicit witnessL5–6

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

  1. L5
    exists 1
  2. L6
    exists 1
04Calculate and transport equalitiesL7–8

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

  1. L7
    rewrite hclass_left
  2. L8
    norm_num
05Use earlier factsL9–9

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

  1. L9
    specialize zero_or_succ p
06Separate the logical casesL10–11

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

  1. L10
    cases zero_or_succ
  2. L11
    exfalso
07Use earlier factsL12–15

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

  1. L12
    specialize prime_nonzero p
  2. L13
    apply prime_nonzero
  3. L14
    exact hprime
  4. L15
    exact zero_or_succ_left
08Separate the logical casesL16–16

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

  1. L16
    cases zero_or_succ_right
09Use earlier factsL17–22

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

  1. L17
    specialize prime_mod_four_one_is_sum_of_two_squares p
  2. L18
    specialize prime_mod_four_one_is_sum_of_two_squares x
  3. L19
    apply prime_mod_four_one_is_sum_of_two_squares
  4. L20
    exact zero_or_succ_right_witness
  5. L21
    exact hprime
  6. L22
    exact hclass_right

Library-wide reading audit

Original defined command ledger · 22 lines
  1. 0001intro p
  2. 0002intro hprime
  3. 0003intro hclass
  4. 0004cases hclass
  5. 0005exists 1
  6. 0006exists 1
  7. 0007rewrite hclass_left
  8. 0008norm_num
  9. 0009specialize zero_or_succ p
  10. 0010cases zero_or_succ
  11. 0011exfalso
  12. 0012specialize prime_nonzero p
  13. 0013apply prime_nonzero
  14. 0014exact hprime
  15. 0015exact zero_or_succ_left
  16. 0016cases zero_or_succ_right
  17. 0017specialize prime_mod_four_one_is_sum_of_two_squares p
  18. 0018specialize prime_mod_four_one_is_sum_of_two_squares x
  19. 0019apply prime_mod_four_one_is_sum_of_two_squares
  20. 0020exact zero_or_succ_right_witness
  21. 0021exact hprime
  22. 0022exact hclass_right