TS002O

prime_two_or_one_mod_four_is_sum_of_two_squares

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

Exact expanded first-order arithmetic 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)

Constructive proof overview

Generated structural guide

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

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

zero_or_succ Stable theorem; checked-use authorized prime_nonzero Stable theorem; checked-use authorized TS001O prime_mod_four_one_is_sum_of_two_squares

Direct 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

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

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.

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