TS002U · theorem body

beta_two_square_prefix_append_equal_pair

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

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.

Statement with defined notation

∀ b. ∀ c. ∀ l. ∀ n. ∀ q. Product(b,c,S S l,n) → (∀ x. ∀ y. Lt(x,l) → BetaAt(b,c,x,y) → ∃ z. ∃ m. y = z · z + m · m) → BetaAt(b,c,l,q) → BetaAt(b,c,S l,q) → ∃ 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

PD0014 Product
Exact expanded first-order 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)

Proof neighborhood

Direct theorem prerequisites

TS002T beta_product_adjacent_equal_pair_decomposes_as_square TS002R represented_factor_product_times_square_is_two_square

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

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.

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 product adjacent equal pair decomposes as squarerepresented factor product times square is two square
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(b,c,l,r)Original native command in the exact edition
  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 defined 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 : ∃ r. Product(b,c,l,r) ∧ n = r · (q · q)
    Exact native replay linehave 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