TS002S · theorem body

beta_grouped_prime_square_factor_product_is_two_square

dependency-curried kernel-checked candidate body; not enrolled in Alpha or Stable

A beta-coded grouped product folds represented prime singletons together with explicit square blocks pairing primes congruent to three modulo four.

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

∀ b. ∀ c. ∀ l. ∀ n. Product(b,c,l,n) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → Prime(y) ∧ (y = 2 ∨ Mod4One(y)) ∨ (∃ z. ∃ m. Prime(z) ∧ (z = 4 · m + 3 ∧ y = z · z))) → ∃ x. ∃ y. n = 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

PD0002 Lt PD0004 Prime PD0011 Mod4One PD0013 BetaAt PD0014 Product

In local proof propositions

PD0004 Prime PD0011 Mod4One
Exact expanded first-order statement
forall b c l n. (exists ff_u_ftsf_grouped_product ff_v_ftsf_grouped_product. ((((exists ff_h_ftsf_grouped_product_start. ff_h_ftsf_grouped_product_start + S (1) = S ((S (0)) * ff_v_ftsf_grouped_product)) /\ exists ff_q_ftsf_grouped_product_start. ff_u_ftsf_grouped_product = ff_q_ftsf_grouped_product_start * S ((S (0)) * ff_v_ftsf_grouped_product) + (1))) /\ ((((exists ff_h_ftsf_grouped_product_terminal. ff_h_ftsf_grouped_product_terminal + S (n) = S ((S (l)) * ff_v_ftsf_grouped_product)) /\ exists ff_q_ftsf_grouped_product_terminal. ff_u_ftsf_grouped_product = ff_q_ftsf_grouped_product_terminal * S ((S (l)) * ff_v_ftsf_grouped_product) + (n))) /\ forall ff_i_ftsf_grouped_product. (exists ff_lt_ftsf_grouped_product_bound. ff_lt_ftsf_grouped_product_bound + S ff_i_ftsf_grouped_product = l) -> exists ff_p_ftsf_grouped_product ff_r_ftsf_grouped_product ff_s_ftsf_grouped_product. ((((exists ff_h_ftsf_grouped_product_factor. ff_h_ftsf_grouped_product_factor + S (ff_p_ftsf_grouped_product) = S ((S (ff_i_ftsf_grouped_product)) * c)) /\ exists ff_q_ftsf_grouped_product_factor. b = ff_q_ftsf_grouped_product_factor * S ((S (ff_i_ftsf_grouped_product)) * c) + (ff_p_ftsf_grouped_product))) /\ ((((exists ff_h_ftsf_grouped_product_partial. ff_h_ftsf_grouped_product_partial + S (ff_r_ftsf_grouped_product) = S ((S (ff_i_ftsf_grouped_product)) * ff_v_ftsf_grouped_product)) /\ exists ff_q_ftsf_grouped_product_partial. ff_u_ftsf_grouped_product = ff_q_ftsf_grouped_product_partial * S ((S (ff_i_ftsf_grouped_product)) * ff_v_ftsf_grouped_product) + (ff_r_ftsf_grouped_product))) /\ ((((exists ff_h_ftsf_grouped_product_successor. ff_h_ftsf_grouped_product_successor + S (ff_s_ftsf_grouped_product) = S ((S (S ff_i_ftsf_grouped_product)) * ff_v_ftsf_grouped_product)) /\ exists ff_q_ftsf_grouped_product_successor. ff_u_ftsf_grouped_product = ff_q_ftsf_grouped_product_successor * S ((S (S ff_i_ftsf_grouped_product)) * ff_v_ftsf_grouped_product) + (ff_s_ftsf_grouped_product))) /\ ff_s_ftsf_grouped_product = ff_r_ftsf_grouped_product * ff_p_ftsf_grouped_product)))))) -> (forall ftsf_index_grouped_source ftsf_factor_grouped_source. (exists ftsf_gap_grouped_source_bound. ftsf_gap_grouped_source_bound + S ftsf_index_grouped_source = (l)) -> (((exists ff_h_ftsf_grouped_source_entry. ff_h_ftsf_grouped_source_entry + S (ftsf_factor_grouped_source) = S ((S (ftsf_index_grouped_source)) * c)) /\ exists ff_q_ftsf_grouped_source_entry. b = ff_q_ftsf_grouped_source_entry * S ((S (ftsf_index_grouped_source)) * c) + (ftsf_factor_grouped_source))) -> ((((~(ftsf_factor_grouped_source = 1) /\ forall frm_prime_left_ftsf_grouped_source_good_prime frm_prime_right_ftsf_grouped_source_good_prime. ftsf_factor_grouped_source = frm_prime_left_ftsf_grouped_source_good_prime * frm_prime_right_ftsf_grouped_source_good_prime -> frm_prime_left_ftsf_grouped_source_good_prime = 1 \/ frm_prime_right_ftsf_grouped_source_good_prime = 1)) /\ (ftsf_factor_grouped_source = 2 \/ exists ftsf_good_residue_grouped_source. ftsf_factor_grouped_source = 4 * ftsf_good_residue_grouped_source + 1)) \/ exists ftsf_bad_prime_grouped_source ftsf_bad_residue_grouped_source. (((~(ftsf_bad_prime_grouped_source = 1) /\ forall frm_prime_left_ftsf_grouped_source_bad_prime frm_prime_right_ftsf_grouped_source_bad_prime. ftsf_bad_prime_grouped_source = frm_prime_left_ftsf_grouped_source_bad_prime * frm_prime_right_ftsf_grouped_source_bad_prime -> frm_prime_left_ftsf_grouped_source_bad_prime = 1 \/ frm_prime_right_ftsf_grouped_source_bad_prime = 1)) /\ (ftsf_bad_prime_grouped_source = 4 * ftsf_bad_residue_grouped_source + 3 /\ ftsf_factor_grouped_source = ftsf_bad_prime_grouped_source * ftsf_bad_prime_grouped_source)))) -> (exists ftsf_first_grouped_result ftsf_second_grouped_result. (n) = ftsf_first_grouped_result * ftsf_first_grouped_result + ftsf_second_grouped_result * ftsf_second_grouped_result)

Proof neighborhood

Direct theorem prerequisites

TS002M beta_two_square_represented_factor_product TS002O prime_two_or_one_mod_four_is_sum_of_two_squares TS001Z every_natural_square_is_sum_of_two_squares

Direct theorem dependents

none

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

35 script commands · 10 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 (3)
beta two square represented factor productprime two or one mod four is sum of two squaresevery natural square is sum of two squares
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 hgrouped
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 hgrouped i
  2. L18
    specialize hgrouped p
05Establish hblockL19–22

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

  1. L19
    have hblock : Prime(p) ∧ (p = 2 ∨ Mod4One(p)) ∨ (∃ x. ∃ y. Prime(x) ∧ (x = 4 · y + 3 ∧ p = x · x))Definitions: Prime(p)Mod4One(p)Prime(x)Original native command in the exact edition
  2. L20
    apply hgrouped
  3. L21
    exact hi
  4. L22
    exact hp
06Separate the logical casesL23–24

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

  1. L23
    cases hblock
  2. L24
    cases hblock_left
07Use earlier factsL25–28

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

  1. L25
    specialize prime_two_or_one_mod_four_is_sum_of_two_squares p
  2. L26
    apply prime_two_or_one_mod_four_is_sum_of_two_squares
  3. L27
    exact hblock_left_left
  4. L28
    exact hblock_left_right
08Separate the logical casesL29–32

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

  1. L29
    cases hblock_right
  2. L30
    cases hblock_right_witness
  3. L31
    cases hblock_right_witness_witness
  4. L32
    cases hblock_right_witness_witness_right
09Calculate and transport equalitiesL33–33

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

  1. L33
    rewrite hblock_right_witness_witness_right_right
10Use earlier factsL34–35

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

  1. L34
    specialize every_natural_square_is_sum_of_two_squares x
  2. L35
    exact every_natural_square_is_sum_of_two_squares

Library-wide reading audit

Original defined command ledger · 35 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro hproduct
  6. 0006intro hgrouped
  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 hgrouped i
  18. 0018specialize hgrouped p
  19. 0019have hblock : Prime(p) ∧ (p = 2 ∨ Mod4One(p)) ∨ (∃ x. ∃ y. Prime(x) ∧ (x = 4 · y + 3 ∧ p = x · x))
    Exact native replay linehave hblock : ((((~(p = 1) /\ forall frm_prime_left_ftsf_grouped_local_good frm_prime_right_ftsf_grouped_local_good. p = frm_prime_left_ftsf_grouped_local_good * frm_prime_right_ftsf_grouped_local_good -> frm_prime_left_ftsf_grouped_local_good = 1 \/ frm_prime_right_ftsf_grouped_local_good = 1)) /\ (p = 2 \/ exists t. p = 4 * t + 1)) \/ exists q t. (((~(q = 1) /\ forall frm_prime_left_ftsf_grouped_local_bad frm_prime_right_ftsf_grouped_local_bad. q = frm_prime_left_ftsf_grouped_local_bad * frm_prime_right_ftsf_grouped_local_bad -> frm_prime_left_ftsf_grouped_local_bad = 1 \/ frm_prime_right_ftsf_grouped_local_bad = 1)) /\ (q = 4 * t + 3 /\ p = q * q)))
  20. 0020apply hgrouped
  21. 0021exact hi
  22. 0022exact hp
  23. 0023cases hblock
  24. 0024cases hblock_left
  25. 0025specialize prime_two_or_one_mod_four_is_sum_of_two_squares p
  26. 0026apply prime_two_or_one_mod_four_is_sum_of_two_squares
  27. 0027exact hblock_left_left
  28. 0028exact hblock_left_right
  29. 0029cases hblock_right
  30. 0030cases hblock_right_witness
  31. 0031cases hblock_right_witness_witness
  32. 0032cases hblock_right_witness_witness_right
  33. 0033rewrite hblock_right_witness_witness_right_right
  34. 0034specialize every_natural_square_is_sum_of_two_squares x
  35. 0035exact every_natural_square_is_sum_of_two_squares