TF0005

beta_admissible_prime_factor_product_is_two_square

Any finite product whose decoded factors are prime two or prime one modulo four is constructively a sum of two squares.

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

∀ b. ∀ c. ∀ l. ∀ n. Product(b,c,l,n) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Prime(y) ∧ (y = 2 ∨ (∃ z. y = 4 · z + 1))) → ∃ x. ∃ y. n = x · x + y · y

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

Definition DAG

Lt(a,b) · 1Prime(p) · 1BetaAt(b,c,i,x) · 1Product(b,c,l,z) · 1

Actual proof prerequisites

beta_two_square_represented_factor_productprime_two_or_one_mod_four_is_sum_of_two_squares · checked external prerequisite
Original expanded first-order statement 
forall b c l n. (exists ff_u_ftsf_admissible_product ff_v_ftsf_admissible_product. ((((exists ff_h_ftsf_admissible_product_start. ff_h_ftsf_admissible_product_start + S (1) = S ((S (0)) * ff_v_ftsf_admissible_product)) /\ exists ff_q_ftsf_admissible_product_start. ff_u_ftsf_admissible_product = ff_q_ftsf_admissible_product_start * S ((S (0)) * ff_v_ftsf_admissible_product) + (1))) /\ ((((exists ff_h_ftsf_admissible_product_terminal. ff_h_ftsf_admissible_product_terminal + S (n) = S ((S (l)) * ff_v_ftsf_admissible_product)) /\ exists ff_q_ftsf_admissible_product_terminal. ff_u_ftsf_admissible_product = ff_q_ftsf_admissible_product_terminal * S ((S (l)) * ff_v_ftsf_admissible_product) + (n))) /\ forall ff_i_ftsf_admissible_product. (exists ff_lt_ftsf_admissible_product_bound. ff_lt_ftsf_admissible_product_bound + S ff_i_ftsf_admissible_product = l) -> exists ff_p_ftsf_admissible_product ff_r_ftsf_admissible_product ff_s_ftsf_admissible_product. ((((exists ff_h_ftsf_admissible_product_factor. ff_h_ftsf_admissible_product_factor + S (ff_p_ftsf_admissible_product) = S ((S (ff_i_ftsf_admissible_product)) * c)) /\ exists ff_q_ftsf_admissible_product_factor. b = ff_q_ftsf_admissible_product_factor * S ((S (ff_i_ftsf_admissible_product)) * c) + (ff_p_ftsf_admissible_product))) /\ ((((exists ff_h_ftsf_admissible_product_partial. ff_h_ftsf_admissible_product_partial + S (ff_r_ftsf_admissible_product) = S ((S (ff_i_ftsf_admissible_product)) * ff_v_ftsf_admissible_product)) /\ exists ff_q_ftsf_admissible_product_partial. ff_u_ftsf_admissible_product = ff_q_ftsf_admissible_product_partial * S ((S (ff_i_ftsf_admissible_product)) * ff_v_ftsf_admissible_product) + (ff_r_ftsf_admissible_product))) /\ ((((exists ff_h_ftsf_admissible_product_successor. ff_h_ftsf_admissible_product_successor + S (ff_s_ftsf_admissible_product) = S ((S (S ff_i_ftsf_admissible_product)) * ff_v_ftsf_admissible_product)) /\ exists ff_q_ftsf_admissible_product_successor. ff_u_ftsf_admissible_product = ff_q_ftsf_admissible_product_successor * S ((S (S ff_i_ftsf_admissible_product)) * ff_v_ftsf_admissible_product) + (ff_s_ftsf_admissible_product))) /\ ff_s_ftsf_admissible_product = ff_r_ftsf_admissible_product * ff_p_ftsf_admissible_product)))))) -> (forall ftsf_index_admissible_source ftsf_factor_admissible_source. (exists ftsf_gap_admissible_source_bound. ftsf_gap_admissible_source_bound + S ftsf_index_admissible_source = (l)) -> (((exists ff_h_ftsf_admissible_source_entry. ff_h_ftsf_admissible_source_entry + S (ftsf_factor_admissible_source) = S ((S (ftsf_index_admissible_source)) * c)) /\ exists ff_q_ftsf_admissible_source_entry. b = ff_q_ftsf_admissible_source_entry * S ((S (ftsf_index_admissible_source)) * c) + (ftsf_factor_admissible_source))) -> (((~(ftsf_factor_admissible_source = 1) /\ forall frm_prime_left_ftsf_admissible_source_prime frm_prime_right_ftsf_admissible_source_prime. ftsf_factor_admissible_source = frm_prime_left_ftsf_admissible_source_prime * frm_prime_right_ftsf_admissible_source_prime -> frm_prime_left_ftsf_admissible_source_prime = 1 \/ frm_prime_right_ftsf_admissible_source_prime = 1)) /\ (ftsf_factor_admissible_source = 2 \/ exists ftsf_residue_admissible_source. ftsf_factor_admissible_source = 4 * ftsf_residue_admissible_source + 1))) -> (exists ftsf_first_admissible_result ftsf_second_admissible_result. (n) = ftsf_first_admissible_result * ftsf_first_admissible_result + ftsf_second_admissible_result * ftsf_second_admissible_result)

Complete unchanged native tactic proof

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

Read the argument

Proof checkpoints

27 script commands · 7 reading checkpoints · 1 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)
beta two square represented factor product
01Fix variables and assumptionsL1–6

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

  1. L1
    intro b
  2. L2
    intro c
  3. L3
    intro l
  4. L4
    intro n
  5. L5
    intro hproduct
  6. L6
    intro hadmissible
02Use earlier factsL7–12

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

  1. L7
    specialize beta_two_square_represented_factor_product b
  2. L8
    specialize beta_two_square_represented_factor_product c
  3. L9
    specialize beta_two_square_represented_factor_product l
  4. L10
    specialize beta_two_square_represented_factor_product n
  5. L11
    apply beta_two_square_represented_factor_product
  6. L12
    exact hproduct
03Fix variables and assumptionsL13–16

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

  1. L13
    intro i
  2. L14
    intro p
  3. L15
    intro hi
  4. L16
    intro hp
04Use earlier factsL17–18

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

  1. L17
    specialize hadmissible i
  2. L18
    specialize hadmissible p
05Establish hclassL19–22

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

  1. L19
    have hclass : ((~(p = 1) /\ forall frm_prime_left_ftsf_admissible_local frm_prime_right_ftsf_admissible_local. p = frm_prime_left_ftsf_admissible_local * frm_prime_right_ftsf_admissible_local -> frm_prime_left_ftsf_admissible_local = 1 \/ frm_prime_right_ftsf_admissible_local = 1)) /\ (p = 2 \/ exists t. p = 4 * t + 1)
  2. L20
    apply hadmissible
  3. L21
    exact hi
  4. L22
    exact hp
06Separate the logical casesL23–23

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

  1. L23
    cases hclass
07Use earlier factsL24–27

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

  1. L24
    specialize prime_two_or_one_mod_four_is_sum_of_two_squares p
  2. L25
    apply prime_two_or_one_mod_four_is_sum_of_two_squares
  3. L26
    exact hclass_left
  4. L27
    exact hclass_right

Library-wide reading audit

Original defined command ledger · 27 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hproduct
  6. 0006intro hadmissible
  7. 0007specialize beta_two_square_represented_factor_product b
  8. 0008specialize beta_two_square_represented_factor_product c
  9. 0009specialize beta_two_square_represented_factor_product l
  10. 0010specialize beta_two_square_represented_factor_product n
  11. 0011apply beta_two_square_represented_factor_product
  12. 0012exact hproduct
  13. 0013intro i
  14. 0014intro p
  15. 0015intro hi
  16. 0016intro hp
  17. 0017specialize hadmissible i
  18. 0018specialize hadmissible p
  19. 0019have hclass : ((~(p = 1) /\ forall frm_prime_left_ftsf_admissible_local frm_prime_right_ftsf_admissible_local. p = frm_prime_left_ftsf_admissible_local * frm_prime_right_ftsf_admissible_local -> frm_prime_left_ftsf_admissible_local = 1 \/ frm_prime_right_ftsf_admissible_local = 1)) /\ (p = 2 \/ exists t. p = 4 * t + 1)
  20. 0020apply hadmissible
  21. 0021exact hi
  22. 0022exact hp
  23. 0023cases hclass
  24. 0024specialize prime_two_or_one_mod_four_is_sum_of_two_squares p
  25. 0025apply prime_two_or_one_mod_four_is_sum_of_two_squares
  26. 0026exact hclass_left
  27. 0027exact hclass_right