TF0006

positive_number_with_admissible_prime_divisors_is_two_square

A positive natural number all of whose prime divisors are two or one modulo four has an explicitly constructed two-square representation via its canonical prime factorization.

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

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.

The exact G025 progression-prime milestone is fully proved in unchanged constructive arithmetic; Mod4Three deliberately reuses its existing Quadratic Reciprocity definition PD0012. The much stronger full Dirichlet progression-prime milestone G030 remains open.

Exact theorem in conservative defined notation

∀ n. ¬n = 0 → (∀ x. Prime(x) → Dvd(x,n) → x = 2 ∨ (∃ y. x = 4 · y + 1)) → ∃ x. ∃ y. n = x · x + y · y

Every linked abbreviation expands hygienically to the identical original native formula.

Definition DAG

Dvd(d,n) · 1Prime(p) · 1

Actual proof prerequisites

prime_factorization_existence · checked external prerequisitebeta_all_prime_entry_is_primebeta_factor_divides_product · checked external prerequisitebeta_admissible_prime_factor_product_is_two_square
Original expanded first-order statement 
forall n. ~(n = 0) -> (forall ftsf_divisor_canonical_source. ((~(ftsf_divisor_canonical_source = 1) /\ forall frm_prime_left_ftsf_canonical_source_prime frm_prime_right_ftsf_canonical_source_prime. ftsf_divisor_canonical_source = frm_prime_left_ftsf_canonical_source_prime * frm_prime_right_ftsf_canonical_source_prime -> frm_prime_left_ftsf_canonical_source_prime = 1 \/ frm_prime_right_ftsf_canonical_source_prime = 1)) -> (exists ftsf_quotient_canonical_source. (n) = ftsf_divisor_canonical_source * ftsf_quotient_canonical_source) -> (ftsf_divisor_canonical_source = 2 \/ exists ftsf_residue_canonical_source. ftsf_divisor_canonical_source = 4 * ftsf_residue_canonical_source + 1)) -> (exists ftsf_first_canonical_result ftsf_second_canonical_result. (n) = ftsf_first_canonical_result * ftsf_first_canonical_result + ftsf_second_canonical_result * ftsf_second_canonical_result)

Complete unchanged native tactic proof

All 47 lines are the exact independently kernel-checked original script.

Read the argument

Proof checkpoints

47 script commands · 10 reading checkpoints · 2 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 (2)
beta admissible prime factor product is two squarebeta all prime entry is prime

Long local formulas use this family’s existing definitions. Each new abbreviation was expanded back to the identical native formula, including its free-variable context. The original edition is preserved below.

01Fix variables and assumptionsL1–3

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

  1. L1
    intro n
  2. L2
    intro hnonzero
  3. L3
    intro hdivisors
02Use earlier factsL4–4

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

  1. L4
    specialize prime_factorization_existence n
03Establish hfactorizationL5–7

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

  1. L5
    have hfactorization : ∃ l. ∃ b. ∃ c. Product(b,c,l,n) ∧ (AllPrime(b,c,l) ∧ (∀ x. Lt(S x,l) → ∃ y. ∃ z. BetaAt(b,c,x,y) ∧ (BetaAt(b,c,S x,z) ∧ Le(y,z))))Definitions: LeLtBetaAtProductAllPrimeOriginal native command in the exact edition
  2. L6
    apply prime_factorization_existence
  3. L7
    exact hnonzero
04Separate the logical casesL8–12

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

  1. L8
    cases hfactorization
  2. L9
    cases hfactorization_witness
  3. L10
    cases hfactorization_witness_witness
  4. L11
    cases hfactorization_witness_witness_witness
  5. L12
    cases hfactorization_witness_witness_witness_right
05Use earlier factsL13–18

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

  1. L13
    specialize beta_admissible_prime_factor_product_is_two_square x1
  2. L14
    specialize beta_admissible_prime_factor_product_is_two_square x2
  3. L15
    specialize beta_admissible_prime_factor_product_is_two_square x
  4. L16
    specialize beta_admissible_prime_factor_product_is_two_square n
  5. L17
    apply beta_admissible_prime_factor_product_is_two_square
  6. L18
    exact hfactorization_witness_witness_witness_left
06Fix variables and assumptionsL19–22

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

  1. L19
    intro i
  2. L20
    intro p
  3. L21
    intro hi
  4. L22
    intro hp
07Establish hprimeL23–32

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta all prime entry is prime.

  1. L23
    have hprime : (~(p = 1) /\ forall frm_prime_left_ftsf_canonical_local_prime frm_prime_right_ftsf_canonical_local_prime. p = frm_prime_left_ftsf_canonical_local_prime * frm_prime_right_ftsf_canonical_local_prime -> frm_prime_left_ftsf_canonical_local_prime = 1 \/ frm_prime_right_ftsf_canonical_local_prime = 1)
  2. L24
    specialize beta_all_prime_entry_is_prime x1
  3. L25
    specialize beta_all_prime_entry_is_prime x2
  4. L26
    specialize beta_all_prime_entry_is_prime x
  5. L27
    specialize beta_all_prime_entry_is_prime i
  6. L28
    specialize beta_all_prime_entry_is_prime p
  7. L29
    apply beta_all_prime_entry_is_prime
  8. L30
    exact hfactorization_witness_witness_witness_right_left
  9. L31
    exact hi
  10. L32
    exact hp
08Separate the logical casesL33–33

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

  1. L33
    split
09Use earlier factsL34–43

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

  1. L34
    exact hprime
  2. L35
    specialize hdivisors p
  3. L36
    apply hdivisors
  4. L37
    exact hprime
  5. L38
    specialize beta_factor_divides_product x1
  6. L39
    specialize beta_factor_divides_product x2
  7. L40
    specialize beta_factor_divides_product x
  8. L41
    specialize beta_factor_divides_product n
  9. L42
    specialize beta_factor_divides_product i
  10. L43
    specialize beta_factor_divides_product p
10Use earlier factsL44–47

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

  1. L44
    apply beta_factor_divides_product
  2. L45
    exact hi
  3. L46
    exact hp
  4. L47
    exact hfactorization_witness_witness_witness_left

Library-wide reading audit

Original defined command ledger · 47 lines
  1. 0001intro n
  2. 0002intro hnonzero
  3. 0003intro hdivisors
  4. 0004specialize prime_factorization_existence n
  5. 0005have hfactorization : exists l b c. ((exists ff_u_ftsf_canonical_product ff_v_ftsf_canonical_product. ((((exists ff_h_ftsf_canonical_product_start. ff_h_ftsf_canonical_product_start + S (1) = S ((S (0)) * ff_v_ftsf_canonical_product)) /\ exists ff_q_ftsf_canonical_product_start. ff_u_ftsf_canonical_product = ff_q_ftsf_canonical_product_start * S ((S (0)) * ff_v_ftsf_canonical_product) + (1))) /\ ((((exists ff_h_ftsf_canonical_product_terminal. ff_h_ftsf_canonical_product_terminal + S (n) = S ((S (l)) * ff_v_ftsf_canonical_product)) /\ exists ff_q_ftsf_canonical_product_terminal. ff_u_ftsf_canonical_product = ff_q_ftsf_canonical_product_terminal * S ((S (l)) * ff_v_ftsf_canonical_product) + (n))) /\ forall ff_i_ftsf_canonical_product. (exists ff_lt_ftsf_canonical_product_bound. ff_lt_ftsf_canonical_product_bound + S ff_i_ftsf_canonical_product = l) -> exists ff_p_ftsf_canonical_product ff_r_ftsf_canonical_product ff_s_ftsf_canonical_product. ((((exists ff_h_ftsf_canonical_product_factor. ff_h_ftsf_canonical_product_factor + S (ff_p_ftsf_canonical_product) = S ((S (ff_i_ftsf_canonical_product)) * c)) /\ exists ff_q_ftsf_canonical_product_factor. b = ff_q_ftsf_canonical_product_factor * S ((S (ff_i_ftsf_canonical_product)) * c) + (ff_p_ftsf_canonical_product))) /\ ((((exists ff_h_ftsf_canonical_product_partial. ff_h_ftsf_canonical_product_partial + S (ff_r_ftsf_canonical_product) = S ((S (ff_i_ftsf_canonical_product)) * ff_v_ftsf_canonical_product)) /\ exists ff_q_ftsf_canonical_product_partial. ff_u_ftsf_canonical_product = ff_q_ftsf_canonical_product_partial * S ((S (ff_i_ftsf_canonical_product)) * ff_v_ftsf_canonical_product) + (ff_r_ftsf_canonical_product))) /\ ((((exists ff_h_ftsf_canonical_product_successor. ff_h_ftsf_canonical_product_successor + S (ff_s_ftsf_canonical_product) = S ((S (S ff_i_ftsf_canonical_product)) * ff_v_ftsf_canonical_product)) /\ exists ff_q_ftsf_canonical_product_successor. ff_u_ftsf_canonical_product = ff_q_ftsf_canonical_product_successor * S ((S (S ff_i_ftsf_canonical_product)) * ff_v_ftsf_canonical_product) + (ff_s_ftsf_canonical_product))) /\ ff_s_ftsf_canonical_product = ff_r_ftsf_canonical_product * ff_p_ftsf_canonical_product)))))) /\ ((forall ftsf_index_canonical_all_prime. (exists ftsf_gap_canonical_all_prime_bound. ftsf_gap_canonical_all_prime_bound + S ftsf_index_canonical_all_prime = (l)) -> exists ftsf_factor_canonical_all_prime. ((((exists ff_h_ftsf_canonical_all_prime_entry. ff_h_ftsf_canonical_all_prime_entry + S (ftsf_factor_canonical_all_prime) = S ((S (ftsf_index_canonical_all_prime)) * c)) /\ exists ff_q_ftsf_canonical_all_prime_entry. b = ff_q_ftsf_canonical_all_prime_entry * S ((S (ftsf_index_canonical_all_prime)) * c) + (ftsf_factor_canonical_all_prime))) /\ ((~(ftsf_factor_canonical_all_prime = 1) /\ forall frm_prime_left_ftsf_canonical_all_prime_prime frm_prime_right_ftsf_canonical_all_prime_prime. ftsf_factor_canonical_all_prime = frm_prime_left_ftsf_canonical_all_prime_prime * frm_prime_right_ftsf_canonical_all_prime_prime -> frm_prime_left_ftsf_canonical_all_prime_prime = 1 \/ frm_prime_right_ftsf_canonical_all_prime_prime = 1)))) /\ (forall i. (exists ftsf_gap_canonical_sorted_bound. ftsf_gap_canonical_sorted_bound + S S i = (l)) -> exists p q. ((((exists ff_h_ftsf_canonical_sorted_left. ff_h_ftsf_canonical_sorted_left + S (p) = S ((S (i)) * c)) /\ exists ff_q_ftsf_canonical_sorted_left. b = ff_q_ftsf_canonical_sorted_left * S ((S (i)) * c) + (p))) /\ ((((exists ff_h_ftsf_canonical_sorted_right. ff_h_ftsf_canonical_sorted_right + S (q) = S ((S (S i)) * c)) /\ exists ff_q_ftsf_canonical_sorted_right. b = ff_q_ftsf_canonical_sorted_right * S ((S (S i)) * c) + (q))) /\ (exists h. h + p = q))))))
  6. 0006apply prime_factorization_existence
  7. 0007exact hnonzero
  8. 0008cases hfactorization
  9. 0009cases hfactorization_witness
  10. 0010cases hfactorization_witness_witness
  11. 0011cases hfactorization_witness_witness_witness
  12. 0012cases hfactorization_witness_witness_witness_right
  13. 0013specialize beta_admissible_prime_factor_product_is_two_square x1
  14. 0014specialize beta_admissible_prime_factor_product_is_two_square x2
  15. 0015specialize beta_admissible_prime_factor_product_is_two_square x
  16. 0016specialize beta_admissible_prime_factor_product_is_two_square n
  17. 0017apply beta_admissible_prime_factor_product_is_two_square
  18. 0018exact hfactorization_witness_witness_witness_left
  19. 0019intro i
  20. 0020intro p
  21. 0021intro hi
  22. 0022intro hp
  23. 0023have hprime : (~(p = 1) /\ forall frm_prime_left_ftsf_canonical_local_prime frm_prime_right_ftsf_canonical_local_prime. p = frm_prime_left_ftsf_canonical_local_prime * frm_prime_right_ftsf_canonical_local_prime -> frm_prime_left_ftsf_canonical_local_prime = 1 \/ frm_prime_right_ftsf_canonical_local_prime = 1)
  24. 0024specialize beta_all_prime_entry_is_prime x1
  25. 0025specialize beta_all_prime_entry_is_prime x2
  26. 0026specialize beta_all_prime_entry_is_prime x
  27. 0027specialize beta_all_prime_entry_is_prime i
  28. 0028specialize beta_all_prime_entry_is_prime p
  29. 0029apply beta_all_prime_entry_is_prime
  30. 0030exact hfactorization_witness_witness_witness_right_left
  31. 0031exact hi
  32. 0032exact hp
  33. 0033split
  34. 0034exact hprime
  35. 0035specialize hdivisors p
  36. 0036apply hdivisors
  37. 0037exact hprime
  38. 0038specialize beta_factor_divides_product x1
  39. 0039specialize beta_factor_divides_product x2
  40. 0040specialize beta_factor_divides_product x
  41. 0041specialize beta_factor_divides_product n
  42. 0042specialize beta_factor_divides_product i
  43. 0043specialize beta_factor_divides_product p
  44. 0044apply beta_factor_divides_product
  45. 0045exact hi
  46. 0046exact hp
  47. 0047exact hfactorization_witness_witness_witness_left