TS002M · theorem body

beta_two_square_represented_factor_product

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

Induction on an arbitrary beta-coded product constructs a two-square representation from represented decoded factors.

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) → ∃ z. ∃ m. y = z · z + m · m) → ∃ 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 PD0013 BetaAt PD0014 Product

In local proof propositions

PD0002 Lt PD0013 BetaAt PD0014 Product
Exact expanded first-order statement
forall b c l n. (exists ff_u_ftsf_fold_product ff_v_ftsf_fold_product. ((((exists ff_h_ftsf_fold_product_start. ff_h_ftsf_fold_product_start + S (1) = S ((S (0)) * ff_v_ftsf_fold_product)) /\ exists ff_q_ftsf_fold_product_start. ff_u_ftsf_fold_product = ff_q_ftsf_fold_product_start * S ((S (0)) * ff_v_ftsf_fold_product) + (1))) /\ ((((exists ff_h_ftsf_fold_product_terminal. ff_h_ftsf_fold_product_terminal + S (n) = S ((S (l)) * ff_v_ftsf_fold_product)) /\ exists ff_q_ftsf_fold_product_terminal. ff_u_ftsf_fold_product = ff_q_ftsf_fold_product_terminal * S ((S (l)) * ff_v_ftsf_fold_product) + (n))) /\ forall ff_i_ftsf_fold_product. (exists ff_lt_ftsf_fold_product_bound. ff_lt_ftsf_fold_product_bound + S ff_i_ftsf_fold_product = l) -> exists ff_p_ftsf_fold_product ff_r_ftsf_fold_product ff_s_ftsf_fold_product. ((((exists ff_h_ftsf_fold_product_factor. ff_h_ftsf_fold_product_factor + S (ff_p_ftsf_fold_product) = S ((S (ff_i_ftsf_fold_product)) * c)) /\ exists ff_q_ftsf_fold_product_factor. b = ff_q_ftsf_fold_product_factor * S ((S (ff_i_ftsf_fold_product)) * c) + (ff_p_ftsf_fold_product))) /\ ((((exists ff_h_ftsf_fold_product_partial. ff_h_ftsf_fold_product_partial + S (ff_r_ftsf_fold_product) = S ((S (ff_i_ftsf_fold_product)) * ff_v_ftsf_fold_product)) /\ exists ff_q_ftsf_fold_product_partial. ff_u_ftsf_fold_product = ff_q_ftsf_fold_product_partial * S ((S (ff_i_ftsf_fold_product)) * ff_v_ftsf_fold_product) + (ff_r_ftsf_fold_product))) /\ ((((exists ff_h_ftsf_fold_product_successor. ff_h_ftsf_fold_product_successor + S (ff_s_ftsf_fold_product) = S ((S (S ff_i_ftsf_fold_product)) * ff_v_ftsf_fold_product)) /\ exists ff_q_ftsf_fold_product_successor. ff_u_ftsf_fold_product = ff_q_ftsf_fold_product_successor * S ((S (S ff_i_ftsf_fold_product)) * ff_v_ftsf_fold_product) + (ff_s_ftsf_fold_product))) /\ ff_s_ftsf_fold_product = ff_r_ftsf_fold_product * ff_p_ftsf_fold_product)))))) -> (forall ftsf_index_fold_prefix ftsf_factor_fold_prefix. (exists ftsf_gap_fold_prefix_bound. ftsf_gap_fold_prefix_bound + S ftsf_index_fold_prefix = (l)) -> (((exists ff_h_ftsf_fold_prefix_entry. ff_h_ftsf_fold_prefix_entry + S (ftsf_factor_fold_prefix) = S ((S (ftsf_index_fold_prefix)) * c)) /\ exists ff_q_ftsf_fold_prefix_entry. b = ff_q_ftsf_fold_prefix_entry * S ((S (ftsf_index_fold_prefix)) * c) + (ftsf_factor_fold_prefix))) -> (exists ftsf_first_fold_prefix_representation ftsf_second_fold_prefix_representation. (ftsf_factor_fold_prefix) = ftsf_first_fold_prefix_representation * ftsf_first_fold_prefix_representation + ftsf_second_fold_prefix_representation * ftsf_second_fold_prefix_representation)) -> (exists ftsf_first_fold_result ftsf_second_fold_result. (n) = ftsf_first_fold_result * ftsf_first_fold_result + ftsf_second_fold_result * ftsf_second_fold_result)

Proof neighborhood

Direct theorem prerequisites

beta_product_zero · Stable closed beta_product_succ_decompose · Stable closed TS002J beta_two_square_prefix_drop_last TS002L beta_two_square_prefix_last_represented TS001X two_square_representation_multiplicatively_closed

Direct theorem dependents

TS002N beta_witnessed_two_square_factor_product TS002Q beta_admissible_prime_factor_product_is_two_square TS002R represented_factor_product_times_square_is_two_square TS002S beta_grouped_prime_square_factor_product_is_two_square

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

55 script commands · 12 reading checkpoints · 5 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 prefix drop lastbeta two square prefix last representedtwo square representation multiplicatively closed
01Fix variables and assumptionsL1–2

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

  1. L1
    intro b
  2. L2
    intro c
02Induction on lL3–6

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction l
  2. L4
    intro n
  3. L5
    intro hproduct
  4. L6
    intro hprefix
03Establish hunitL7–12

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

  1. L7
    have hunit : n = 1
  2. L8
    specialize beta_product_zero b
  3. L9
    specialize beta_product_zero c
  4. L10
    specialize beta_product_zero n
  5. L11
    apply beta_product_zero
  6. L12
    exact hproduct
04Construct an explicit witnessL13–14

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

  1. L13
    exists 1
  2. L14
    exists 0
05Calculate and transport equalitiesL15–16

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

  1. L15
    rewrite hunit
  2. L16
    norm_num
06Fix variables and assumptionsL17–19

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

  1. L17
    intro n
  2. L18
    intro hproduct
  3. L19
    intro hprefix
07Establish hdecompositionL20–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product succ decompose.

  1. L20
    have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)Definitions: BetaAt(b,c,l,a)Product(b,c,l,r)Original native command in the exact edition
  2. L21
    specialize beta_product_succ_decompose b
  3. L22
    specialize beta_product_succ_decompose c
  4. L23
    specialize beta_product_succ_decompose l
  5. L24
    specialize beta_product_succ_decompose n
  6. L25
    apply beta_product_succ_decompose
  7. L26
    exact hproduct
08Separate the logical casesL27–30

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

  1. L27
    cases hdecomposition
  2. L28
    cases hdecomposition_witness
  3. L29
    cases hdecomposition_witness_witness
  4. L30
    cases hdecomposition_witness_witness_right
09Establish hrestrictedL31–36

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta two square prefix drop last.

  1. L31
    have hrestricted : ∀ ftsf_index_fold_local_prefix. ∀ ftsf_factor_fold_local_prefix. Lt(ftsf_index_fold_local_prefix,l) → BetaAt(b,c,ftsf_index_fold_local_prefix,ftsf_factor_fold_local_prefix) → ∃ x. ∃ y. ftsf_factor_fold_local_prefix = x · x + y · yDefinitions: Lt(ftsf_index_fold_local_prefix,l)BetaAt(b,c,ftsf_index_fold_local_prefix,ftsf_factor_fold_local_prefix)Original native command in the exact edition
  2. L32
    specialize beta_two_square_prefix_drop_last b
  3. L33
    specialize beta_two_square_prefix_drop_last c
  4. L34
    specialize beta_two_square_prefix_drop_last l
  5. L35
    apply beta_two_square_prefix_drop_last
  6. L36
    exact hprefix
10Establish hpartialL37–41

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

  1. L37
    have hpartial : exists ftsf_first_fold_partial ftsf_second_fold_partial. (x1) = ftsf_first_fold_partial * ftsf_first_fold_partial + ftsf_second_fold_partial * ftsf_second_fold_partial
  2. L38
    specialize IH x1
  3. L39
    apply IH
  4. L40
    exact hdecomposition_witness_witness_right_left
  5. L41
    exact hrestricted
11Establish hlastL42–51

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta two square prefix last represented.

  1. L42
    have hlast : exists ftsf_first_fold_last_representation ftsf_second_fold_last_representation. (x) = ftsf_first_fold_last_representation * ftsf_first_fold_last_representation + ftsf_second_fold_last_representation * ftsf_second_fold_last_representation
  2. L43
    specialize beta_two_square_prefix_last_represented b
  3. L44
    specialize beta_two_square_prefix_last_represented c
  4. L45
    specialize beta_two_square_prefix_last_represented l
  5. L46
    specialize beta_two_square_prefix_last_represented x
  6. L47
    apply beta_two_square_prefix_last_represented
  7. L48
    exact hprefix
  8. L49
    exact hdecomposition_witness_witness_left
  9. L50
    rewrite hdecomposition_witness_witness_right_right
  10. L51
    specialize two_square_representation_multiplicatively_closed x1
12Use earlier factsL52–55

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

  1. L52
    specialize two_square_representation_multiplicatively_closed x
  2. L53
    apply two_square_representation_multiplicatively_closed
  3. L54
    exact hpartial
  4. L55
    exact hlast

Library-wide reading audit

Original defined command ledger · 55 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003induction l
  4. 0004intro n
  5. 0005intro hproduct
  6. 0006intro hprefix
  7. 0007have hunit : n = 1
  8. 0008specialize beta_product_zero b
  9. 0009specialize beta_product_zero c
  10. 0010specialize beta_product_zero n
  11. 0011apply beta_product_zero
  12. 0012exact hproduct
  13. 0013exists 1
  14. 0014exists 0
  15. 0015rewrite hunit
  16. 0016norm_num
  17. 0017intro n
  18. 0018intro hproduct
  19. 0019intro hprefix
  20. 0020have hdecomposition : ∃ a. ∃ r. BetaAt(b,c,l,a) ∧ (Product(b,c,l,r) ∧ n = r · a)
    Exact native replay linehave hdecomposition : exists a r. ((((exists ff_h_ftsf_fold_last. ff_h_ftsf_fold_last + S (a) = S ((S (l)) * c)) /\ exists ff_q_ftsf_fold_last. b = ff_q_ftsf_fold_last * S ((S (l)) * c) + (a))) /\ ((exists ff_u_ftsf_fold_local ff_v_ftsf_fold_local. ((((exists ff_h_ftsf_fold_local_start. ff_h_ftsf_fold_local_start + S (1) = S ((S (0)) * ff_v_ftsf_fold_local)) /\ exists ff_q_ftsf_fold_local_start. ff_u_ftsf_fold_local = ff_q_ftsf_fold_local_start * S ((S (0)) * ff_v_ftsf_fold_local) + (1))) /\ ((((exists ff_h_ftsf_fold_local_terminal. ff_h_ftsf_fold_local_terminal + S (r) = S ((S (l)) * ff_v_ftsf_fold_local)) /\ exists ff_q_ftsf_fold_local_terminal. ff_u_ftsf_fold_local = ff_q_ftsf_fold_local_terminal * S ((S (l)) * ff_v_ftsf_fold_local) + (r))) /\ forall ff_i_ftsf_fold_local. (exists ff_lt_ftsf_fold_local_bound. ff_lt_ftsf_fold_local_bound + S ff_i_ftsf_fold_local = l) -> exists ff_p_ftsf_fold_local ff_r_ftsf_fold_local ff_s_ftsf_fold_local. ((((exists ff_h_ftsf_fold_local_factor. ff_h_ftsf_fold_local_factor + S (ff_p_ftsf_fold_local) = S ((S (ff_i_ftsf_fold_local)) * c)) /\ exists ff_q_ftsf_fold_local_factor. b = ff_q_ftsf_fold_local_factor * S ((S (ff_i_ftsf_fold_local)) * c) + (ff_p_ftsf_fold_local))) /\ ((((exists ff_h_ftsf_fold_local_partial. ff_h_ftsf_fold_local_partial + S (ff_r_ftsf_fold_local) = S ((S (ff_i_ftsf_fold_local)) * ff_v_ftsf_fold_local)) /\ exists ff_q_ftsf_fold_local_partial. ff_u_ftsf_fold_local = ff_q_ftsf_fold_local_partial * S ((S (ff_i_ftsf_fold_local)) * ff_v_ftsf_fold_local) + (ff_r_ftsf_fold_local))) /\ ((((exists ff_h_ftsf_fold_local_successor. ff_h_ftsf_fold_local_successor + S (ff_s_ftsf_fold_local) = S ((S (S ff_i_ftsf_fold_local)) * ff_v_ftsf_fold_local)) /\ exists ff_q_ftsf_fold_local_successor. ff_u_ftsf_fold_local = ff_q_ftsf_fold_local_successor * S ((S (S ff_i_ftsf_fold_local)) * ff_v_ftsf_fold_local) + (ff_s_ftsf_fold_local))) /\ ff_s_ftsf_fold_local = ff_r_ftsf_fold_local * ff_p_ftsf_fold_local)))))) /\ n = r * a))
  21. 0021specialize beta_product_succ_decompose b
  22. 0022specialize beta_product_succ_decompose c
  23. 0023specialize beta_product_succ_decompose l
  24. 0024specialize beta_product_succ_decompose n
  25. 0025apply beta_product_succ_decompose
  26. 0026exact hproduct
  27. 0027cases hdecomposition
  28. 0028cases hdecomposition_witness
  29. 0029cases hdecomposition_witness_witness
  30. 0030cases hdecomposition_witness_witness_right
  31. 0031have hrestricted : ∀ ftsf_index_fold_local_prefix. ∀ ftsf_factor_fold_local_prefix. Lt(ftsf_index_fold_local_prefix,l) → BetaAt(b,c,ftsf_index_fold_local_prefix,ftsf_factor_fold_local_prefix) → ∃ x. ∃ y. ftsf_factor_fold_local_prefix = x · x + y · y
    Exact native replay linehave hrestricted : forall ftsf_index_fold_local_prefix ftsf_factor_fold_local_prefix. (exists ftsf_gap_fold_local_prefix_bound. ftsf_gap_fold_local_prefix_bound + S ftsf_index_fold_local_prefix = (l)) -> (((exists ff_h_ftsf_fold_local_prefix_entry. ff_h_ftsf_fold_local_prefix_entry + S (ftsf_factor_fold_local_prefix) = S ((S (ftsf_index_fold_local_prefix)) * c)) /\ exists ff_q_ftsf_fold_local_prefix_entry. b = ff_q_ftsf_fold_local_prefix_entry * S ((S (ftsf_index_fold_local_prefix)) * c) + (ftsf_factor_fold_local_prefix))) -> (exists ftsf_first_fold_local_prefix_representation ftsf_second_fold_local_prefix_representation. (ftsf_factor_fold_local_prefix) = ftsf_first_fold_local_prefix_representation * ftsf_first_fold_local_prefix_representation + ftsf_second_fold_local_prefix_representation * ftsf_second_fold_local_prefix_representation)
  32. 0032specialize beta_two_square_prefix_drop_last b
  33. 0033specialize beta_two_square_prefix_drop_last c
  34. 0034specialize beta_two_square_prefix_drop_last l
  35. 0035apply beta_two_square_prefix_drop_last
  36. 0036exact hprefix
  37. 0037have hpartial : exists ftsf_first_fold_partial ftsf_second_fold_partial. (x1) = ftsf_first_fold_partial * ftsf_first_fold_partial + ftsf_second_fold_partial * ftsf_second_fold_partial
  38. 0038specialize IH x1
  39. 0039apply IH
  40. 0040exact hdecomposition_witness_witness_right_left
  41. 0041exact hrestricted
  42. 0042have hlast : exists ftsf_first_fold_last_representation ftsf_second_fold_last_representation. (x) = ftsf_first_fold_last_representation * ftsf_first_fold_last_representation + ftsf_second_fold_last_representation * ftsf_second_fold_last_representation
  43. 0043specialize beta_two_square_prefix_last_represented b
  44. 0044specialize beta_two_square_prefix_last_represented c
  45. 0045specialize beta_two_square_prefix_last_represented l
  46. 0046specialize beta_two_square_prefix_last_represented x
  47. 0047apply beta_two_square_prefix_last_represented
  48. 0048exact hprefix
  49. 0049exact hdecomposition_witness_witness_left
  50. 0050rewrite hdecomposition_witness_witness_right_right
  51. 0051specialize two_square_representation_multiplicatively_closed x1
  52. 0052specialize two_square_representation_multiplicatively_closed x
  53. 0053apply two_square_representation_multiplicatively_closed
  54. 0054exact hpartial
  55. 0055exact hlast