TS002U

beta_two_square_prefix_append_equal_pair

Dependency-curried candidate body; not Alpha-enrolled; no checked-use authority

Appending two equal adjacent decoded factors to any represented beta-coded prefix preserves constructive two-square representability.

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.

Exact expanded first-order arithmetic statement

forall b c l n q. (exists ff_u_ftsf_pair_product ff_v_ftsf_pair_product. ((((exists ff_h_ftsf_pair_product_start. ff_h_ftsf_pair_product_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_start. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_start * S ((S (0)) * ff_v_ftsf_pair_product) + (1))) /\ ((((exists ff_h_ftsf_pair_product_terminal. ff_h_ftsf_pair_product_terminal + S (n) = S ((S (S S l)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_terminal. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_terminal * S ((S (S S l)) * ff_v_ftsf_pair_product) + (n))) /\ forall ff_i_ftsf_pair_product. (exists ff_lt_ftsf_pair_product_bound. ff_lt_ftsf_pair_product_bound + S ff_i_ftsf_pair_product = S S l) -> exists ff_p_ftsf_pair_product ff_r_ftsf_pair_product ff_s_ftsf_pair_product. ((((exists ff_h_ftsf_pair_product_factor. ff_h_ftsf_pair_product_factor + S (ff_p_ftsf_pair_product) = S ((S (ff_i_ftsf_pair_product)) * c)) /\ exists ff_q_ftsf_pair_product_factor. b = ff_q_ftsf_pair_product_factor * S ((S (ff_i_ftsf_pair_product)) * c) + (ff_p_ftsf_pair_product))) /\ ((((exists ff_h_ftsf_pair_product_partial. ff_h_ftsf_pair_product_partial + S (ff_r_ftsf_pair_product) = S ((S (ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_partial. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_partial * S ((S (ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product) + (ff_r_ftsf_pair_product))) /\ ((((exists ff_h_ftsf_pair_product_successor. ff_h_ftsf_pair_product_successor + S (ff_s_ftsf_pair_product) = S ((S (S ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product)) /\ exists ff_q_ftsf_pair_product_successor. ff_u_ftsf_pair_product = ff_q_ftsf_pair_product_successor * S ((S (S ff_i_ftsf_pair_product)) * ff_v_ftsf_pair_product) + (ff_s_ftsf_pair_product))) /\ ff_s_ftsf_pair_product = ff_r_ftsf_pair_product * ff_p_ftsf_pair_product)))))) -> (forall ftsf_index_drop_old ftsf_factor_drop_old. (exists ftsf_gap_drop_old_bound. ftsf_gap_drop_old_bound + S ftsf_index_drop_old = (l)) -> (((exists ff_h_ftsf_drop_old_entry. ff_h_ftsf_drop_old_entry + S (ftsf_factor_drop_old) = S ((S (ftsf_index_drop_old)) * c)) /\ exists ff_q_ftsf_drop_old_entry. b = ff_q_ftsf_drop_old_entry * S ((S (ftsf_index_drop_old)) * c) + (ftsf_factor_drop_old))) -> (exists ftsf_first_drop_old_representation ftsf_second_drop_old_representation. (ftsf_factor_drop_old) = ftsf_first_drop_old_representation * ftsf_first_drop_old_representation + ftsf_second_drop_old_representation * ftsf_second_drop_old_representation)) -> (((exists ff_h_ftsf_pair_first. ff_h_ftsf_pair_first + S (q) = S ((S (l)) * c)) /\ exists ff_q_ftsf_pair_first. b = ff_q_ftsf_pair_first * S ((S (l)) * c) + (q))) -> (((exists ff_h_ftsf_pair_second. ff_h_ftsf_pair_second + S (q) = S ((S (S l)) * c)) /\ exists ff_q_ftsf_pair_second. b = ff_q_ftsf_pair_second * S ((S (S l)) * c) + (q))) -> (exists ftsf_first_pair_result ftsf_second_pair_result. (n) = ftsf_first_pair_result * ftsf_first_pair_result + ftsf_second_pair_result * ftsf_second_pair_result)

Constructive proof overview

Generated structural guide

Appending two equal adjacent decoded factors to any represented beta-coded prefix preserves constructive two-square representability.

The unchanged tactic script uses 2 declared prerequisites and contains 31 exact native proof lines.

dependency-curried kernel-checked theorem body; Alpha enrollment and checked-use authority follow separately sealed release evidence; Stable membership remains unchanged

Proof neighborhood

Direct dependencies

TS002T beta_product_adjacent_equal_pair_decomposes_as_square TS002R represented_factor_product_times_square_is_two_square

Direct dependents

none

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Local theorem links identify exact declared prerequisites. This dependency-curried candidate body does not grant checked theorem use or Stable membership.

Read the argument

Proof checkpoints

31 script commands · 5 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.

Named ingredients (2)
beta product adjacent equal pair decomposes as squarerepresented factor product times square is two square

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–9

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 q
  6. L6
    intro hproduct
  7. L7
    intro hprefix
  8. L8
    intro hfirst
  9. L9
    intro hsecond
02Use earlier factsL10–14

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

  1. L10
    specialize beta_product_adjacent_equal_pair_decomposes_as_square b
  2. L11
    specialize beta_product_adjacent_equal_pair_decomposes_as_square c
  3. L12
    specialize beta_product_adjacent_equal_pair_decomposes_as_square l
  4. L13
    specialize beta_product_adjacent_equal_pair_decomposes_as_square n
  5. L14
    specialize beta_product_adjacent_equal_pair_decomposes_as_square q
03Establish hdecompositionL15–19

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply beta product adjacent equal pair decomposes as square.

  1. L15
    have hdecomposition : ∃ r. Product(b,c,l,r) ∧ n = r · (q · q)Definitions: Product
  2. L16
    apply beta_product_adjacent_equal_pair_decomposes_as_square
  3. L17
    exact hproduct
  4. L18
    exact hfirst
  5. L19
    exact hsecond
04Separate the logical casesL20–21

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

  1. L20
    cases hdecomposition
  2. L21
    cases hdecomposition_witness
05Use earlier factsL22–31

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

  1. L22
    specialize represented_factor_product_times_square_is_two_square b
  2. L23
    specialize represented_factor_product_times_square_is_two_square c
  3. L24
    specialize represented_factor_product_times_square_is_two_square l
  4. L25
    specialize represented_factor_product_times_square_is_two_square x
  5. L26
    specialize represented_factor_product_times_square_is_two_square q
  6. L27
    specialize represented_factor_product_times_square_is_two_square n
  7. L28
    apply represented_factor_product_times_square_is_two_square
  8. L29
    exact hdecomposition_witness_left
  9. L30
    exact hprefix
  10. L31
    exact hdecomposition_witness_right

Library-wide reading audit

Original exact command ledger · 31 lines
  1. 0001intro b
  2. 0002intro c
  3. 0003intro l
  4. 0004intro n
  5. 0005intro q
  6. 0006intro hproduct
  7. 0007intro hprefix
  8. 0008intro hfirst
  9. 0009intro hsecond
  10. 0010specialize beta_product_adjacent_equal_pair_decomposes_as_square b
  11. 0011specialize beta_product_adjacent_equal_pair_decomposes_as_square c
  12. 0012specialize beta_product_adjacent_equal_pair_decomposes_as_square l
  13. 0013specialize beta_product_adjacent_equal_pair_decomposes_as_square n
  14. 0014specialize beta_product_adjacent_equal_pair_decomposes_as_square q
  15. 0015have hdecomposition : exists r. ((exists ff_u_ftsf_pair_local ff_v_ftsf_pair_local. ((((exists ff_h_ftsf_pair_local_start. ff_h_ftsf_pair_local_start + S (1) = S ((S (0)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_start. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_start * S ((S (0)) * ff_v_ftsf_pair_local) + (1))) /\ ((((exists ff_h_ftsf_pair_local_terminal. ff_h_ftsf_pair_local_terminal + S (r) = S ((S (l)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_terminal. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_terminal * S ((S (l)) * ff_v_ftsf_pair_local) + (r))) /\ forall ff_i_ftsf_pair_local. (exists ff_lt_ftsf_pair_local_bound. ff_lt_ftsf_pair_local_bound + S ff_i_ftsf_pair_local = l) -> exists ff_p_ftsf_pair_local ff_r_ftsf_pair_local ff_s_ftsf_pair_local. ((((exists ff_h_ftsf_pair_local_factor. ff_h_ftsf_pair_local_factor + S (ff_p_ftsf_pair_local) = S ((S (ff_i_ftsf_pair_local)) * c)) /\ exists ff_q_ftsf_pair_local_factor. b = ff_q_ftsf_pair_local_factor * S ((S (ff_i_ftsf_pair_local)) * c) + (ff_p_ftsf_pair_local))) /\ ((((exists ff_h_ftsf_pair_local_partial. ff_h_ftsf_pair_local_partial + S (ff_r_ftsf_pair_local) = S ((S (ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_partial. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_partial * S ((S (ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local) + (ff_r_ftsf_pair_local))) /\ ((((exists ff_h_ftsf_pair_local_successor. ff_h_ftsf_pair_local_successor + S (ff_s_ftsf_pair_local) = S ((S (S ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local)) /\ exists ff_q_ftsf_pair_local_successor. ff_u_ftsf_pair_local = ff_q_ftsf_pair_local_successor * S ((S (S ff_i_ftsf_pair_local)) * ff_v_ftsf_pair_local) + (ff_s_ftsf_pair_local))) /\ ff_s_ftsf_pair_local = ff_r_ftsf_pair_local * ff_p_ftsf_pair_local)))))) /\ n = r * (q * q))
  16. 0016apply beta_product_adjacent_equal_pair_decomposes_as_square
  17. 0017exact hproduct
  18. 0018exact hfirst
  19. 0019exact hsecond
  20. 0020cases hdecomposition
  21. 0021cases hdecomposition_witness
  22. 0022specialize represented_factor_product_times_square_is_two_square b
  23. 0023specialize represented_factor_product_times_square_is_two_square c
  24. 0024specialize represented_factor_product_times_square_is_two_square l
  25. 0025specialize represented_factor_product_times_square_is_two_square x
  26. 0026specialize represented_factor_product_times_square_is_two_square q
  27. 0027specialize represented_factor_product_times_square_is_two_square n
  28. 0028apply represented_factor_product_times_square_is_two_square
  29. 0029exact hdecomposition_witness_left
  30. 0030exact hprefix
  31. 0031exact hdecomposition_witness_right