TS001O · theorem body

prime_mod_four_one_is_sum_of_two_squares

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

Every prime congruent to one modulo four has an explicitly witnessed constructive representation as the sum of two natural 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.

Statement with defined notation

∀ p. ∀ n. p = S n → Prime(p) → 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

PD0002 Lt PD0013 BetaAt PD0051 FloorSqrt
Exact expanded first-order statement
forall p n. p = S n -> ((~(p = 1) /\ forall frm_prime_left_ftpr_prime frm_prime_right_ftpr_prime. p = frm_prime_left_ftpr_prime * frm_prime_right_ftpr_prime -> frm_prime_left_ftpr_prime = 1 \/ frm_prime_right_ftpr_prime = 1)) -> (exists t. p = 4 * t + 1) -> exists x y. p = x * x + y * y

Proof neighborhood

Direct theorem prerequisites

TS0009 prime_mod_four_one_bounded_divisible_two_square_norm_exists floor_sqrt_total · Alpha closed TS000Z prime_floor_affine_residue_grid_collision TS001N prime_floor_affine_grid_collision_represents_prime

Direct theorem dependents

TS0028 prime_is_two_squares_iff_two_or_one_mod_four TS002O prime_two_or_one_mod_four_is_sum_of_two_squares

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

45 script commands · 12 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.

Named ingredients (3)
prime mod four one bounded divisible two square norm existsprime floor affine residue grid collisionprime floor affine grid collision represents prime
01Fix variables and assumptionsL1–5

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

  1. L1
    intro p
  2. L2
    intro n
  3. L3
    intro hpredecessor
  4. L4
    intro hprime
  5. L5
    intro hmodfour
02Establish hrootL6–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime mod four one bounded divisible two square norm exists.

  1. L6
    have hroot : ∃ r. ∃ k. Lt(r,p) ∧ r · r + 1 = p · kDefinitions: Lt(r,p)Original native command in the exact edition
  2. L7
    specialize prime_mod_four_one_bounded_divisible_two_square_norm_exists p
  3. L8
    specialize prime_mod_four_one_bounded_divisible_two_square_norm_exists n
  4. L9
    apply prime_mod_four_one_bounded_divisible_two_square_norm_exists
  5. L10
    exact hpredecessor
  6. L11
    exact hprime
  7. L12
    exact hmodfour
03Separate the logical casesL13–15

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

  1. L13
    cases hroot
  2. L14
    cases hroot_witness
  3. L15
    cases hroot_witness_witness
04Establish hfloorL16–18

Establish this local claim before using it. It is not an additional assumption.

  1. L16
    have hfloor : ∃ s. FloorSqrt(p,s)Definitions: FloorSqrt(p,s)Original native command in the exact edition
  2. L17
    specialize floor_sqrt_total p
  3. L18
    exact floor_sqrt_total
05Separate the logical casesL19–19

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

  1. L19
    cases hfloor
06Establish hgridL20–28

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply prime floor affine residue grid collision.

  1. L20
    have hgrid : ∃ b. ∃ c. (∀ y. Lt(y,S x2 · S x2) → ∃ z. ∃ n. ∃ m. ∃ k. y = S x2 · z + n ∧ (Lt(n,S x2) ∧ (x · z + n = p · m + k ∧ (Lt(k,p) ∧ BetaAt(b,c,y,k))))) ∧ (∃ y. ∃ z. ∃ n. Lt(y,S x2 · S x2) ∧ (Lt(z,S x2 · S x2) ∧ (¬y = z ∧ (BetaAt(b,c,y,n) ∧ BetaAt(b,c,z,n)))))Definitions: Lt(y,S x2 · S x2)Lt(n,S x2)Lt(k,p)BetaAt(b,c,y,k)Lt(z,S x2 · S x2)BetaAt(b,c,y,n)BetaAt(b,c,z,n)Original native command in the exact edition
  2. L21
    specialize prime_floor_affine_residue_grid_collision p
  3. L22
    specialize prime_floor_affine_residue_grid_collision x2
  4. L23
    specialize prime_floor_affine_residue_grid_collision x
  5. L24
    specialize prime_floor_affine_residue_grid_collision (S x2 * S x2)
  6. L25
    apply prime_floor_affine_residue_grid_collision
  7. L26
    refl
  8. L27
    exact hprime
  9. L28
    exact hfloor_witness
07Separate the logical casesL29–31

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

  1. L29
    cases hgrid
  2. L30
    cases hgrid_witness
  3. L31
    cases hgrid_witness_witness
08Use earlier factsL32–38

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

  1. L32
    specialize prime_floor_affine_grid_collision_represents_prime p
  2. L33
    specialize prime_floor_affine_grid_collision_represents_prime x2
  3. L34
    specialize prime_floor_affine_grid_collision_represents_prime x
  4. L35
    specialize prime_floor_affine_grid_collision_represents_prime x3
  5. L36
    specialize prime_floor_affine_grid_collision_represents_prime x4
  6. L37
    specialize prime_floor_affine_grid_collision_represents_prime (S x2 * S x2)
  7. L38
    apply prime_floor_affine_grid_collision_represents_prime
09Calculate and transport equalitiesL39–39

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

  1. L39
    refl
10Use earlier factsL40–41

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

  1. L40
    exact hprime
  2. L41
    exact hfloor_witness
11Construct an explicit witnessL42–42

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

  1. L42
    exists x1
12Use earlier factsL43–45

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

  1. L43
    exact hroot_witness_witness_right
  2. L44
    exact hgrid_witness_witness_left
  3. L45
    exact hgrid_witness_witness_right

Library-wide reading audit

Original defined command ledger · 45 lines
  1. 0001intro p
  2. 0002intro n
  3. 0003intro hpredecessor
  4. 0004intro hprime
  5. 0005intro hmodfour
  6. 0006have hroot : ∃ r. ∃ k. Lt(r,p) ∧ r · r + 1 = p · k
    Exact native replay linehave hroot : exists r k. ((exists ftcn_strict_final_root. ftcn_strict_final_root + S (r) = (p)) /\ r * r + 1 = p * k)
  7. 0007specialize prime_mod_four_one_bounded_divisible_two_square_norm_exists p
  8. 0008specialize prime_mod_four_one_bounded_divisible_two_square_norm_exists n
  9. 0009apply prime_mod_four_one_bounded_divisible_two_square_norm_exists
  10. 0010exact hpredecessor
  11. 0011exact hprime
  12. 0012exact hmodfour
  13. 0013cases hroot
  14. 0014cases hroot_witness
  15. 0015cases hroot_witness_witness
  16. 0016have hfloor : ∃ s. FloorSqrt(p,s)
    Exact native replay linehave hfloor : exists s. (((exists bcs_sqrt_lower_gap_ftpr_final_floor. bcs_sqrt_lower_gap_ftpr_final_floor + (s) * (s) = (p)) /\ exists bcs_sqrt_upper_gap_ftpr_final_floor. bcs_sqrt_upper_gap_ftpr_final_floor + S (p) = S (s) * S (s)))
  17. 0017specialize floor_sqrt_total p
  18. 0018exact floor_sqrt_total
  19. 0019cases hfloor
  20. 0020have hgrid : ∃ b. ∃ c. (∀ y. Lt(y,S x2 · S x2) → ∃ z. ∃ n. ∃ m. ∃ k. y = S x2 · z + n ∧ (Lt(n,S x2) ∧ (x · z + n = p · m + k ∧ (Lt(k,p) ∧ BetaAt(b,c,y,k))))) ∧ (∃ y. ∃ z. ∃ n. Lt(y,S x2 · S x2) ∧ (Lt(z,S x2 · S x2) ∧ (¬y = z ∧ (BetaAt(b,c,y,n) ∧ BetaAt(b,c,z,n)))))
    Exact native replay linehave hgrid : exists b c. ((forall ftrg_index_ftpr_final_grid. (exists ftrg_gap_ftpr_final_grid_index. ftrg_gap_ftpr_final_grid_index + S (ftrg_index_ftpr_final_grid) = (S x2 * S x2)) -> exists ftrg_row_ftpr_final_grid ftrg_column_ftpr_final_grid ftrg_quotient_ftpr_final_grid ftrg_remainder_ftpr_final_grid. ((ftrg_index_ftpr_final_grid) = (S x2) * ftrg_row_ftpr_final_grid + ftrg_column_ftpr_final_grid /\ ((exists ftrg_gap_ftpr_final_grid_column. ftrg_gap_ftpr_final_grid_column + S (ftrg_column_ftpr_final_grid) = (S x2)) /\ ((x * ftrg_row_ftpr_final_grid + ftrg_column_ftpr_final_grid = (p) * ftrg_quotient_ftpr_final_grid + ftrg_remainder_ftpr_final_grid) /\ ((exists ftrg_gap_ftpr_final_grid_residue. ftrg_gap_ftpr_final_grid_residue + S (ftrg_remainder_ftpr_final_grid) = (p)) /\ (((exists ff_h_ftrg_ftpr_final_grid_entry. ff_h_ftrg_ftpr_final_grid_entry + S (ftrg_remainder_ftpr_final_grid) = S ((S (ftrg_index_ftpr_final_grid)) * c)) /\ exists ff_q_ftrg_ftpr_final_grid_entry. b = ff_q_ftrg_ftpr_final_grid_entry * S ((S (ftrg_index_ftpr_final_grid)) * c) + (ftrg_remainder_ftpr_final_grid)))))))) /\ (exists ftsp_first_ftpr_final_collision ftsp_second_ftpr_final_collision ftsp_value_ftpr_final_collision. ((exists ftsp_gap_ftpr_final_collision_first. ftsp_gap_ftpr_final_collision_first + S (ftsp_first_ftpr_final_collision) = S x2 * S x2) /\ ((exists ftsp_gap_ftpr_final_collision_second. ftsp_gap_ftpr_final_collision_second + S (ftsp_second_ftpr_final_collision) = S x2 * S x2) /\ (~(ftsp_first_ftpr_final_collision = ftsp_second_ftpr_final_collision) /\ ((((exists ff_h_ftsp_ftpr_final_collision_left. ff_h_ftsp_ftpr_final_collision_left + S (ftsp_value_ftpr_final_collision) = S ((S (ftsp_first_ftpr_final_collision)) * c)) /\ exists ff_q_ftsp_ftpr_final_collision_left. b = ff_q_ftsp_ftpr_final_collision_left * S ((S (ftsp_first_ftpr_final_collision)) * c) + (ftsp_value_ftpr_final_collision))) /\ (((exists ff_h_ftsp_ftpr_final_collision_right. ff_h_ftsp_ftpr_final_collision_right + S (ftsp_value_ftpr_final_collision) = S ((S (ftsp_second_ftpr_final_collision)) * c)) /\ exists ff_q_ftsp_ftpr_final_collision_right. b = ff_q_ftsp_ftpr_final_collision_right * S ((S (ftsp_second_ftpr_final_collision)) * c) + (ftsp_value_ftpr_final_collision)))))))))
  21. 0021specialize prime_floor_affine_residue_grid_collision p
  22. 0022specialize prime_floor_affine_residue_grid_collision x2
  23. 0023specialize prime_floor_affine_residue_grid_collision x
  24. 0024specialize prime_floor_affine_residue_grid_collision (S x2 * S x2)
  25. 0025apply prime_floor_affine_residue_grid_collision
  26. 0026refl
  27. 0027exact hprime
  28. 0028exact hfloor_witness
  29. 0029cases hgrid
  30. 0030cases hgrid_witness
  31. 0031cases hgrid_witness_witness
  32. 0032specialize prime_floor_affine_grid_collision_represents_prime p
  33. 0033specialize prime_floor_affine_grid_collision_represents_prime x2
  34. 0034specialize prime_floor_affine_grid_collision_represents_prime x
  35. 0035specialize prime_floor_affine_grid_collision_represents_prime x3
  36. 0036specialize prime_floor_affine_grid_collision_represents_prime x4
  37. 0037specialize prime_floor_affine_grid_collision_represents_prime (S x2 * S x2)
  38. 0038apply prime_floor_affine_grid_collision_represents_prime
  39. 0039refl
  40. 0040exact hprime
  41. 0041exact hfloor_witness
  42. 0042exists x1
  43. 0043exact hroot_witness_witness_right
  44. 0044exact hgrid_witness_witness_left
  45. 0045exact hgrid_witness_witness_right